[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a✝ b c d : WithTop α
x y : α
a : WithTop α
⊢ a + ⊤ = ⊤
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y : α
⊢ none + ⊤ = ⊤
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y val✝ : α
⊢ Option.some val✝ + ⊤ = ⊤
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y : α
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝ : Add α
b c d : WithTop α
x y : α
⊢ none + b = ⊤ ↔ none = ⊤ ∨ b = ⊤
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u
β : Type v
inst✝ : Add α
b c d : WithTop α
x y val✝ : α
⊢ Option.some val✝ + b = ⊤ ↔ Option.some val✝ = ⊤ ∨ b = ⊤
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u
β : Type v
inst✝ : Add α
c d : WithTop α
x y : α
⊢ none + none = ⊤ ↔ none = ⊤ ∨ none = ⊤
[PROOFSTEP]
simp [none_eq_top, some_eq_coe, ← WithTop.coe_add]
[GOAL]
case none.some
α : Type u
β : Type v
inst✝ : Add α
c d : WithTop α
x y val✝ : α
⊢ none + Option.some val✝ = ⊤ ↔ none = ⊤ ∨ Option.some val✝ = ⊤
[PROOFSTEP]
simp [none_eq_top, some_eq_coe, ← WithTop.coe_add]
[GOAL]
case some.none
α : Type u
β : Type v
inst✝ : Add α
c d : WithTop α
x y val✝ : α
⊢ Option.some val✝ + none = ⊤ ↔ Option.some val✝ = ⊤ ∨ none = ⊤
[PROOFSTEP]
simp [none_eq_top, some_eq_coe, ← WithTop.coe_add]
[GOAL]
case some.some
α : Type u
β : Type v
inst✝ : Add α
c d : WithTop α
x y val✝¹ val✝ : α
⊢ Option.some val✝¹ + Option.some val✝ = ⊤ ↔ Option.some val✝¹ = ⊤ ∨ Option.some val✝ = ⊤
[PROOFSTEP]
simp [none_eq_top, some_eq_coe, ← WithTop.coe_add]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Add α
a✝ b✝ c d : WithTop α
x y : α
inst✝ : LT α
a b : WithTop α
⊢ a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
[PROOFSTEP]
simp_rw [WithTop.lt_top_iff_ne_top, add_ne_top]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a b✝ c✝ d : WithTop α
x y : α
b : WithTop α
c : α
⊢ none + b = ↑c ↔ ∃ a' b', ↑a' = none ∧ ↑b' = b ∧ a' + b' = c
[PROOFSTEP]
simp [none_eq_top]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a✝ b c✝ d : WithTop α
x y a c : α
⊢ Option.some a + none = ↑c ↔ ∃ a' b', ↑a' = Option.some a ∧ ↑b' = none ∧ a' + b' = c
[PROOFSTEP]
simp [none_eq_top]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a✝ b✝ c✝ d : WithTop α
x y a b c : α
⊢ Option.some a + Option.some b = ↑c ↔ ∃ a' b', ↑a' = Option.some a ∧ ↑b' = Option.some b ∧ a' + b' = c
[PROOFSTEP]
simp only [some_eq_coe, ← coe_add, coe_eq_coe, exists_and_left, exists_eq_left]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x✝ y✝ : α
x : WithTop α
y : α
⊢ x + ↑y = ⊤ ↔ x = ⊤
[PROOFSTEP]
induction x using WithTop.recTopCoe
[GOAL]
case top
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y✝ y : α
⊢ ⊤ + ↑y = ⊤ ↔ ⊤ = ⊤
[PROOFSTEP]
simp [← coe_add]
[GOAL]
case coe
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y✝ y a✝ : α
⊢ ↑a✝ + ↑y = ⊤ ↔ ↑a✝ = ⊤
[PROOFSTEP]
simp [← coe_add]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y✝ : α
y : WithTop α
⊢ ↑x + y = ⊤ ↔ y = ⊤
[PROOFSTEP]
induction y using WithTop.recTopCoe
[GOAL]
case top
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y : α
⊢ ↑x + ⊤ = ⊤ ↔ ⊤ = ⊤
[PROOFSTEP]
simp [← coe_add]
[GOAL]
case coe
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y a✝ : α
⊢ ↑x + ↑a✝ = ⊤ ↔ ↑a✝ = ⊤
[PROOFSTEP]
simp [← coe_add]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Add α
a b c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
ha : a ≠ ⊤
⊢ b + a = c + a ↔ b = c
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : Add α
b c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
a : α
⊢ b + ↑a = c + ↑a ↔ b = c
[PROOFSTEP]
obtain rfl | hb := (eq_or_ne b ⊤)
[GOAL]
case intro.inl
α : Type u
β : Type v
inst✝¹ : Add α
c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
a : α
⊢ ⊤ + ↑a = c + ↑a ↔ ⊤ = c
[PROOFSTEP]
rw [top_add, eq_comm, WithTop.add_coe_eq_top_iff, eq_comm]
[GOAL]
case intro.inr
α : Type u
β : Type v
inst✝¹ : Add α
b c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
a : α
hb : b ≠ ⊤
⊢ b + ↑a = c + ↑a ↔ b = c
[PROOFSTEP]
lift b to α using hb
[GOAL]
case intro.inr.intro
α : Type u
β : Type v
inst✝¹ : Add α
c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
a b : α
⊢ ↑b + ↑a = c + ↑a ↔ ↑b = c
[PROOFSTEP]
simp_rw [← WithTop.coe_add, eq_comm, WithTop.add_eq_coe, coe_eq_coe, exists_and_left, exists_eq_left, add_left_inj,
  exists_eq_right, eq_comm]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Add α
a b c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
ha : a ≠ ⊤
⊢ a + b = a + c ↔ b = c
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : Add α
b c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
a : α
⊢ ↑a + b = ↑a + c ↔ b = c
[PROOFSTEP]
obtain rfl | hb := (eq_or_ne b ⊤)
[GOAL]
case intro.inl
α : Type u
β : Type v
inst✝¹ : Add α
c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
a : α
⊢ ↑a + ⊤ = ↑a + c ↔ ⊤ = c
[PROOFSTEP]
rw [add_top, eq_comm, WithTop.coe_add_eq_top_iff, eq_comm]
[GOAL]
case intro.inr
α : Type u
β : Type v
inst✝¹ : Add α
b c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
a : α
hb : b ≠ ⊤
⊢ ↑a + b = ↑a + c ↔ b = c
[PROOFSTEP]
lift b to α using hb
[GOAL]
case intro.inr.intro
α : Type u
β : Type v
inst✝¹ : Add α
c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
a b : α
⊢ ↑a + ↑b = ↑a + c ↔ ↑b = c
[PROOFSTEP]
simp_rw [← WithTop.coe_add, eq_comm, WithTop.add_eq_coe, eq_comm, coe_eq_coe, exists_and_left, exists_eq_left',
  add_right_inj, exists_eq_right']
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : WithTop α
h : b ≤ c
⊢ a + b ≤ a + c
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : WithTop α
h : b ≤ c
⊢ none + b ≤ none + c
[PROOFSTEP]
cases c
[GOAL]
case some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : WithTop α
h : b ≤ c
val✝ : α
⊢ Option.some val✝ + b ≤ Option.some val✝ + c
[PROOFSTEP]
cases c
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
h : b ≤ none
⊢ none + b ≤ none + none
[PROOFSTEP]
try exact le_top
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
h : b ≤ none
⊢ none + b ≤ none + none
[PROOFSTEP]
exact le_top
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ Option.some val✝
⊢ none + b ≤ none + Option.some val✝
[PROOFSTEP]
try exact le_top
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ Option.some val✝
⊢ none + b ≤ none + Option.some val✝
[PROOFSTEP]
exact le_top
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ none
⊢ Option.some val✝ + b ≤ Option.some val✝ + none
[PROOFSTEP]
try exact le_top
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ none
⊢ Option.some val✝ + b ≤ Option.some val✝ + none
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ Option.some val✝¹ + b ≤ Option.some val✝¹ + Option.some val✝
[PROOFSTEP]
try exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ Option.some val✝¹ + b ≤ Option.some val✝¹ + Option.some val✝
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ Option.some val✝¹ + b ≤ Option.some val✝¹ + Option.some val✝
[PROOFSTEP]
rcases le_coe_iff.1 h with ⟨b, rfl, _⟩
[GOAL]
case some.some.intro.intro
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
val✝¹ val✝ b : α
right✝ : b ≤ val✝
h : ↑b ≤ Option.some val✝
⊢ Option.some val✝¹ + ↑b ≤ Option.some val✝¹ + Option.some val✝
[PROOFSTEP]
exact coe_le_coe.2 (add_le_add_left (coe_le_coe.1 h) _)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : WithTop α
h : b ≤ c
⊢ swap (fun x x_1 => x + x_1) a b ≤ swap (fun x x_1 => x + x_1) a c
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : WithTop α
h : b ≤ c
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none c
[PROOFSTEP]
cases c
[GOAL]
case some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : WithTop α
h : b ≤ c
val✝ : α
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝) c
[PROOFSTEP]
cases c
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
h : b ≤ none
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none none
[PROOFSTEP]
try exact le_top
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
h : b ≤ none
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none none
[PROOFSTEP]
exact le_top
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none (Option.some val✝)
[PROOFSTEP]
try exact le_top
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none (Option.some val✝)
[PROOFSTEP]
exact le_top
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ none
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝) none
[PROOFSTEP]
try exact le_top
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ none
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝) none
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝¹) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝)
[PROOFSTEP]
try exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝¹) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝)
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝¹) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝)
[PROOFSTEP]
rcases le_coe_iff.1 h with ⟨b, rfl, _⟩
[GOAL]
case some.some.intro.intro
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
val✝¹ val✝ b : α
right✝ : b ≤ val✝
h : ↑b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝¹) ↑b ≤
    swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝)
