[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C (↑(of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
⊢ C x
[PROOFSTEP]
apply DFinsupp.induction x H_zero
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C (↑(of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
⊢ ∀ (i : ι) (b : (fun i => β i) i) (f : Π₀ (i : ι), (fun i => β i) i),
    ↑f i = 0 → b ≠ 0 → C f → C (DFinsupp.single i b + f)
[PROOFSTEP]
intro i b f h1 h2 ih
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C (↑(of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
i : ι
b : β i
f : Π₀ (i : ι), (fun i => β i) i
h1 : ↑f i = 0
h2 : b ≠ 0
ih : C f
⊢ C (DFinsupp.single i b + f)
[PROOFSTEP]
solve_by_elim
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ↑ψ f = ↑(toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)) f
[PROOFSTEP]
congr
  -- Porting note: ext applies addHom_ext' here, which isn't what we want.
[GOAL]
case e_a
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ψ = toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)
[PROOFSTEP]
apply DFinsupp.addHom_ext'
[GOAL]
case e_a.H
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ∀ (x : ι),
    AddMonoidHom.comp ψ (DFinsupp.singleAddHom (fun i => (fun i => β i) i) x) =
      AddMonoidHom.comp (toAddMonoid fun i => AddMonoidHom.comp ψ (of β i))
        (DFinsupp.singleAddHom (fun i => (fun i => β i) i) x)
[PROOFSTEP]
simp [toAddMonoid, of]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ ↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) f
[PROOFSTEP]
rw [fromAddMonoid, toAddMonoid_of]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ ↑(↑AddMonoidHom.compHom (of β i)) f = AddMonoidHom.comp (of β i) f
[PROOFSTEP]
rfl
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
x : γ
⊢ ↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)
[PROOFSTEP]
rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]
[GOAL]
ι✝ : Type v
dec_ι : DecidableEq ι✝
β : ι✝ → Type w
inst✝³ : (i : ι✝) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type v
ι : optParam (Type u_1) PUnit
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
src✝ : (⨁ (i : ι), M) →+ M := toAddMonoid fun x => AddMonoidHom.id M
x : ⨁ (x : ι), M
⊢ ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) 0) = 0
[PROOFSTEP]
rw [AddMonoidHom.map_zero, AddMonoidHom.map_zero]
[GOAL]
ι✝ : Type v
dec_ι : DecidableEq ι✝
β : ι✝ → Type w
inst✝³ : (i : ι✝) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type v
ι : optParam (Type u_1) PUnit
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
src✝ : (⨁ (i : ι), M) →+ M := toAddMonoid fun x => AddMonoidHom.id M
x✝ : ⨁ (x : ι), M
p : ι
x : M
⊢ ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (↑(of (fun i => M) p) x)) =
    ↑(of (fun i => M) p) x
