[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (a b c : RingAut R), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ b✝ c✝ : RingAut R
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (a : RingAut R), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ : RingAut R
⊢ 1 * a✝ = a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (a : RingAut R), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ : RingAut R
⊢ a✝ * 1 = a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (a : RingAut R), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ : RingAut R
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ : RingAut R
x✝ : R
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
apply Equiv.left_inv
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingAut R →* AddAut R
[PROOFSTEP]
refine' { toFun := RingEquiv.toAddEquiv .. }
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingEquiv.toAddEquiv 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingEquiv.toAddEquiv 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (x y : RingAut R),
    OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
        (x * y) =
      OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
          x *
        OneHom.toFun
          { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) } y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
x✝ y✝ : RingAut R
⊢ OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
      (x✝ * y✝) =
    OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
        x✝ *
      OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
        y✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingAut R →* MulAut R
[PROOFSTEP]
refine' { toFun := RingEquiv.toMulEquiv .. }
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingEquiv.toMulEquiv 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingEquiv.toMulEquiv 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (x y : RingAut R),
    OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
        (x * y) =
      OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
          x *
        OneHom.toFun
          { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) } y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
x✝ y✝ : RingAut R
⊢ OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
      (x✝ * y✝) =
    OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
        x✝ *
      OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
        y✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingAut R →* Equiv.Perm R
[PROOFSTEP]
refine' { toFun := RingEquiv.toEquiv .. }
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ 1.toEquiv = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ 1.toEquiv = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (x y : RingAut R),
    OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } (x * y) =
      OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } x *
        OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
x✝ y✝ : RingAut R
⊢ OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } (x✝ * y✝) =
    OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } x✝ *
      OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } y✝
[PROOFSTEP]
rfl