[PROOFSTEP]
exact coe_le_coe.2 (add_le_add_right (coe_le_coe.1 h) _)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b c : WithTop α
h : a + b < a + c
⊢ b < c
[PROOFSTEP]
induction a using WithTop.recTopCoe
[GOAL]
case top
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
b c : WithTop α
h : ⊤ + b < ⊤ + c
⊢ b < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case coe
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
b c : WithTop α
a✝ : α
h : ↑a✝ + b < ↑a✝ + c
⊢ b < c
[PROOFSTEP]
induction b using WithTop.recTopCoe
[GOAL]
case coe.top
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
a✝ : α
h : ↑a✝ + ⊤ < ↑a✝ + c
⊢ ⊤ < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
a✝¹ a✝ : α
h : ↑a✝¹ + ↑a✝ < ↑a✝¹ + c
⊢ ↑a✝ < c
[PROOFSTEP]
induction c using WithTop.recTopCoe
[GOAL]
case coe.coe.top
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a✝¹ a✝ : α
h : ↑a✝¹ + ↑a✝ < ↑a✝¹ + ⊤
⊢ ↑a✝ < ⊤
[PROOFSTEP]
exact coe_lt_top _
[GOAL]
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a✝² a✝¹ a✝ : α
h : ↑a✝² + ↑a✝¹ < ↑a✝² + ↑a✝
⊢ ↑a✝¹ < ↑a✝
[PROOFSTEP]
exact coe_lt_coe.2 (lt_of_add_lt_add_left <| coe_lt_coe.1 h)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b c : WithTop α
h : swap (fun x x_1 => x + x_1) a b < swap (fun x x_1 => x + x_1) a c
⊢ b < c
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
b c : WithTop α
h : swap (fun x x_1 => x + x_1) none b < swap (fun x x_1 => x + x_1) none c
⊢ b < c
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
b c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) (Option.some val✝) b < swap (fun x x_1 => x + x_1) (Option.some val✝) c
⊢ b < c
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
h : swap (fun x x_1 => x + x_1) none none < swap (fun x x_1 => x + x_1) none c
⊢ none < c
[PROOFSTEP]
try exact (not_none_lt _ h).elim
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
h : swap (fun x x_1 => x + x_1) none none < swap (fun x x_1 => x + x_1) none c
⊢ none < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) none (Option.some val✝) < swap (fun x x_1 => x + x_1) none c
⊢ Option.some val✝ < c
[PROOFSTEP]
try exact (not_none_lt _ h).elim
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) none (Option.some val✝) < swap (fun x x_1 => x + x_1) none c
⊢ Option.some val✝ < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) (Option.some val✝) none < swap (fun x x_1 => x + x_1) (Option.some val✝) c
⊢ none < c
[PROOFSTEP]
try exact (not_none_lt _ h).elim
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) (Option.some val✝) none < swap (fun x x_1 => x + x_1) (Option.some val✝) c
⊢ none < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝) < swap (fun x x_1 => x + x_1) (Option.some val✝¹) c
⊢ Option.some val✝ < c
[PROOFSTEP]
try exact (not_none_lt _ h).elim
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝) < swap (fun x x_1 => x + x_1) (Option.some val✝¹) c
⊢ Option.some val✝ < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝) < swap (fun x x_1 => x + x_1) (Option.some val✝¹) c
⊢ Option.some val✝ < c
[PROOFSTEP]
cases c
[GOAL]
case some.some.none
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝) <
    swap (fun x x_1 => x + x_1) (Option.some val✝¹) none