[PROOFSTEP]
rw [Unique.default_eq p, toAddMonoid_of]
[GOAL]
ι✝ : Type v
dec_ι : DecidableEq ι✝
β : ι✝ → Type w
inst✝³ : (i : ι✝) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type v
ι : optParam (Type u_1) PUnit
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
src✝ : (⨁ (i : ι), M) →+ M := toAddMonoid fun x => AddMonoidHom.id M
x✝ : ⨁ (x : ι), M
p : ι
x : M
⊢ ↑(of (fun x => M) p) (↑(AddMonoidHom.id M) x) = ↑(of (fun i => M) p) x
[PROOFSTEP]
rfl
[GOAL]
ι✝ : Type v
dec_ι : DecidableEq ι✝
β : ι✝ → Type w
inst✝³ : (i : ι✝) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type v
ι : optParam (Type u_1) PUnit
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
src✝ : (⨁ (i : ι), M) →+ M := toAddMonoid fun x => AddMonoidHom.id M
x✝ x y : ⨁ (i : ι), M
ihx : ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x
ihy : ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y
⊢ ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (x + y)) = x + y
[PROOFSTEP]
rw [AddMonoidHom.map_add, AddMonoidHom.map_add, ihx, ihy]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
κ : Type u_1
h : ι ≃ κ
f : ⨁ (i : ι), β i
k : κ
⊢ ↑(↑(equivCongrLeft h) f) k = ↑f (↑h.symm k)
[PROOFSTEP]
exact DFinsupp.comapDomain'_apply _ h.right_inv _ _
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : { x // x ∈ A i }
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)
[PROOFSTEP]
obtain rfl | h := Decidable.eq_or_ne i j
[GOAL]
case inl
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i : ι
x : { x // x ∈ A i }
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) i) = ↑(if i = i then x else 0)
[PROOFSTEP]
rw [DirectSum.of_eq_same, if_pos rfl]
[GOAL]
case inr
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : { x // x ∈ A i }
h : i ≠ j
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)
[PROOFSTEP]
rw [DirectSum.of_eq_of_ne _ _ _ _ h, if_neg h, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ iSup A = ⊤
[PROOFSTEP]
rw [AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom, AddMonoidHom.mrange_top_iff_surjective]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ Function.Surjective ↑(DFinsupp.sumAddHom fun i => AddSubmonoid.subtype (A i))
[PROOFSTEP]
exact Function.Bijective.surjective h


[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x y : WithOne α
⊢ OneHom.toFun
      { toFun := fun x => Option.casesOn x 1 ↑f,
        map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
      (1 * y) =
    OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        1 *
      OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        y
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x y : WithOne α
⊢ OneHom.toFun
      { toFun := fun x => Option.casesOn x 1 ↑f,
        map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
      y =
    OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        1 *
      OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        y
[PROOFSTEP]
exact (one_mul _).symm
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x✝ y : WithOne α
x : α
⊢ OneHom.toFun
      { toFun := fun x => Option.casesOn x 1 ↑f,
        map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
      (↑x * 1) =
    OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        ↑x *
      OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x✝ y : WithOne α
x : α
⊢ OneHom.toFun
      { toFun := fun x => Option.casesOn x 1 ↑f,
        map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
      ↑x =
    OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        ↑x *
      OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        1
[PROOFSTEP]
exact (mul_one _).symm
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
⊢ map (MulHom.id α) = MonoidHom.id (WithOne α)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
x : WithOne α
⊢ ↑(map (MulHom.id α)) x = ↑(MonoidHom.id (WithOne α)) x
[PROOFSTEP]
induction x using WithOne.cases_on
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
⊢ ↑(map (MulHom.id α)) 1 = ↑(MonoidHom.id (WithOne α)) 1
[PROOFSTEP]
rfl
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
a✝ : α
⊢ ↑(map (MulHom.id α)) ↑a✝ = ↑(MonoidHom.id (WithOne α)) ↑a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
x : WithOne α
⊢ ↑(map g) (↑(map f) x) = ↑(map (MulHom.comp g f)) x
[PROOFSTEP]
induction x using WithOne.cases_on
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
⊢ ↑(map g) (↑(map f) 1) = ↑(map (MulHom.comp g f)) 1
[PROOFSTEP]
rfl
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
a✝ : α
⊢ ↑(map g) (↑(map f) ↑a✝) = ↑(map (MulHom.comp g f)) ↑a✝
[PROOFSTEP]
rfl


[GOAL]
α : Type u
β : Type u_1
x y : ULift α
inst✝ : MulOneClass α
⊢ ∀ (x y : ULift α), ↑Equiv.ulift (x * y) = ↑Equiv.ulift x * ↑Equiv.ulift y
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : Type u_1
x y : ULift α
inst✝ : MulOneClass α
x✝ y✝ : ULift α
⊢ ↑Equiv.ulift (x✝ * y✝) = ↑Equiv.ulift x✝ * ↑Equiv.ulift y✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type u_1
x y : ULift α
inst✝ : MulZeroOneClass α
⊢ ∀ (a b : ULift α), ↑Equiv.ulift (a * b) = ↑Equiv.ulift a * ↑Equiv.ulift b
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : Type u_1
x y : ULift α
inst✝ : MulZeroOneClass α
a✝ b✝ : ULift α
⊢ ↑Equiv.ulift (a✝ * b✝) = ↑Equiv.ulift a✝ * ↑Equiv.ulift b✝
[PROOFSTEP]
rfl


[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : InvolutiveInv α
src✝ : Inv (WithOne α) := inv
a : WithOne α
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a
[PROOFSTEP]
simp_rw [inv_comp_inv, Option.map_id, id]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : InvolutiveInv α
src✝ : Inv (WithZero α) := inv
a : WithZero α
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a
[PROOFSTEP]
simp_rw [inv_comp_inv, Option.map_id, id]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : InvOneClass α
src✝¹ : One (WithZero α) := one
src✝ : Inv (WithZero α) := inv
⊢ ↑1⁻¹ = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : DivisionMonoid α
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : InvolutiveInv (WithZero α) := involutiveInv
a b✝ : WithZero α
b : α
x✝ : none * some b = 1
⊢ none⁻¹ = some b
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : DivisionMonoid α
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : InvolutiveInv (WithZero α) := involutiveInv
a✝ b : WithZero α
a : α
x✝ : some a * none = 1
⊢ (some a)⁻¹ = none
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Group α
src✝² : MonoidWithZero (WithZero α) := monoidWithZero
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : Nontrivial (WithZero α) := nontrivial
a : WithZero α
ha : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝ : Group α
src✝² : MonoidWithZero (WithZero α) := monoidWithZero
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : Nontrivial (WithZero α) := nontrivial
a : α
⊢ ↑a * (↑a)⁻¹ = 1
[PROOFSTEP]
norm_cast
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝ : Group α
src✝² : MonoidWithZero (WithZero α) := monoidWithZero
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : Nontrivial (WithZero α) := nontrivial
a : α
⊢ a * a⁻¹ = 1
[PROOFSTEP]
apply mul_right_inv
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
cases n with
| zero => show (((1 : ℕ) : α) : WithZero α) = 0 + 1; · rw [Nat.cast_one, coe_one, zero_add]
| succ n =>
  show (((n + 2 : ℕ) : α) : WithZero α) = ((n + 1 : ℕ) : α) + 1
  rw [Nat.cast_succ, coe_add, coe_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
cases n with
| zero => show (((1 : ℕ) : α) : WithZero α) = 0 + 1; · rw [Nat.cast_one, coe_one, zero_add]
| succ n =>
  show (((n + 2 : ℕ) : α) : WithZero α) = ((n + 1 : ℕ) : α) + 1
  rw [Nat.cast_succ, coe_add, coe_one]
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
⊢ NatCast.natCast (Nat.zero + 1) = NatCast.natCast Nat.zero + 1
[PROOFSTEP]

| zero => show (((1 : ℕ) : α) : WithZero α) = 0 + 1; · rw [Nat.cast_one, coe_one, zero_add]
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
⊢ NatCast.natCast (Nat.zero + 1) = NatCast.natCast Nat.zero + 1
[PROOFSTEP]
show (((1 : ℕ) : α) : WithZero α) = 0 + 1
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
⊢ ↑↑1 = 0 + 1
[PROOFSTEP]
rw [Nat.cast_one, coe_one, zero_add]
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ NatCast.natCast (Nat.succ n + 1) = NatCast.natCast (Nat.succ n) + 1
[PROOFSTEP]

| succ n =>
  show (((n + 2 : ℕ) : α) : WithZero α) = ((n + 1 : ℕ) : α) + 1
  rw [Nat.cast_succ, coe_add, coe_one]
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ NatCast.natCast (Nat.succ n + 1) = NatCast.natCast (Nat.succ n) + 1
[PROOFSTEP]
show (((n + 2 : ℕ) : α) : WithZero α) = ((n + 1 : ℕ) : α) + 1
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ ↑↑(n + 2) = ↑↑(n + 1) + 1
[PROOFSTEP]
rw [Nat.cast_succ, coe_add, coe_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : WithZero α
⊢ a * (b + c) = a * b + a * c
[PROOFSTEP]
cases' a with a
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
b c : WithZero α
⊢ none * (b + c) = none * b + none * c
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
b c : WithZero α
a : α
⊢ some a * (b + c) = some a * b + some a * c
[PROOFSTEP]
cases' b with b
[GOAL]
case some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c : WithZero α
a : α
⊢ some a * (none + c) = some a * none + some a * c
[PROOFSTEP]
cases' c with c
[GOAL]
case some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c : WithZero α
a b : α
⊢ some a * (some b + c) = some a * some b + some a * c
[PROOFSTEP]
cases' c with c
[GOAL]
case some.none.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a : α
⊢ some a * (none + none) = some a * none + some a * none
[PROOFSTEP]
try rfl
[GOAL]
case some.none.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a : α
⊢ some a * (none + none) = some a * none + some a * none
[PROOFSTEP]
rfl
[GOAL]
case some.none.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a c : α
⊢ some a * (none + some c) = some a * none + some a * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.none.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a c : α
⊢ some a * (none + some c) = some a * none + some a * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : α
⊢ some a * (some b + none) = some a * some b + some a * none
[PROOFSTEP]
try rfl
[GOAL]
case some.some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : α
⊢ some a * (some b + none) = some a * some b + some a * none
[PROOFSTEP]
rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : α
⊢ some a * (some b + some c) = some a * some b + some a * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : α
⊢ some a * (some b + some c) = some a * some b + some a * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : α
⊢ some a * (some b + some c) = some a * some b + some a * some c
[PROOFSTEP]
exact congr_arg some (left_distrib _ _ _)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : WithZero α
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
cases' c with c
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : WithZero α
⊢ (a + b) * none = a * none + b * none
[PROOFSTEP]
change (a + b) * 0 = a * 0 + b * 0
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : WithZero α
⊢ (a + b) * 0 = a * 0 + b * 0
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : WithZero α
c : α
⊢ (a + b) * some c = a * some c + b * some c
[PROOFSTEP]
cases' a with a
[GOAL]
case some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
b : WithZero α
c : α
⊢ (none + b) * some c = none * some c + b * some c
[PROOFSTEP]
cases' b with b
[GOAL]
case some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
b : WithZero α
c a : α
⊢ (some a + b) * some c = some a * some c + b * some c
[PROOFSTEP]
cases' b with b
[GOAL]
case some.none.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c : α
⊢ (none + none) * some c = none * some c + none * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.none.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c : α
⊢ (none + none) * some c = none * some c + none * some c
[PROOFSTEP]
rfl
[GOAL]
case some.none.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c b : α
⊢ (none + some b) * some c = none * some c + some b * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.none.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c b : α
⊢ (none + some b) * some c = none * some c + some b * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a : α
⊢ (some a + none) * some c = some a * some c + none * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a : α
⊢ (some a + none) * some c = some a * some c + none * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a b : α
⊢ (some a + some b) * some c = some a * some c + some b * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a b : α
⊢ (some a + some b) * some c = some a * some c + some b * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a b : α
⊢ (some a + some b) * some c = some a * some c + some b * some c
[PROOFSTEP]
exact congr_arg some (right_distrib _ _ _)


[GOAL]
α : Type u_1
inst✝ : DivisionRing α
src✝² : DivisionSemiring αᵐᵒᵖ := divisionSemiring α
src✝¹ : Ring αᵐᵒᵖ := ring α
src✝ : RatCast αᵐᵒᵖ := ratCast α
a : ℤ
b : ℕ
hb : b ≠ 0
h : Nat.coprime (Int.natAbs a) b
⊢ unop ↑(Rat.mk' a b) = unop (↑a * (↑b)⁻¹)
[PROOFSTEP]
rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
[GOAL]
α : Type ?u.3697
inst✝ : DivisionRing α
src✝² : Ring αᵃᵒᵖ := ring α
src✝¹ : GroupWithZero αᵃᵒᵖ := groupWithZero α
src✝ : RatCast αᵃᵒᵖ := ratCast α
a : ℤ
b : ℕ
hb : b ≠ 0
h : Nat.coprime (Int.natAbs a) b
⊢ unop ↑(Rat.mk' a b) = unop (↑a * (↑b)⁻¹)
[PROOFSTEP]
rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast, div_eq_mul_inv]


[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) = fun x_1 => x * y * x_1
[PROOFSTEP]
ext z
[GOAL]
case h
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) z = x * y * z
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 => x_1 * x) ∘ fun x => x * y) = fun x_1 => x_1 * (y * x)
[PROOFSTEP]
ext z
[GOAL]
case h
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x_1 * x) ∘ fun x => x * y) z = z * (y * x)
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 ↔ b = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 → b = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
b : M
h : 1 * b = 1
⊢ b = 1
[PROOFSTEP]
simpa using h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommSemigroup G
a b c d : G
⊢ a * b * (c * d) = a * c * (b * d)
[PROOFSTEP]
simp only [mul_left_comm, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * b * c = b * c * a
[PROOFSTEP]
simp only [mul_left_comm, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * (b * c) = b * (c * a)
[PROOFSTEP]
simp only [mul_left_comm, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : AddCommSemigroup M
inst✝ : One M
a b : M
⊢ bit1 (a + b) = bit1 a + bit0 b
[PROOFSTEP]
rw [add_comm, bit1_add, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝¹ : AddMonoid M
a b c : M
inst✝ : One M
⊢ bit1 0 = 1
[PROOFSTEP]
rw [bit1, bit0_zero, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : LeftCancelMonoid M
a b : M
⊢ a * b = a ↔ a * b = a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u
inst✝ : RightCancelMonoid M
a b : M
⊢ a * b = b ↔ a * b = 1 * b
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a b c x : G
⊢ x⁻¹ = 1 / x
[PROOFSTEP]
rw [div_eq_mul_inv, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a b c x y : G
⊢ x * (1 / y) = x / y
[PROOFSTEP]
rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a✝ b✝ c✝ a b c : G
⊢ a * b / c = a * (b / c)
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a✝ b✝ c✝ a b c : G
⊢ a * (b / c) = a * b / c
[PROOFSTEP]
simp only [mul_assoc, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvMonoid G
a✝ b✝ c a b : G
⊢ a / b = a * (1 / b)
[PROOFSTEP]
rw [div_eq_mul_inv, one_div]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivInvOneMonoid G
a : G
⊢ a / 1 = a
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : a * b = 1
⊢ b⁻¹ = a
[PROOFSTEP]
rw [← inv_eq_of_mul_eq_one_right h, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : b * a = 1
⊢ b = 1 / a
[PROOFSTEP]
rw [eq_inv_of_mul_eq_one_left h, one_div]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : a * b = 1
⊢ b = 1 / a
[PROOFSTEP]
rw [eq_inv_of_mul_eq_one_right h, one_div]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : a / b = 1
⊢ a * b⁻¹ = 1
[PROOFSTEP]
rwa [← div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ 1 / a * (1 / b) = 1 / (b * a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ a⁻¹ / b = (b * a)⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ (a / b)⁻¹ = b / a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ 1 / (a / b) = b / a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ 1 / (1 / a) = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
src✝ : DivInvMonoid α := toDivInvMonoid
⊢ 1⁻¹ = 1
[PROOFSTEP]
simpa only [one_div, inv_inv] using (inv_div (1 : α) 1).symm
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
h : 1 / a = 1 / b
⊢ a = b
[PROOFSTEP]
rw [← one_div_one_div a, h, one_div_one_div]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ a / (b / c) = a * c / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ a / b⁻¹ = a * b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionMonoid α
a b c : α
⊢ a / (b * c) = a / c / b
[PROOFSTEP]
simp only [mul_assoc, mul_inv_rev, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ (a / b)⁻¹ = a⁻¹ / b⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b = b⁻¹ * a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a⁻¹ * b = b / a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ (a * b)⁻¹ = a⁻¹ / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a⁻¹ / b⁻¹ = b / a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ (a⁻¹ / b⁻¹)⁻¹ = a / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ 1 / a * (1 / b) = 1 / (a * b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / c = a / c / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / c = a / (b * c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * c = a / (b / c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a * (b / c) = b * (a / c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a * b / c = a / c * b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / (b * c) = a / b / c
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * c = a * c / b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * c = a * (c / b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * c = c / b * a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / (b * c) = a / b * (1 / c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a * d / (b * c)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a / c / (b / d)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * (c / d) = a * c / (b * d)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a * b / (c * d) = a / c * (b / d)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a / b = b⁻¹ ↔ a = 1
[PROOFSTEP]
rw [div_eq_mul_inv, mul_left_eq_self]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * c = b
⊢ a = b * c⁻¹
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b * a = c
⊢ a = b⁻¹ * c
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b = a * c
⊢ a⁻¹ * b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c * b
⊢ a * b⁻¹ = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * c⁻¹ = b
⊢ a = b * c
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b⁻¹ * a = c
⊢ a = b * c
[PROOFSTEP]
simp [h.symm, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b = a⁻¹ * c
⊢ a * b = c
[PROOFSTEP]
rw [h, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c * b⁻¹
⊢ a * b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = b⁻¹
⊢ a * b = 1
[PROOFSTEP]
rw [h, mul_left_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a * b = 1 ↔ a⁻¹ = b
[PROOFSTEP]
rw [mul_eq_one_iff_eq_inv, inv_eq_iff_eq_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = b * c⁻¹
⊢ a * c = b
[PROOFSTEP]
rw [h, inv_mul_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * c = b
⊢ a = b * c⁻¹
[PROOFSTEP]
rw [← h, mul_inv_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = b⁻¹ * c
⊢ b * a = c
[PROOFSTEP]
rw [h, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b * a = c
⊢ a = b⁻¹ * c
[PROOFSTEP]
rw [← h, inv_mul_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a⁻¹ * b = c
⊢ b = a * c
[PROOFSTEP]
rw [← h, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : b = a * c
⊢ a⁻¹ * b = c
[PROOFSTEP]
rw [h, inv_mul_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * b⁻¹ = c
⊢ a = c * b
[PROOFSTEP]
rw [← h, inv_mul_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c * b
⊢ a * b⁻¹ = c
[PROOFSTEP]
rw [h, mul_inv_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a * b⁻¹ = 1 ↔ a = b
[PROOFSTEP]
rw [mul_eq_one_iff_eq_inv, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a⁻¹ * b = 1 ↔ a = b
[PROOFSTEP]
rw [mul_eq_one_iff_eq_inv, inv_inj]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ Injective fun a => a / b
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ Injective fun a => a * b⁻¹
[PROOFSTEP]
exact fun a a' h ↦ mul_left_injective b⁻¹ h
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ Injective fun a => b / a
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ Injective fun a => b * a⁻¹
[PROOFSTEP]
exact fun a a' h ↦ inv_injective (mul_right_injective b h)
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c d a b : G
⊢ a / b * b = a
[PROOFSTEP]
rw [div_eq_mul_inv, inv_mul_cancel_right a b]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b c d a : G
⊢ a / a = 1
[PROOFSTEP]
rw [div_eq_mul_inv, mul_right_inv a]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c d a b : G
⊢ a * b / b = a
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_cancel_right a b]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c d a b : G
⊢ a / (b * a) = b⁻¹
[PROOFSTEP]
rw [← inv_div, mul_div_cancel'']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a * c / (b * c) = a / b
[PROOFSTEP]
rw [div_mul_eq_div_div_swap]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a * c / c / b = a / b
[PROOFSTEP]
simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel'']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a * c = b
⊢ a = b / c
[PROOFSTEP]
simp [← h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c * b
⊢ a / b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a / c = b
⊢ a = b * c
[PROOFSTEP]
simp [← h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = c / b
⊢ a * b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ b / a = c / a ↔ b = c
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ b * a⁻¹ = c * a⁻¹ ↔ b = c
[PROOFSTEP]
exact mul_left_inj _
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a / b * (b / c) = a / c
[PROOFSTEP]
rw [← mul_div_assoc, div_mul_cancel']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a / c / (b / c) = a / b
[PROOFSTEP]
rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
h : a = b
⊢ a / b = 1
[PROOFSTEP]
rw [h, div_self']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a / b = a ↔ b = 1
[PROOFSTEP]
rw [div_eq_mul_inv, mul_right_eq_self, inv_eq_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a = b / c ↔ a * c = b
[PROOFSTEP]
rw [div_eq_mul_inv, eq_mul_inv_iff_mul_eq]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
⊢ a / b = c ↔ a = c * b
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
H : a / b = c / d
⊢ a = b ↔ c = d
[PROOFSTEP]
rw [← div_eq_one, H, div_eq_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d : G
n : ℤ
hn : n ≠ 0
x : G
h : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ Int.ofNat n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
simp only [Int.ofNat_eq_coe] at h
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ ↑n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
rw [zpow_ofNat] at h
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
refine' ⟨n, Nat.pos_of_ne_zero fun n0 ↦ hn ?_, h⟩
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
n0 : n = 0
⊢ Int.ofNat n = 0
[PROOFSTEP]
rw [n0]
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
n0 : n = 0
⊢ Int.ofNat 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.negSucc n ≠ 0
h : x ^ Int.negSucc n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
rw [zpow_negSucc, inv_eq_one] at h
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.negSucc n ≠ 0
h : x ^ (n + 1) = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
refine' ⟨n + 1, n.succ_pos, h⟩
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
h : a = b * c
⊢ a / b = c
[PROOFSTEP]
rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ c * a / (c * b) = a / b
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_rev, mul_comm b⁻¹ c⁻¹, mul_comm c a, mul_assoc, ← mul_assoc c, mul_right_inv, one_mul,
  div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
h : c * a = b
⊢ a = b / c
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
h : a / b = c
⊢ a = b * c
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
h : b = c / a
⊢ a * b = c
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
h : b = c / a
⊢ a * (c * a⁻¹) = c
[PROOFSTEP]
rw [mul_comm c, mul_inv_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a / (a / b) = b
[PROOFSTEP]
simpa using mul_inv_cancel_left a b
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a / b = c / b * (a / c)
[PROOFSTEP]
simp [mul_left_comm c]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a / b / a = b⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a = b / c ↔ c * a = b
[PROOFSTEP]
rw [eq_div_iff_mul_eq', mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c ↔ a = b * c
[PROOFSTEP]
rw [div_eq_iff_eq_mul, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a * b / a = b
[PROOFSTEP]
rw [div_eq_inv_mul, inv_mul_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a * (b / a) = b
[PROOFSTEP]
rw [← mul_div_assoc, mul_div_cancel''']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a / (a * b) = b⁻¹
[PROOFSTEP]
rw [← inv_div, mul_div_cancel''']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c d a b : G
⊢ a * (b * a⁻¹) = b
[PROOFSTEP]
rw [← div_eq_mul_inv, mul_div_cancel'_right a b]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a * c * (b / c) = a * b
[PROOFSTEP]
rw [mul_assoc, mul_div_cancel'_right]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a / c * (b * c) = a * b
[PROOFSTEP]
rw [mul_left_comm, div_mul_cancel', mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a / b * (c / a) = c / b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ c / a * (a / b) = c / b
[PROOFSTEP]
apply div_mul_div_cancel'
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a * b / (a / c) = b * c
[PROOFSTEP]
rw [← div_mul, mul_div_cancel''']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ c / a / (c / b) = b / a
[PROOFSTEP]
rw [← inv_div b c, div_inv_eq_mul, mul_comm, div_mul_div_cancel']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b
[PROOFSTEP]
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ c * b = d * a ↔ a * d = c * b
[PROOFSTEP]
simp only [mul_comm, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a / c = b / d
[PROOFSTEP]
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, div_eq_iff_eq_mul', mul_div_assoc]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
⊢ f a c = f a b * f b c
[PROOFSTEP]
have hmul' : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c :=
  by
  intros b c rbc pab pbc pac
  obtain rab | rba := total_of r a b
  · exact hmul rab rbc pab pbc pac
  rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
  obtain rac | rca := total_of r a c
  · rw [hmul rba rac (hsymm pab) pac pbc]
  · rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
⊢ ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
[PROOFSTEP]
intros b c rbc pab pbc pac
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
⊢ f a c = f a b * f b c
[PROOFSTEP]
obtain rab | rba := total_of r a b
[GOAL]
case inl
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rab : r a b
⊢ f a c = f a b * f b c
[PROOFSTEP]
exact hmul rab rbc pab pbc pac
[GOAL]
case inr
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a c = f a b * f b c
[PROOFSTEP]
rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
[GOAL]
case inr
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a b * (f b a * f a c) = f a b * f b c
[PROOFSTEP]
obtain rac | rca := total_of r a c
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rac : r a c
⊢ f a b * (f b a * f a c) = f a b * f b c
[PROOFSTEP]
rw [hmul rba rac (hsymm pab) pac pbc]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rca : r c a
⊢ f a b * (f b a * f a c) = f a b * f b c
[PROOFSTEP]
rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
⊢ f a c = f a b * f b c
[PROOFSTEP]
obtain rbc | rcb := total_of r b c
[GOAL]
case inl
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rbc : r b c
⊢ f a c = f a b * f b c
[PROOFSTEP]
exact hmul' rbc pab pbc pac
[GOAL]
case inr
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rcb : r c b
⊢ f a c = f a b * f b c
[PROOFSTEP]
rw [hmul' rcb pac (hsymm pbc) pab, mul_assoc, hf_swap (hsymm pbc), mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ f a c = f a b * f b c
[PROOFSTEP]
apply multiplicative_of_symmetric_of_isTotal (fun a b => p a ∧ p b) r f fun _ _ => And.symm
[GOAL]
case hf_swap
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ ∀ {a b : α}, p a ∧ p b → f a b * f b a = 1
[PROOFSTEP]
simp_rw [and_imp]
[GOAL]
case hf_swap
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ ∀ {a b : α}, p a → p b → f a b * f b a = 1
[PROOFSTEP]
exact @hswap
[GOAL]
case hmul
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ ∀ {a b c : α}, r a b → r b c → p a ∧ p b → p b ∧ p c → p a ∧ p c → f a c = f a b * f b c
[PROOFSTEP]
exact fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2
[GOAL]
case pab
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p a ∧ p b
case pbc
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p b ∧ p c
case pac
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : Monoid β
p✝ r : α → α → Prop
inst✝ : IsTotal α r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p a ∧ p c
[PROOFSTEP]
exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]


[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionRing K
a b : K
A : Type u_4
inst✝ : DivisionRing A
m : ℚ
⊢ m • 1 = ↑m
[PROOFSTEP]
rw [Rat.smul_def, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Semiring R
h : IsField R
src✝ : Semiring R := inst✝
a : R
ha : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
convert Classical.choose_spec (IsField.mul_inv_cancel h ha)
[GOAL]
case h.e'_2.h.e'_6
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Semiring R
h : IsField R
src✝ : Semiring R := inst✝
a : R
ha : a ≠ 0
⊢ a⁻¹ = choose (_ : ∃ b, a * b = 1)
[PROOFSTEP]
exact dif_neg ha
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
⊢ ∀ (x : R), x ≠ 0 → ∃! y, x * y = 1
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃! y, x * y = 1
[PROOFSTEP]
apply exists_unique_of_exists_of_unique
[GOAL]
case hex
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1
[PROOFSTEP]
exact hf.mul_inv_cancel hx
[GOAL]
case hunique
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂
[PROOFSTEP]
intro y z hxy hxz
[GOAL]
case hunique
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = z
[PROOFSTEP]
calc
  y = y * (x * z) := by rw [hxz, mul_one]
  _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
  _ = z := by rw [hxy, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = y * (x * z)
[PROOFSTEP]
rw [hxz, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y * (x * z) = x * y * z
[PROOFSTEP]
rw [← mul_assoc, hf.mul_comm y x]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ x * y * z = z
[PROOFSTEP]
rw [hxy, one_mul]


[GOAL]
F : Type u_1
M : Type u_2
N : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
a x y : M
inst✝ : MulHomClass F M N
h : SemiconjBy a x y
f : F
⊢ SemiconjBy (↑f a) (↑f x) (↑f y)
[PROOFSTEP]
simpa only [SemiconjBy, map_mul] using congr_arg f h
[GOAL]
F : Type u_1
M : Type u_2
N : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
a x y : M
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ↑f
h : SemiconjBy (↑f a) (↑f x) (↑f y)
⊢ ↑f (a * x) = ↑f (y * a)
[PROOFSTEP]
simpa only [SemiconjBy, map_mul] using h
[GOAL]
F : Type u_1
M : Type u_2
N : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
a x y : M
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ↑f
h : Commute (↑f x) (↑f y)
⊢ ↑f (x * y) = ↑f (y * x)
[PROOFSTEP]
simpa only [map_mul] using h.eq


[GOAL]
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ DivisionSemiring (ULift α)
[PROOFSTEP]
refine' down_injective.divisionSemiring down ..
[GOAL]
case refine'_1
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ 0.down = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ 1.down = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x y : ULift α), (x + y).down = x.down + y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x y : ULift α), (x * y).down = x.down * y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x : ULift α), x⁻¹.down = x.down⁻¹
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x y : ULift α), (x / y).down = x.down / y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x : ULift α) (n : ℕ), (n • x).down = n • x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x : ULift α) (n : ℕ), (x ^ n).down = x.down ^ n
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x : ULift α) (n : ℤ), (x ^ n).down = x.down ^ n
[PROOFSTEP]
intros
[GOAL]
case refine'_10
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (n : ℕ), (↑n).down = ↑n
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ 0.down = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ 1.down = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ y✝ : ULift α
⊢ (x✝ + y✝).down = x✝.down + y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ y✝ : ULift α
⊢ (x✝ * y✝).down = x✝.down * y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ : ULift α
⊢ x✝⁻¹.down = x✝.down⁻¹
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ y✝ : ULift α
⊢ (x✝ / y✝).down = x✝.down / y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ : ULift α
n✝ : ℕ
⊢ (n✝ • x✝).down = n✝ • x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_8
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ : ULift α
n✝ : ℕ
⊢ (x✝ ^ n✝).down = x✝.down ^ n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ : ULift α
n✝ : ℤ
⊢ (x✝ ^ n✝).down = x✝.down ^ n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
n✝ : ℕ
⊢ (↑n✝).down = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ DivisionRing (ULift α)
[PROOFSTEP]
refine' down_injective.divisionRing down ..
[GOAL]
case refine'_1
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ 0.down = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ 1.down = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x y : ULift α), (x + y).down = x.down + y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x y : ULift α), (x * y).down = x.down * y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α), (-x).down = -x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x y : ULift α), (x - y).down = x.down - y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α), x⁻¹.down = x.down⁻¹
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x y : ULift α), (x / y).down = x.down / y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℕ), (n • x).down = n • x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_10
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℤ), (n • x).down = n • x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_11
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℚ), (n • x).down = n • x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_12
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℕ), (x ^ n).down = x.down ^ n
[PROOFSTEP]
intros
[GOAL]
case refine'_13
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℤ), (x ^ n).down = x.down ^ n
[PROOFSTEP]
intros
[GOAL]
case refine'_14
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (n : ℕ), (↑n).down = ↑n
[PROOFSTEP]
intros
[GOAL]
case refine'_15
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (n : ℤ), (↑n).down = ↑n
[PROOFSTEP]
intros
[GOAL]
case refine'_16
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (n : ℚ), (↑n).down = ↑n
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ 0.down = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ 1.down = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ y✝ : ULift α
⊢ (x✝ + y✝).down = x✝.down + y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ y✝ : ULift α
⊢ (x✝ * y✝).down = x✝.down * y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
⊢ (-x✝).down = -x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ y✝ : ULift α
⊢ (x✝ - y✝).down = x✝.down - y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
⊢ x✝⁻¹.down = x✝.down⁻¹
[PROOFSTEP]
rfl
[GOAL]
case refine'_8
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ y✝ : ULift α
⊢ (x✝ / y✝).down = x✝.down / y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℕ
⊢ (n✝ • x✝).down = n✝ • x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℤ
⊢ (n✝ • x✝).down = n✝ • x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_11
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℚ
⊢ (n✝ • x✝).down = n✝ • x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_12
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℕ
⊢ (x✝ ^ n✝).down = x✝.down ^ n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_13
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℤ
⊢ (x✝ ^ n✝).down = x✝.down ^ n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_14
α : Type u
x y : ULift α
inst✝ : DivisionRing α
n✝ : ℕ
⊢ (↑n✝).down = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_15
α : Type u
x y : ULift α
inst✝ : DivisionRing α
n✝ : ℤ
⊢ (↑n✝).down = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_16
α : Type u
x y : ULift α
inst✝ : DivisionRing α
n✝ : ℚ
⊢ (↑n✝).down = ↑n✝
[PROOFSTEP]
rfl


[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1, b₁) * (1, b₂) = (1, b₁ * b₂)
[PROOFSTEP]
rw [mk_mul_mk, mul_one]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Mul M
inst✝ : Monoid N
a₁ a₂ : M
⊢ (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
[PROOFSTEP]
rw [mk_mul_mk, mul_one]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : SemigroupWithZero M
inst✝ : SemigroupWithZero N
⊢ ∀ (a : M × N), 0 * a = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : SemigroupWithZero M
inst✝ : SemigroupWithZero N
⊢ ∀ (a : M × N), a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ ∀ (a : M × N), 1 * a = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ ∀ (a : M × N), a * 1 = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : DivisionMonoid G
inst✝ : DivisionMonoid H
⊢ ∀ (x : G × H), x⁻¹⁻¹ = x
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : DivisionCommMonoid G
inst✝ : DivisionCommMonoid H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
[PROOFSTEP]
rw [mk_mul_mk, mul_comm g₁, mul_comm h₁]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : DivisionCommMonoid G
inst✝ : DivisionCommMonoid H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁)
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : LeftCancelMonoid M
inst✝ : LeftCancelMonoid N
⊢ ∀ (a : M × N), 1 * a = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : LeftCancelMonoid M
inst✝ : LeftCancelMonoid N
⊢ ∀ (a : M × N), a * 1 = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : RightCancelMonoid M
inst✝ : RightCancelMonoid N
⊢ ∀ (a : M × N), 1 * a = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : RightCancelMonoid M
inst✝ : RightCancelMonoid N
⊢ ∀ (a : M × N), a * 1 = a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : CancelMonoid M
inst✝ : CancelMonoid N
⊢ ∀ (a b c : M × N), a * b = c * b → a = c
[PROOFSTEP]
simp only [mul_left_inj, imp_self, forall_const]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
[PROOFSTEP]
rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : CancelCommMonoid M
inst✝ : CancelCommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
[PROOFSTEP]
rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
⊢ ∀ (a : M × N), 0 * a = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : MulZeroOneClass M
inst✝ : MulZeroOneClass N
⊢ ∀ (a : M × N), a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : MonoidWithZero M
inst✝ : MonoidWithZero N
⊢ ∀ (a : M × N), 0 * a = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : MonoidWithZero M
inst✝ : MonoidWithZero N
⊢ ∀ (a : M × N), a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
⊢ ∀ (a : M × N), 0 * a = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
⊢ ∀ (a : M × N), a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
[PROOFSTEP]
rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
f : M →ₙ* N × P
x : M
⊢ ↑(MulHom.prod (comp (fst N P) f) (comp (snd N P) f)) x = ↑f x
[PROOFSTEP]
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : CommSemigroup P
f✝ : M →ₙ* P
g✝ : N →ₙ* P
Q : Type u_8
inst✝ : CommSemigroup Q
h : P →ₙ* Q
f : M →ₙ* P
g : N →ₙ* P
x : M × N
⊢ ↑(comp h (coprod f g)) x = ↑(coprod (comp h f) (comp h g)) x
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M →* N × P
x : M
⊢ ↑(MonoidHom.prod (comp (fst N P) f) (comp (snd N P) f)) x = ↑f x
[PROOFSTEP]
simp only [prod_apply, coe_fst, coe_snd, comp_apply, Prod.mk.eta]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : M
⊢ ↑(comp (coprod f g) (inl M N)) x = ↑f x
[PROOFSTEP]
simp [coprod_apply]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : N
⊢ ↑(comp (coprod f g) (inr M N)) x = ↑g x
[PROOFSTEP]
simp [coprod_apply]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f✝ : M →* P
g : N →* P
f : M × N →* P
x : M × N
⊢ ↑(coprod (comp f (inl M N)) (comp f (inr M N))) x = ↑f x
[PROOFSTEP]
simp [coprod_apply, inl_apply, inr_apply, ← map_mul]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
f✝ : M →* P
g✝ : N →* P
Q : Type u_8
inst✝ : CommMonoid Q
h : P →* Q
f : M →* P
g : N →* P
x : M × N
⊢ ↑(comp h (coprod f g)) x = ↑(coprod (comp h f) (comp h g)) x
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
u : Mˣ × Nˣ
⊢ (↑u.fst, ↑u.snd) * (↑u.fst⁻¹, ↑u.snd⁻¹) = 1
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
u : Mˣ × Nˣ
⊢ (↑u.fst⁻¹, ↑u.snd⁻¹) * (↑u.fst, ↑u.snd) = 1
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
u : (M × N)ˣ
⊢ (fun u =>
        { val := (↑u.fst, ↑u.snd), inv := (↑u.fst⁻¹, ↑u.snd⁻¹),
          val_inv := (_ : (↑u.fst * ↑u.fst⁻¹, ↑u.snd * ↑u.snd⁻¹) = 1),
          inv_val := (_ : (↑u.fst⁻¹ * ↑u.fst, ↑u.snd⁻¹ * ↑u.snd) = 1) })
      (↑(MonoidHom.prod (Units.map (MonoidHom.fst M N)) (Units.map (MonoidHom.snd M N))) u) =
    u
[PROOFSTEP]
simp only [MonoidHom.prod_apply, Units.coe_map, MonoidHom.coe_fst, MonoidHom.coe_snd, Prod.mk.eta, Units.coe_map_inv,
  Units.mk_val]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : Mˣ × Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ ↑(MonoidHom.prod (Units.map (MonoidHom.fst M N)) (Units.map (MonoidHom.snd M N)))
      ((fun u =>
          { val := (↑u.fst, ↑u.snd), inv := (↑u.fst⁻¹, ↑u.snd⁻¹),
            val_inv := (_ : (↑u.fst * ↑u.fst⁻¹, ↑u.snd * ↑u.snd⁻¹) = 1),
            inv_val := (_ : (↑u.fst⁻¹ * ↑u.fst, ↑u.snd⁻¹ * ↑u.snd) = 1) })
        (u₁, u₂)) =
    (u₁, u₂)
[PROOFSTEP]
simp only [Units.map, MonoidHom.coe_fst, Units.inv_eq_val_inv, MonoidHom.coe_snd, MonoidHom.prod_apply, Prod.mk.injEq]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : Mˣ × Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ ↑(MonoidHom.mk'
            (fun u =>
              { val := (↑u).fst, inv := (↑u⁻¹).fst, val_inv := (_ : (↑u).fst * (↑u⁻¹).fst = 1),
                inv_val := (_ : (↑u⁻¹).fst * (↑u).fst = 1) })
            (_ :
              ∀ (a b : (M × N)ˣ),
                (fun u =>
                      { val := (↑u).fst, inv := (↑u⁻¹).fst, val_inv := (_ : (↑u).fst * (↑u⁻¹).fst = 1),
                        inv_val := (_ : (↑u⁻¹).fst * (↑u).fst = 1) })
                    (a * b) =
                  (fun u =>
                        { val := (↑u).fst, inv := (↑u⁻¹).fst, val_inv := (_ : (↑u).fst * (↑u⁻¹).fst = 1),
                          inv_val := (_ : (↑u⁻¹).fst * (↑u).fst = 1) })
                      a *
                    (fun u =>
                        { val := (↑u).fst, inv := (↑u⁻¹).fst, val_inv := (_ : (↑u).fst * (↑u⁻¹).fst = 1),
                          inv_val := (_ : (↑u⁻¹).fst * (↑u).fst = 1) })
                      b))
        { val := (↑u₁, ↑u₂), inv := (↑u₁⁻¹, ↑u₂⁻¹),
          val_inv := (_ : (↑(u₁, u₂).fst * ↑(u₁, u₂).fst⁻¹, ↑(u₁, u₂).snd * ↑(u₁, u₂).snd⁻¹) = 1),
          inv_val := (_ : (↑(u₁, u₂).fst⁻¹ * ↑(u₁, u₂).fst, ↑(u₁, u₂).snd⁻¹ * ↑(u₁, u₂).snd) = 1) } =
      u₁ ∧
    ↑(MonoidHom.mk'
            (fun u =>
              { val := (↑u).snd, inv := (↑u⁻¹).snd, val_inv := (_ : (↑u).snd * (↑u⁻¹).snd = 1),
                inv_val := (_ : (↑u⁻¹).snd * (↑u).snd = 1) })
            (_ :
              ∀ (a b : (M × N)ˣ),
                (fun u =>
                      { val := (↑u).snd, inv := (↑u⁻¹).snd, val_inv := (_ : (↑u).snd * (↑u⁻¹).snd = 1),
                        inv_val := (_ : (↑u⁻¹).snd * (↑u).snd = 1) })
                    (a * b) =
                  (fun u =>
                        { val := (↑u).snd, inv := (↑u⁻¹).snd, val_inv := (_ : (↑u).snd * (↑u⁻¹).snd = 1),
                          inv_val := (_ : (↑u⁻¹).snd * (↑u).snd = 1) })
                      a *
                    (fun u =>
                        { val := (↑u).snd, inv := (↑u⁻¹).snd, val_inv := (_ : (↑u).snd * (↑u⁻¹).snd = 1),
                          inv_val := (_ : (↑u⁻¹).snd * (↑u).snd = 1) })
                      b))
        { val := (↑u₁, ↑u₂), inv := (↑u₁⁻¹, ↑u₂⁻¹),
          val_inv := (_ : (↑(u₁, u₂).fst * ↑(u₁, u₂).fst⁻¹, ↑(u₁, u₂).snd * ↑(u₁, u₂).snd⁻¹) = 1),
          inv_val := (_ : (↑(u₁, u₂).fst⁻¹ * ↑(u₁, u₂).fst, ↑(u₁, u₂).snd⁻¹ * ↑(u₁, u₂).snd) = 1) } =
      u₂
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
α : Type u_8
inst✝ : Monoid α
⊢ (fun x => (↑x, op ↑x⁻¹)) 1 = 1
[PROOFSTEP]
simp only [inv_one, eq_self_iff_true, Units.val_one, op_one, Prod.mk_eq_one, and_self_iff]
[GOAL]
A : Type u_1
B : Type u_2
G : Type u_3
H : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
α : Type u_8
inst✝ : Monoid α
x y : αˣ
⊢ OneHom.toFun { toFun := fun x => (↑x, op ↑x⁻¹), map_one' := (_ : (1, op ↑1⁻¹) = 1) } (x * y) =
    OneHom.toFun { toFun := fun x => (↑x, op ↑x⁻¹), map_one' := (_ : (1, op ↑1⁻¹) = 1) } x *
      OneHom.toFun { toFun := fun x => (↑x, op ↑x⁻¹), map_one' := (_ : (1, op ↑1⁻¹) = 1) } y
[PROOFSTEP]
simp only [mul_inv_rev, op_mul, Units.val_mul, Prod.mk_mul_mk]