⊢ Option.some val✝ < none
[PROOFSTEP]
exact coe_lt_top _
[GOAL]
case some.some.some
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
val✝² val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝²) (Option.some val✝¹) <
    swap (fun x x_1 => x + x_1) (Option.some val✝²) (Option.some val✝)
⊢ Option.some val✝¹ < Option.some val✝
[PROOFSTEP]
exact coe_lt_coe.2 (lt_of_add_lt_add_right <| coe_lt_coe.1 h)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
ha : a ≠ ⊤
h : a + b ≤ a + c
⊢ b ≤ c
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : ↑a + b ≤ ↑a + c
⊢ b ≤ c
[PROOFSTEP]
induction c using WithTop.recTopCoe
[GOAL]
case intro.top
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : ↑a + b ≤ ↑a + ⊤
⊢ b ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case intro.coe
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a a✝ : α
h : ↑a + b ≤ ↑a + ↑a✝
⊢ b ≤ ↑a✝
[PROOFSTEP]
induction b using WithTop.recTopCoe
[GOAL]
case intro.coe.top
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a a✝ : α
h : ↑a + ⊤ ≤ ↑a + ↑a✝
⊢ ⊤ ≤ ↑a✝
[PROOFSTEP]
exact (not_top_le_coe _ h).elim
[GOAL]
case intro.coe.coe
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a a✝¹ a✝ : α
h : ↑a + ↑a✝ ≤ ↑a + ↑a✝¹
⊢ ↑a✝ ≤ ↑a✝¹
[PROOFSTEP]
simp only [← coe_add, coe_le_coe] at h ⊢
[GOAL]
case intro.coe.coe
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a a✝¹ a✝ : α
h : a + a✝ ≤ a + a✝¹
⊢ a✝ ≤ a✝¹
[PROOFSTEP]
exact le_of_add_le_add_left h
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
ha : a ≠ ⊤
h : b + a ≤ c + a
⊢ b ≤ c
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : b + ↑a ≤ c + ↑a
⊢ b ≤ c
[PROOFSTEP]
cases c
[GOAL]
case intro.none
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : b + ↑a ≤ none + ↑a
⊢ b ≤ none
[PROOFSTEP]
exact le_top
[GOAL]
case intro.some
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a val✝ : α
h : b + ↑a ≤ Option.some val✝ + ↑a
⊢ b ≤ Option.some val✝
[PROOFSTEP]
cases b
[GOAL]
case intro.some.none
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a val✝ : α
h : none + ↑a ≤ Option.some val✝ + ↑a
⊢ none ≤ Option.some val✝
[PROOFSTEP]
exact (not_top_le_coe _ h).elim
[GOAL]
case intro.some.some
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a val✝¹ val✝ : α
h : Option.some val✝ + ↑a ≤ Option.some val✝¹ + ↑a
⊢ Option.some val✝ ≤ Option.some val✝¹
[PROOFSTEP]
exact coe_le_coe.2 (le_of_add_le_add_right <| coe_le_coe.1 h)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
ha : a ≠ ⊤
h : b < c
⊢ a + b < a + c
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : b < c
a : α
⊢ ↑a + b < ↑a + c
[PROOFSTEP]
rcases lt_iff_exists_coe.1 h with ⟨b, rfl, h'⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
inst✝² : Add α
c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < c
⊢ ↑a + ↑b < ↑a + c
[PROOFSTEP]
cases c
[GOAL]
case intro.intro.intro.none
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < none
⊢ ↑a + ↑b < ↑a + none
[PROOFSTEP]
exact coe_lt_top _
[GOAL]
case intro.intro.intro.some
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b val✝ : α
h' h : ↑b < Option.some val✝
⊢ ↑a + ↑b < ↑a + Option.some val✝
[PROOFSTEP]
exact coe_lt_coe.2 (add_lt_add_left (coe_lt_coe.1 h) _)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
ha : a ≠ ⊤
h : b < c
⊢ b + a < c + a
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : b < c
a : α
⊢ b + ↑a < c + ↑a
[PROOFSTEP]
rcases lt_iff_exists_coe.1 h with ⟨b, rfl, h'⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
inst✝² : Add α
c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < c
⊢ ↑b + ↑a < c + ↑a
[PROOFSTEP]
cases c
[GOAL]
case intro.intro.intro.none
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < none
⊢ ↑b + ↑a < none + ↑a
[PROOFSTEP]
exact coe_lt_top _
[GOAL]
case intro.intro.intro.some
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b val✝ : α
h' h : ↑b < Option.some val✝
⊢ ↑b + ↑a < Option.some val✝ + ↑a
[PROOFSTEP]
exact coe_lt_coe.2 (add_lt_add_right (coe_lt_coe.1 h) _)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a b : WithTop α
⊢ map (↑f) (a + b) = map (↑f) a + map (↑f) b
[PROOFSTEP]
induction a using WithTop.recTopCoe
[GOAL]
case top
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
⊢ map (↑f) (⊤ + b) = map ↑f ⊤ + map (↑f) b
[PROOFSTEP]
exact (top_add _).symm
[GOAL]
case coe
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (↑f) (↑a✝ + b) = map ↑f ↑a✝ + map (↑f) b
[PROOFSTEP]
induction b using WithTop.recTopCoe
[GOAL]
case coe.top
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (↑f) (↑a✝ + ⊤) = map ↑f ↑a✝ + map ↑f ⊤
[PROOFSTEP]
exact (add_top _).symm
[GOAL]
case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (↑f) (↑a✝¹ + ↑a✝) = map ↑f ↑a✝¹ + map ↑f ↑a✝
[PROOFSTEP]
rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
[GOAL]
case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ↑f ↑(a✝¹ + a✝) = ↑(↑f (a✝¹ + a✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
src✝¹ : One (WithTop α) := one
src✝ : AddMonoid (WithTop α) := addMonoid
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp only
  -- Porting note: Had to add this...?
[GOAL]
α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
src✝¹ : One (WithTop α) := one
src✝ : AddMonoid (WithTop α) := addMonoid
⊢ ↑↑0 = 0
[PROOFSTEP]
rw [Nat.cast_zero, WithTop.coe_zero]
[GOAL]
α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
src✝¹ : One (WithTop α) := one
src✝ : AddMonoid (WithTop α) := addMonoid
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
simp only
  -- Porting note: Had to add this...?
[GOAL]
α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
src✝¹ : One (WithTop α) := one
src✝ : AddMonoid (WithTop α) := addMonoid
n : ℕ
⊢ ↑↑(n + 1) = ↑↑n + 1
[PROOFSTEP]
rw [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one]
[GOAL]
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
⊢ ∀ (a b : WithTop α), a ≤ b → ∀ (c : WithTop α), c + a ≤ c + b
[PROOFSTEP]
rintro a b h (_ | c)
[GOAL]
case none
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
a b : WithTop α
h : a ≤ b
⊢ none + a ≤ none + b
[PROOFSTEP]
simp [none_eq_top]
[GOAL]
case some
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
a b : WithTop α
h : a ≤ b
c : α
⊢ Option.some c + a ≤ Option.some c + b
[PROOFSTEP]
rcases b with (_ | b)
[GOAL]
case some.none
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
a : WithTop α
c : α
h : a ≤ none
⊢ Option.some c + a ≤ Option.some c + none
[PROOFSTEP]
simp [none_eq_top]
[GOAL]
case some.some
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
a : WithTop α
c b : α
h : a ≤ Option.some b
⊢ Option.some c + a ≤ Option.some c + Option.some b
[PROOFSTEP]
rcases le_coe_iff.1 h with ⟨a, rfl, _⟩
[GOAL]
case some.some.intro.intro
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
c b a : α
right✝ : a ≤ b
h : ↑a ≤ Option.some b
⊢ Option.some c + ↑a ≤ Option.some c + Option.some b
[PROOFSTEP]
simp only [some_eq_coe, ← coe_add, coe_le_coe] at h ⊢
[GOAL]
case some.some.intro.intro
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
c b a : α
right✝ h : a ≤ b
⊢ c + a ≤ c + b
[PROOFSTEP]
exact add_le_add_left h c
[GOAL]
α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a b : WithTop α
⊢ ⊤ ≤ ⊤ → ∃ c, ⊤ = ⊤ + c
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ b✝ : WithTop α
a b : α
h : ↑a ≤ ↑b
⊢ ∃ c, ↑b = ↑a + c
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le (WithTop.coe_le_coe.1 h)
[GOAL]
case intro
α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ b : WithTop α
a c : α
h : ↑a ≤ ↑(a + c)
⊢ ∃ c_1, ↑(a + c) = ↑a + c_1
[PROOFSTEP]
exact ⟨c, rfl⟩
[GOAL]
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ map (↑f) 1 = 1
[PROOFSTEP]
rw [WithTop.map_one, map_one, coe_one]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a✝ b c d : WithBot α
x y : α
a : WithBot α
⊢ a + ⊥ = ⊥
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithBot α
x y : α
⊢ none + ⊥ = ⊥
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithBot α
x y val✝ : α
⊢ Option.some val✝ + ⊥ = ⊥
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithBot α
x y : α
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ map (↑f) 1 = 1
[PROOFSTEP]
rw [WithBot.map_one, map_one, coe_one]


[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ CovariantClass (WithZero α) (WithZero α) (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
[PROOFSTEP]
refine ⟨fun a b c hbc => ?_⟩
[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : WithZero α
hbc : b ≤ c
⊢ a * b ≤ a * c
[PROOFSTEP]
induction a using WithZero.recZeroCoe
[GOAL]
case h₁
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
b c : WithZero α
hbc : b ≤ c
⊢ 0 * b ≤ 0 * c
[PROOFSTEP]
exact zero_le _
[GOAL]
case h₂
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ * b ≤ ↑a✝ * c
[PROOFSTEP]
induction b using WithZero.recZeroCoe
[GOAL]
case h₂.h₁
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ * 0 ≤ ↑a✝ * c
[PROOFSTEP]
exact zero_le _
[GOAL]
case h₂.h₂
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑a✝¹ * c
[PROOFSTEP]
rcases WithBot.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑a✝¹ * ↑c
[PROOFSTEP]
refine
  le_trans ?_
    (le_of_eq <| coe_mul)
      -- rw [← coe_mul, ← coe_mul, coe_le_coe]
        -- Porting note: rewriting `coe_mul` here doesn't work because of some difference between
        -- `coe` and `WithBot.some`, even though they're definitionally equal as shown by the `refine'`
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑(a✝¹ * c)
[PROOFSTEP]
rw [← coe_mul, coe_le_coe]
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ a✝¹ * a✝ ≤ a✝¹ * c
[PROOFSTEP]
exact mul_le_mul_left' hbc' _
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ ↑a ≤ max ↑b ↑c ↔ a ≤ max b c
[PROOFSTEP]
simp only [WithZero.coe_le_coe, le_max_iff]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min ↑a ↑b ≤ ↑c ↔ min a b ≤ c
[PROOFSTEP]
simp only [WithZero.coe_le_coe, min_le_iff]
[GOAL]
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
⊢ CovariantClass (WithZero α) (WithZero α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
[PROOFSTEP]
refine ⟨fun a b c hbc => ?_⟩
[GOAL]
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a b c : WithZero α
hbc : b ≤ c
⊢ a + b ≤ a + c
[PROOFSTEP]
induction a using WithZero.recZeroCoe
[GOAL]
case h₁
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
⊢ 0 + b ≤ 0 + c
[PROOFSTEP]
rwa [zero_add, zero_add]
[GOAL]
case h₂
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ + b ≤ ↑a✝ + c
[PROOFSTEP]
induction b using WithZero.recZeroCoe
[GOAL]
case h₂.h₁
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ + 0 ≤ ↑a✝ + c
[PROOFSTEP]
rw [add_zero]
[GOAL]
case h₂.h₁
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ ≤ ↑a✝ + c
[PROOFSTEP]
induction c using WithZero.recZeroCoe
[GOAL]
case h₂.h₁.h₁
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝ : α
hbc : 0 ≤ 0
⊢ ↑a✝ ≤ ↑a✝ + 0
[PROOFSTEP]
rw [add_zero]
[GOAL]
case h₂.h₁.h₂
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ ↑a✝¹ ≤ ↑a✝¹ + ↑a✝
[PROOFSTEP]
rw [← coe_add, coe_le_coe]
[GOAL]
case h₂.h₁.h₂
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ a✝¹ ≤ a✝¹ + a✝
[PROOFSTEP]
exact le_add_of_nonneg_right (h _)
[GOAL]
case h₂.h₂
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + c
[PROOFSTEP]
rcases WithBot.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + ↑c
[PROOFSTEP]
refine le_trans ?_ (le_of_eq <| coe_add _ _)
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑(a✝¹ + c)
[PROOFSTEP]
rw [← coe_add, coe_le_coe]
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ a✝¹ + a✝ ≤ a✝¹ + c
[PROOFSTEP]
exact add_le_add_left hbc' _
[GOAL]
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a b : WithZero α
⊢ a ≤ b → ∃ c, b = a + c
[PROOFSTEP]
induction a using WithZero.cases_on
[GOAL]
case a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
b : WithZero α
⊢ 0 ≤ b → ∃ c, b = 0 + c
[PROOFSTEP]
exact fun _ => ⟨b, (zero_add b).symm⟩
[GOAL]
case a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
b : WithZero α
a✝ : α
⊢ ↑a✝ ≤ b → ∃ c, b = ↑a✝ + c
[PROOFSTEP]
induction b using WithZero.cases_on
[GOAL]
case a.a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a✝ : α
⊢ ↑a✝ ≤ 0 → ∃ c, 0 = ↑a✝ + c
[PROOFSTEP]
exact fun h => (WithBot.not_coe_le_bot _ h).elim
[GOAL]
case a.a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ∃ c, ↑a✝ = ↑a✝¹ + c
[PROOFSTEP]
intro h
[GOAL]
case a.a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a✝¹ a✝ : α
h : ↑a✝¹ ≤ ↑a✝
⊢ ∃ c, ↑a✝ = ↑a✝¹ + c
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le (WithZero.coe_le_coe.1 h)
[GOAL]
case a.a.intro
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a✝ c : α
h : ↑a✝ ≤ ↑(a✝ + c)
⊢ ∃ c_1, ↑(a✝ + c) = ↑a✝ + c_1
[PROOFSTEP]
exact ⟨c, rfl⟩
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
a b : WithZero α
⊢ a ≤ a + b
[PROOFSTEP]
induction a using WithZero.cases_on
[GOAL]
case a
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
b : WithZero α
⊢ 0 ≤ 0 + b
[PROOFSTEP]
exact bot_le
[GOAL]
case a
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
b : WithZero α
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + b
[PROOFSTEP]
induction b using WithZero.cases_on
[GOAL]
case a.a
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + 0
[PROOFSTEP]
exact le_rfl
[GOAL]
case a.a
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝¹ + ↑a✝
[PROOFSTEP]
exact WithZero.coe_le_coe.2 le_self_add


[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ ContravariantClass (WithZero α) (WithZero α) (fun x x_1 => x * x_1) fun x x_1 => x < x_1
[PROOFSTEP]
refine ⟨fun a b c h => ?_⟩
[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : WithZero α
h : a * b < a * c
⊢ b < c
[PROOFSTEP]
have := ((zero_le _).trans_lt h).ne'
[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : WithZero α
h : a * b < a * c
this : a * c ≠ 0
⊢ b < c
[PROOFSTEP]
induction a using WithZero.recZeroCoe
[GOAL]
case h₁
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b c : WithZero α
h : 0 * b < 0 * c
this : 0 * c ≠ 0
⊢ b < c
[PROOFSTEP]
exfalso
[GOAL]
case h₁.h
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b c : WithZero α
h : 0 * b < 0 * c
this : 0 * c ≠ 0
⊢ False
[PROOFSTEP]
exact left_ne_zero_of_mul this rfl
[GOAL]
case h₂
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b c : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * c
this : ↑a✝ * c ≠ 0
⊢ b < c
[PROOFSTEP]
induction c using WithZero.recZeroCoe
[GOAL]
case h₂.h₁
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * 0
this : ↑a✝ * 0 ≠ 0
⊢ b < 0
[PROOFSTEP]
exfalso
[GOAL]
case h₂.h₁.h
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * 0
this : ↑a✝ * 0 ≠ 0
⊢ False
[PROOFSTEP]
exact right_ne_zero_of_mul this rfl
[GOAL]
case h₂.h₂
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b : WithZero α
a✝¹ a✝ : α
h : ↑a✝¹ * b < ↑a✝¹ * ↑a✝
this : ↑a✝¹ * ↑a✝ ≠ 0
⊢ b < ↑a✝
[PROOFSTEP]
induction b using WithZero.recZeroCoe
[GOAL]
case h₂.h₂.h₁
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a✝¹ a✝ : α
this : ↑a✝¹ * ↑a✝ ≠ 0
h : ↑a✝¹ * 0 < ↑a✝¹ * ↑a✝
⊢ 0 < ↑a✝
case h₂.h₂.h₂
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a✝² a✝¹ : α
this : ↑a✝² * ↑a✝¹ ≠ 0
a✝ : α
h : ↑a✝² * ↑a✝ < ↑a✝² * ↑a✝¹
⊢ ↑a✝ < ↑a✝¹
[PROOFSTEP]
exacts [zero_lt_coe _, coe_lt_coe.mpr (lt_of_mul_lt_mul_left' <| coe_lt_coe.mp h)]


[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : Monoid R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : DistribMulAction R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
⊢ Function.Injective fun f => f.toFun
[PROOFSTEP]
rintro ⟨⟨⟨⟨f, _⟩, _⟩, _⟩, _⟩ ⟨⟨⟨⟨g, _⟩, _⟩, _⟩, _⟩ h
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : Monoid R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : DistribMulAction R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
f : A → B
map_smul'✝¹ : ∀ (m : R) (x : A), f (m • x) = m • f x
map_zero'✝¹ : MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } (x + y) =
      MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } x +
        MulActionHom.toFun { toFun := f, map_smul' := map_smul'✝¹ } y
map_mul'✝¹ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ }.toMulActionHom
          y
map_star'✝¹ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
                  map_add' := map_add'✝¹ },
              map_mul' := map_mul'✝¹ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
                    map_add' := map_add'✝¹ },
                map_mul' := map_mul'✝¹ }.toDistribMulActionHom.toMulActionHom
          a)
g : A → B
map_smul'✝ : ∀ (m : R) (x : A), g (m • x) = m • g x
map_zero'✝ : MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } 0 = 0
map_add'✝ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } (x + y) =
      MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } x +
        MulActionHom.toFun { toFun := g, map_smul' := map_smul'✝ } y
map_mul'✝ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
            map_add' := map_add'✝ }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ }.toMulActionHom
          y
map_star'✝ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
                  map_add' := map_add'✝ },
              map_mul' := map_mul'✝ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
                    map_add' := map_add'✝ },
                map_mul' := map_mul'✝ }.toDistribMulActionHom.toMulActionHom
          a)
h :
  (fun f => f.toFun)
      {
        toNonUnitalAlgHom :=
          {
            toDistribMulActionHom :=
              { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
                map_add' := map_add'✝¹ },
            map_mul' := map_mul'✝¹ },
        map_star' := map_star'✝¹ } =
    (fun f => f.toFun)
      {
        toNonUnitalAlgHom :=
          {
            toDistribMulActionHom :=
              { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
                map_add' := map_add'✝ },
            map_mul' := map_mul'✝ },
        map_star' := map_star'✝ }
⊢ {
      toNonUnitalAlgHom :=
        {
          toDistribMulActionHom :=
            { toMulActionHom := { toFun := f, map_smul' := map_smul'✝¹ }, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹ },
          map_mul' := map_mul'✝¹ },
      map_star' := map_star'✝¹ } =
    {
      toNonUnitalAlgHom :=
        {
          toDistribMulActionHom :=
            { toMulActionHom := { toFun := g, map_smul' := map_smul'✝ }, map_zero' := map_zero'✝,
              map_add' := map_add'✝ },
          map_mul' := map_mul'✝ },
      map_star' := map_star'✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : Monoid R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : DistribMulAction R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
f : A →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
h₅ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
                map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
          a)
⊢ {
      toNonUnitalAlgHom :=
        {
          toDistribMulActionHom :=
            { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
          map_mul' := h₄ },
      map_star' := h₅ } =
    f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : Monoid R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : DistribMulAction R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
f : A →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
h₅ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
                map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
          a)
x✝ : A
⊢ ↑{
          toNonUnitalAlgHom :=
            {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ },
          map_star' := h₅ }
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : Monoid R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : DistribMulAction R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
f : B →⋆ₙₐ[R] C
g : A →⋆ₙₐ[R] B
src✝ : A →ₙₐ[R] C := NonUnitalAlgHom.comp f.toNonUnitalAlgHom g.toNonUnitalAlgHom
⊢ ∀ (a : A),
    MulActionHom.toFun
        { toDistribMulActionHom := src✝.toDistribMulActionHom,
              map_mul' :=
                (_ :
                  ∀ (x y : A),
                    MulActionHom.toFun src✝.toMulActionHom (x * y) =
                      MulActionHom.toFun src✝.toMulActionHom x *
                        MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          { toDistribMulActionHom := src✝.toDistribMulActionHom,
                map_mul' :=
                  (_ :
                    ∀ (x y : A),
                      MulActionHom.toFun src✝.toMulActionHom (x * y) =
                        MulActionHom.toFun src✝.toMulActionHom x *
                          MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
          a)
[PROOFSTEP]
simp only [map_star, NonUnitalAlgHom.toFun_eq_coe, eq_self_iff_true, NonUnitalAlgHom.coe_comp, coe_toNonUnitalAlgHom,
  Function.comp_apply, forall_const]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : StarAddMonoid A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : DistribMulAction R B
inst✝ : StarAddMonoid B
src✝ : A →ₙₐ[R] B := 0
⊢ ∀ (a : A),
    MulActionHom.toFun
        { toDistribMulActionHom := src✝.toDistribMulActionHom,
              map_mul' :=
                (_ :
                  ∀ (x y : A),
                    MulActionHom.toFun src✝.toMulActionHom (x * y) =
                      MulActionHom.toFun src✝.toMulActionHom x *
                        MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          { toDistribMulActionHom := src✝.toDistribMulActionHom,
                map_mul' :=
                  (_ :
                    ∀ (x y : A),
                      MulActionHom.toFun src✝.toMulActionHom (x * y) =
                        MulActionHom.toFun src✝.toMulActionHom x *
                          MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
          a)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
⊢ Function.Injective fun f => f.toFun
[PROOFSTEP]
rintro ⟨⟨⟨⟨⟨f, _⟩, _⟩, _⟩, _⟩, _⟩ ⟨⟨⟨⟨⟨g, _⟩, _⟩, _⟩, _⟩, _⟩ h
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : A → B
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } x * OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } y
map_zero'✝¹ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) y
commutes'✝¹ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
map_star'✝¹ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
                    map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
                commutes' := commutes'✝¹ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
                      map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
                  commutes' := commutes'✝¹ })
          x)
g : A → B
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    OneHom.toFun { toFun := g, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := g, map_one' := map_one'✝ } x * OneHom.toFun { toFun := g, map_one' := map_one'✝ } y
map_zero'✝ : OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) 0 = 0
map_add'✝ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) y
commutes'✝ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
map_star'✝ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
                    map_zero' := map_zero'✝, map_add' := map_add'✝ },
                commutes' := commutes'✝ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
                      map_zero' := map_zero'✝, map_add' := map_add'✝ },
                  commutes' := commutes'✝ })
          x)
h :
  (fun f => f.toFun)
      {
        toAlgHom :=
          {
            toRingHom :=
              { toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
                map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
            commutes' := commutes'✝¹ },
        map_star' := map_star'✝¹ } =
    (fun f => f.toFun)
      {
        toAlgHom :=
          {
            toRingHom :=
              { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
                map_zero' := map_zero'✝, map_add' := map_add'✝ },
            commutes' := commutes'✝ },
        map_star' := map_star'✝ }
⊢ {
      toAlgHom :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
          commutes' := commutes'✝¹ },
      map_star' := map_star'✝¹ } =
    {
      toAlgHom :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ },
          commutes' := commutes'✝ },
      map_star' := map_star'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : A →⋆ₐ[R] B
h₁ : ↑f 1 = 1
h₂ :
  ∀ (x y : A),
    OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x * y) =
      OneHom.toFun { toFun := ↑f, map_one' := h₁ } x * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y
h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0
h₄ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y
h₅ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
h₆ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                    map_add' := h₄ },
                commutes' := h₅ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                      map_add' := h₄ },
                  commutes' := h₅ })
          x)
⊢ {
      toAlgHom :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ },
          commutes' := h₅ },
      map_star' := h₆ } =
    f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : A →⋆ₐ[R] B
h₁ : ↑f 1 = 1
h₂ :
  ∀ (x y : A),
    OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x * y) =
      OneHom.toFun { toFun := ↑f, map_one' := h₁ } x * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y
h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0
h₄ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y
h₅ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
h₆ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                    map_add' := h₄ },
                commutes' := h₅ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                      map_add' := h₄ },
                  commutes' := h₅ })
          x)
x✝ : A
⊢ ↑{
          toAlgHom :=
            {
              toRingHom :=
                { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                  map_add' := h₄ },
              commutes' := h₅ },
          map_star' := h₆ }
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : B →⋆ₐ[R] C
g : A →⋆ₐ[R] B
src✝ : A →ₐ[R] C := AlgHom.comp f.toAlgHom g.toAlgHom
⊢ ∀ (x : A),
    OneHom.toFun
        (↑↑↑{ toRingHom := ↑src✝,
                commutes' := (_ : ∀ (r : R), OneHom.toFun (↑↑↑src✝) (↑(algebraMap R A) r) = ↑(algebraMap R C) r) })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{ toRingHom := ↑src✝,
                  commutes' := (_ : ∀ (r : R), OneHom.toFun (↑↑↑src✝) (↑(algebraMap R A) r) = ↑(algebraMap R C) r) })
          x)
[PROOFSTEP]
simp only [map_star, AlgHom.toFun_eq_coe, AlgHom.coe_comp, coe_toAlgHom, Function.comp_apply, eq_self_iff_true,
  forall_const]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
src✝ : A →ₙₐ[R] B × C := NonUnitalAlgHom.prod f.toNonUnitalAlgHom g.toNonUnitalAlgHom
x : A
⊢ MulActionHom.toFun
      { toDistribMulActionHom := src✝.toDistribMulActionHom,
            map_mul' :=
              (_ :
                ∀ (x y : A),
                  MulActionHom.toFun src✝.toMulActionHom (x * y) =
                    MulActionHom.toFun src✝.toMulActionHom x *
                      MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
      (star x) =
    star
      (MulActionHom.toFun
        { toDistribMulActionHom := src✝.toDistribMulActionHom,
              map_mul' :=
                (_ :
                  ∀ (x y : A),
                    MulActionHom.toFun src✝.toMulActionHom (x * y) =
                      MulActionHom.toFun src✝.toMulActionHom x *
                        MulActionHom.toFun src✝.toMulActionHom y) }.toDistribMulActionHom.toMulActionHom
        x)
[PROOFSTEP]
simp [map_star, Prod.star_def]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ comp (fst R B C) (prod f g) = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ↑(comp (fst R B C) (prod f g)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ comp (snd R B C) (prod f g) = g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ↑(comp (snd R B C) (prod f g)) x✝ = ↑g x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)
⊢ (fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f) = f
[PROOFSTEP]
ext
[GOAL]
case h₁.h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).fst x✝ = ↑f.fst x✝
[PROOFSTEP]
rfl
[GOAL]
case h₂.h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).snd x✝ = ↑f.snd x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B × C
⊢ (fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f) = f
[PROOFSTEP]
ext
[GOAL]
case h.h₁
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).fst = (↑f x✝).fst
[PROOFSTEP]
rfl
[GOAL]
case h.h₂
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).snd = (↑f x✝).snd
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
src✝ : A →ₐ[R] B × C := AlgHom.prod f.toAlgHom g.toAlgHom
x : A
⊢ OneHom.toFun
      (↑↑↑{ toRingHom := ↑src✝,
              commutes' := (_ : ∀ (r : R), OneHom.toFun (↑↑↑src✝) (↑(algebraMap R A) r) = ↑(algebraMap R (B × C)) r) })
      (star x) =
    star
      (OneHom.toFun
        (↑↑↑{ toRingHom := ↑src✝,
                commutes' :=
                  (_ : ∀ (r : R), OneHom.toFun (↑↑↑src✝) (↑(algebraMap R A) r) = ↑(algebraMap R (B × C)) r) })
        x)
[PROOFSTEP]
simp [Prod.star_def, map_star]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ comp (fst R B C) (prod f g) = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ↑(comp (fst R B C) (prod f g)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ comp (snd R B C) (prod f g) = g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ↑(comp (snd R B C) (prod f g)) x✝ = ↑g x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)
⊢ (fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f) = f
[PROOFSTEP]
ext
[GOAL]
case h₁.h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).fst x✝ = ↑f.fst x✝
[PROOFSTEP]
rfl
[GOAL]
case h₂.h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)
x✝ : A
⊢ ↑((fun f => (comp (fst R B C) f, comp (snd R B C) f)) ((fun f => prod f.fst f.snd) f)).snd x✝ = ↑f.snd x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B × C
⊢ (fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f) = f
[PROOFSTEP]
ext
[GOAL]
case h.h₁
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).fst = (↑f x✝).fst
[PROOFSTEP]
rfl
[GOAL]
case h.h₂
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B × C
x✝ : A
⊢ (↑((fun f => prod f.fst f.snd) ((fun f => (comp (fst R B C) f, comp (snd R B C) f)) f)) x✝).snd = (↑f x✝).snd
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Star A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Star B
hF : StarAlgEquivClass F R A B
f : F
r : R
⊢ ↑f (↑(algebraMap R A) r) = ↑(algebraMap R B) r
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, map_smul, map_one]
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
f g : A ≃⋆ₐ[R] B
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
rcases f with ⟨⟨⟨_, _, _⟩, _⟩, _⟩
[GOAL]
case mk.mk.mk
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
g : A ≃⋆ₐ[R] B
toFun✝ : A → B
invFun✝ : B → A
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_star'✝ :
  ∀ (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
        (star a) =
      star
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a)
map_smul'✝ :
  ∀ (r : R) (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
        (r • a) =
      r •
        Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_star' := map_star'✝, map_smul' := map_smul'✝ } =
    (fun f => f.toFun) g
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_star' := map_star'✝, map_smul' := map_smul'✝ } =
    (fun f => f.invFun) g
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      map_star' := map_star'✝, map_smul' := map_smul'✝ } =
    g
[PROOFSTEP]
rcases g with ⟨⟨⟨_, _, _⟩, _⟩, _⟩
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
toFun✝¹ : A → B
invFun✝¹ : B → A
left_inv✝¹ : Function.LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
map_mul'✝¹ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_star'✝¹ :
  ∀ (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
        (star a) =
      star
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          a)
map_smul'✝¹ :
  ∀ (r : R) (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
        (r • a) =
      r •
        Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          a
toFun✝ : A → B
invFun✝ : B → A
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_star'✝ :
  ∀ (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
        (star a) =
      star
        (Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a)
map_smul'✝ :
  ∀ (r : R) (a : A),
    Equiv.toFun
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
        (r • a) =
      r •
        Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        map_star' := map_star'✝¹, map_smul' := map_smul'✝¹ } =
    (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_star' := map_star'✝, map_smul' := map_smul'✝ }
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        map_star' := map_star'✝¹, map_smul' := map_smul'✝¹ } =
    (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_star' := map_star'✝, map_smul' := map_smul'✝ }
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
          map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
      map_star' := map_star'✝¹, map_smul' := map_smul'✝¹ } =
    {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      map_star' := map_star'✝, map_smul' := map_smul'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
src✝ : B ≃+* A := RingEquiv.symm e.toRingEquiv
b : B
⊢ Equiv.toFun
      { toEquiv := src✝.toEquiv,
          map_mul' :=
            (_ :
              ∀ (x y : B), Equiv.toFun src✝.toEquiv (x * y) = Equiv.toFun src✝.toEquiv x * Equiv.toFun src✝.toEquiv y),
          map_add' :=
            (_ :
              ∀ (x y : B),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }.toEquiv
      (star b) =
    star
      (Equiv.toFun
        { toEquiv := src✝.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : B),
                  Equiv.toFun src✝.toEquiv (x * y) = Equiv.toFun src✝.toEquiv x * Equiv.toFun src✝.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : B),
                  Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }.toEquiv
        b)
[PROOFSTEP]
simpa only [apply_inv_apply, inv_apply_apply] using congr_arg (inv e) (map_star e (inv e b)).symm
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
src✝ : B ≃+* A := RingEquiv.symm e.toRingEquiv
r : R
b : B
⊢ Equiv.toFun
      { toEquiv := src✝.toEquiv,
          map_mul' :=
            (_ :
              ∀ (x y : B), Equiv.toFun src✝.toEquiv (x * y) = Equiv.toFun src✝.toEquiv x * Equiv.toFun src✝.toEquiv y),
          map_add' :=
            (_ :
              ∀ (x y : B),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }.toEquiv
      (r • b) =
    r •
      Equiv.toFun
        { toEquiv := src✝.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : B),
                  Equiv.toFun src✝.toEquiv (x * y) = Equiv.toFun src✝.toEquiv x * Equiv.toFun src✝.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : B),
                  Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }.toEquiv
        b
[PROOFSTEP]
simpa only [apply_inv_apply, inv_apply_apply] using congr_arg (inv e) (map_smul e r (inv e b)).symm
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
⊢ symm (symm e) = e
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
a✝ : A
⊢ ↑(symm (symm e)) a✝ = ↑e a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
src✝ : A ≃+* C := RingEquiv.trans e₁.toRingEquiv e₂.toRingEquiv
a : A
⊢ Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv (star a)) = star (Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv a))
[PROOFSTEP]
rw [e₁.map_star', e₂.map_star']
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
src✝ : A ≃+* C := RingEquiv.trans e₁.toRingEquiv e₂.toRingEquiv
r : R
a : A
⊢ Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv (r • a)) = r • Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv a)
[PROOFSTEP]
rw [e₁.map_smul', e₂.map_smul']


[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Group α
inst✝² : CommSemigroup β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b : α
⊢ ↑f a ≤ ↑f b * ↑f (a / b)
[PROOFSTEP]
simpa only [mul_comm, div_mul_cancel'] using map_mul_le_mul f (a / b) b
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Group α
inst✝² : AddCommSemigroup β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b : α
⊢ ↑f a ≤ ↑f b + ↑f (a / b)
[PROOFSTEP]
simpa only [add_comm, div_mul_cancel'] using map_mul_le_add f (a / b) b
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Group α
inst✝² : CommSemigroup β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b c : α
⊢ ↑f (a / c) ≤ ↑f (a / b) * ↑f (b / c)
[PROOFSTEP]
simpa only [div_mul_div_cancel'] using map_mul_le_mul f (a / b) (b / c)
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Group α
inst✝² : AddCommSemigroup β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b c : α
⊢ ↑f (a / c) ≤ ↑f (a / b) + ↑f (b / c)
[PROOFSTEP]
simpa only [div_mul_div_cancel'] using map_mul_le_add f (a / b) (b / c)
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x / y) ≤ ↑f x + ↑f y
[PROOFSTEP]
rw [div_eq_mul_inv, ← map_inv_eq_map f y]
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x * y⁻¹) ≤ ↑f x + ↑f y⁻¹
[PROOFSTEP]
exact map_mul_le_add _ _ _
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x / y) = ↑f (y / x)
[PROOFSTEP]
rw [← inv_div, map_inv_eq_map]
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f x ≤ ↑f y + ↑f (y / x)
[PROOFSTEP]
simpa only [add_comm, map_div_rev, div_mul_cancel'] using map_mul_le_add f (x / y) y
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ |↑f x - ↑f y| ≤ ↑f (x / y)
[PROOFSTEP]
rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f x ≤ ↑f y + ↑f (x / y) ∧ ↑f y ≤ ↑f x + ↑f (x / y)
[PROOFSTEP]
exact ⟨le_map_add_map_div _ _ _, le_map_add_map_div' _ _ _⟩
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
src✝ : GroupSeminormClass F α β := inst✝
f : F
a : α
⊢ 0 ≤ 2 • ↑f a
[PROOFSTEP]
rw [two_nsmul, ← map_one_eq_zero f, ← div_self' a]
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
src✝ : GroupSeminormClass F α β := inst✝
f : F
a : α
⊢ ↑f (a / a) ≤ ↑f a + ↑f a
[PROOFSTEP]
exact map_div_le_add _ _ _
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupNormClass F α β
f : F
x : α
⊢ x = 1 → ↑f x = 0
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupNormClass F α β
f : F
⊢ ↑f 1 = 0
[PROOFSTEP]
exact map_one_eq_zero _


[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
h : 0 = 1
⊢ False
[PROOFSTEP]
simpa [← h, C.pos_iff] using C.one_pos
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
⊢ 0 ≤ 1
[PROOFSTEP]
change C.nonneg (1 - 0)
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
⊢ AddCommGroup.PositiveCone.nonneg C.toPositiveCone (1 - 0)
[PROOFSTEP]
convert C.one_nonneg
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
⊢ 1 - 0 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ 0 < x * y
[PROOFSTEP]
change
  C.pos
    (x * y - 0)
      -- porting note: used to be convert, but it relied on unfolding definitions
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ AddCommGroup.PositiveCone.pos C.toPositiveCone (x * y - 0)
[PROOFSTEP]
rw [sub_zero]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ AddCommGroup.PositiveCone.pos C.toPositiveCone (x * y)
[PROOFSTEP]
exact C.mul_pos x y (by rwa [← sub_zero x]) (by rwa [← sub_zero y])
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ AddCommGroup.PositiveCone.pos C.toPositiveCone x
[PROOFSTEP]
rwa [← sub_zero x]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ AddCommGroup.PositiveCone.pos C.toPositiveCone y
[PROOFSTEP]
rwa [← sub_zero y]