[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ Group (MulAut M)
[PROOFSTEP]
refine'
  { mul := fun g h => MulEquiv.trans h g
    one := MulEquiv.refl M
    inv := MulEquiv.symm
    div := fun g h => MulEquiv.trans h.symm g
    npow := @npowRec _ ⟨MulEquiv.refl M⟩ ⟨fun g h => MulEquiv.trans h g⟩
    zpow := @zpowRec _ ⟨MulEquiv.refl M⟩ ⟨fun g h => MulEquiv.trans h g⟩ ⟨MulEquiv.symm⟩ .. }
[GOAL]
case refine'_1
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (a b c : MulAut M), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
case refine'_2
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (a : MulAut M), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
case refine'_3
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (a : MulAut M), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
case refine'_4
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (x : MulAut M), npowRec 0 x = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_5
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (n : ℕ) (x : MulAut M), npowRec (n + 1) x = x * npowRec n x
[PROOFSTEP]
intros
[GOAL]
case refine'_6
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (a b : MulAut M), a / b = a * b⁻¹
[PROOFSTEP]
intros
[GOAL]
case refine'_7
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (a : MulAut M), zpowRec 0 a = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_8
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (n : ℕ) (a : MulAut M), zpowRec (Int.ofNat (Nat.succ n)) a = a * zpowRec (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
case refine'_9
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (n : ℕ) (a : MulAut M), zpowRec (Int.negSucc n) a = (zpowRec (↑(Nat.succ n)) a)⁻¹
[PROOFSTEP]
intros
[GOAL]
case refine'_10
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (a : MulAut M), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ b✝ c✝ : MulAut M
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
ext
[GOAL]
case refine'_2
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
⊢ 1 * a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_3
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
⊢ a✝ * 1 = a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_4
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
x✝ : MulAut M
⊢ npowRec 0 x✝ = 1
[PROOFSTEP]
ext
[GOAL]
case refine'_5
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
n✝ : ℕ
x✝ : MulAut M
⊢ npowRec (n✝ + 1) x✝ = x✝ * npowRec n✝ x✝
[PROOFSTEP]
ext
[GOAL]
case refine'_6
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ b✝ : MulAut M
⊢ a✝ / b✝ = a✝ * b✝⁻¹
[PROOFSTEP]
ext
[GOAL]
case refine'_7
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
⊢ zpowRec 0 a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case refine'_8
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
n✝ : ℕ
a✝ : MulAut M
⊢ zpowRec (Int.ofNat (Nat.succ n✝)) a✝ = a✝ * zpowRec (Int.ofNat n✝) a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_9
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
n✝ : ℕ
a✝ : MulAut M
⊢ zpowRec (Int.negSucc n✝) a✝ = (zpowRec (↑(Nat.succ n✝)) a✝)⁻¹
[PROOFSTEP]
ext
[GOAL]
case refine'_10
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case refine'_1.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ b✝ c✝ : MulAut M
x✝ : M
⊢ ↑(a✝ * b✝ * c✝) x✝ = ↑(a✝ * (b✝ * c✝)) x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_1.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ b✝ c✝ : MulAut M
x✝ : M
⊢ ↑(a✝ * b✝ * c✝) x✝ = ↑(a✝ * (b✝ * c✝)) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
x✝ : M
⊢ ↑(1 * a✝) x✝ = ↑a✝ x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_2.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
x✝ : M
⊢ ↑(1 * a✝) x✝ = ↑a✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
x✝ : M
⊢ ↑(a✝ * 1) x✝ = ↑a✝ x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_3.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
x✝ : M
⊢ ↑(a✝ * 1) x✝ = ↑a✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_4.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
x✝¹ : MulAut M
x✝ : M
⊢ ↑(npowRec 0 x✝¹) x✝ = ↑1 x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_4.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
x✝¹ : MulAut M
x✝ : M
⊢ ↑(npowRec 0 x✝¹) x✝ = ↑1 x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_5.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
n✝ : ℕ
x✝¹ : MulAut M
x✝ : M
⊢ ↑(npowRec (n✝ + 1) x✝¹) x✝ = ↑(x✝¹ * npowRec n✝ x✝¹) x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_5.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
n✝ : ℕ
x✝¹ : MulAut M
x✝ : M
⊢ ↑(npowRec (n✝ + 1) x✝¹) x✝ = ↑(x✝¹ * npowRec n✝ x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_6.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ b✝ : MulAut M
x✝ : M
⊢ ↑(a✝ / b✝) x✝ = ↑(a✝ * b✝⁻¹) x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_6.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ b✝ : MulAut M
x✝ : M
⊢ ↑(a✝ / b✝) x✝ = ↑(a✝ * b✝⁻¹) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_7.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
x✝ : M
⊢ ↑(zpowRec 0 a✝) x✝ = ↑1 x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_7.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
x✝ : M
⊢ ↑(zpowRec 0 a✝) x✝ = ↑1 x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_8.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
n✝ : ℕ
a✝ : MulAut M
x✝ : M
⊢ ↑(zpowRec (Int.ofNat (Nat.succ n✝)) a✝) x✝ = ↑(a✝ * zpowRec (Int.ofNat n✝) a✝) x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_8.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
n✝ : ℕ
a✝ : MulAut M
x✝ : M
⊢ ↑(zpowRec (Int.ofNat (Nat.succ n✝)) a✝) x✝ = ↑(a✝ * zpowRec (Int.ofNat n✝) a✝) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_9.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
n✝ : ℕ
a✝ : MulAut M
x✝ : M
⊢ ↑(zpowRec (Int.negSucc n✝) a✝) x✝ = ↑(zpowRec (↑(Nat.succ n✝)) a✝)⁻¹ x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_9.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
n✝ : ℕ
a✝ : MulAut M
x✝ : M
⊢ ↑(zpowRec (Int.negSucc n✝) a✝) x✝ = ↑(zpowRec (↑(Nat.succ n✝)) a✝)⁻¹ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
x✝ : M
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_10.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
x✝ : M
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
a✝ : MulAut M
x✝ : M
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
apply Equiv.left_inv
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ MulAut M →* Equiv.Perm M
[PROOFSTEP]
refine' { toFun := MulEquiv.toEquiv, .. }
[GOAL]
case refine'_1
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ 1.toEquiv = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_2
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ ∀ (x y : MulAut M),
    OneHom.toFun { toFun := MulEquiv.toEquiv, map_one' := ?refine'_1 } (x * y) =
      OneHom.toFun { toFun := MulEquiv.toEquiv, map_one' := ?refine'_1 } x *
        OneHom.toFun { toFun := MulEquiv.toEquiv, map_one' := ?refine'_1 } y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
⊢ 1.toEquiv = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Mul M
x✝ y✝ : MulAut M
⊢ OneHom.toFun { toFun := MulEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } (x✝ * y✝) =
    OneHom.toFun { toFun := MulEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } x✝ *
      OneHom.toFun { toFun := MulEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } y✝
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Mul M
inst✝ : Group G
g x✝ : G
⊢ (fun h => g⁻¹ * h * g) ((fun h => g * h * g⁻¹) x✝) = x✝
[PROOFSTEP]
simp only [mul_assoc, inv_mul_cancel_left, mul_left_inv, mul_one]
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Mul M
inst✝ : Group G
g x✝ : G
⊢ (fun h => g * h * g⁻¹) ((fun h => g⁻¹ * h * g) x✝) = x✝
[PROOFSTEP]
simp only [mul_assoc, mul_inv_cancel_left, mul_right_inv, mul_one]
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Mul M
inst✝ : Group G
g : G
⊢ ∀ (x y : G),
    Equiv.toFun
        { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
          left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
          right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) }
        (x * y) =
      Equiv.toFun
          { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
            left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
            right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) }
          x *
        Equiv.toFun
          { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
            left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
            right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) }
          y
[PROOFSTEP]
simp only [mul_assoc, inv_mul_cancel_left, forall_const]
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Mul M
inst✝ : Group G
⊢ (fun g =>
        {
          toEquiv :=
            { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
              left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
              right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
          map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) })
      1 =
    1
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Mul M
inst✝ : Group G
x✝ : G
⊢ ↑((fun g =>
            {
              toEquiv :=
                { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                  left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                  right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
              map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) })
          1)
      x✝ =
    ↑1 x✝
[PROOFSTEP]
simp only [one_mul, inv_one, mul_one, one_apply]
[GOAL]
case h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Mul M
inst✝ : Group G
x✝ : G
⊢ ↑{
          toEquiv :=
            { toFun := fun h => h, invFun := fun h => h, left_inv := (_ : Function.LeftInverse (fun h => h) fun h => h),
              right_inv := (_ : Function.RightInverse (fun h => h) fun h => h) },
          map_mul' :=
            (_ :
              ∀ (x y : G),
                Equiv.toFun
                    { toFun := fun h => h, invFun := fun h => h,
                      left_inv := (_ : Function.LeftInverse (fun h => h) fun h => h),
                      right_inv := (_ : Function.RightInverse (fun h => h) fun h => h) }
                    (x * y) =
                  Equiv.toFun
                      { toFun := fun h => h, invFun := fun h => h,
                        left_inv := (_ : Function.LeftInverse (fun h => h) fun h => h),
                        right_inv := (_ : Function.RightInverse (fun h => h) fun h => h) }
                      x *
                    Equiv.toFun
                      { toFun := fun h => h, invFun := fun h => h,
                        left_inv := (_ : Function.LeftInverse (fun h => h) fun h => h),
                        right_inv := (_ : Function.RightInverse (fun h => h) fun h => h) }
                      y) }
      x✝ =
    x✝
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Mul M
inst✝ : Group G
g₁ g₂ : G
⊢ OneHom.toFun
      {
        toFun := fun g =>
          {
            toEquiv :=
              { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
            map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) },
        map_one' :=
          (_ :
            (fun g =>
                  {
                    toEquiv :=
                      { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                        left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                        right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
                    map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) })
                1 =
              1) }
      (g₁ * g₂) =
    OneHom.toFun
        {
          toFun := fun g =>
            {
              toEquiv :=
                { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                  left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                  right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
              map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) },
          map_one' :=
            (_ :
              (fun g =>
                    {
                      toEquiv :=
                        { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                          left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                          right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
                      map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) })
                  1 =
                1) }
        g₁ *
      OneHom.toFun
        {
          toFun := fun g =>
            {
              toEquiv :=
                { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                  left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                  right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
              map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) },
          map_one' :=
            (_ :
              (fun g =>
                    {
                      toEquiv :=
                        { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                          left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                          right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
                      map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) })
                  1 =
                1) }
        g₂
[PROOFSTEP]
ext h
[GOAL]
case h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Mul M
inst✝ : Group G
g₁ g₂ h : G
⊢ ↑(OneHom.toFun
          {
            toFun := fun g =>
              {
                toEquiv :=
                  { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                    left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                    right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
                map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) },
            map_one' :=
              (_ :
                (fun g =>
                      {
                        toEquiv :=
                          { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                            left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                            right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
                        map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) })
                    1 =
                  1) }
          (g₁ * g₂))
      h =
    ↑(OneHom.toFun
            {
              toFun := fun g =>
                {
                  toEquiv :=
                    { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                      left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                      right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
                  map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) },
              map_one' :=
                (_ :
                  (fun g =>
                        {
                          toEquiv :=
                            { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                              left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                              right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
                          map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) })
                      1 =
                    1) }
            g₁ *
          OneHom.toFun
            {
              toFun := fun g =>
                {
                  toEquiv :=
                    { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                      left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                      right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
                  map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) },
              map_one' :=
                (_ :
                  (fun g =>
                        {
                          toEquiv :=
                            { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g,
                              left_inv := (_ : ∀ (x : G), g⁻¹ * (g * x * g⁻¹) * g = x),
                              right_inv := (_ : ∀ (x : G), g * (g⁻¹ * x * g) * g⁻¹ = x) },
                          map_mul' := (_ : ∀ (a a_1 : G), g * (a * a_1) * g⁻¹ = g * a * g⁻¹ * (g * a_1 * g⁻¹)) })
                      1 =
                    1) }
            g₂)
      h
[PROOFSTEP]
show g₁ * g₂ * h * (g₁ * g₂)⁻¹ = g₁ * (g₂ * h * g₂⁻¹) * g₁⁻¹
[GOAL]
case h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Mul M
inst✝ : Group G
g₁ g₂ h : G
⊢ g₁ * g₂ * h * (g₁ * g₂)⁻¹ = g₁ * (g₂ * h * g₂⁻¹) * g₁⁻¹
[PROOFSTEP]
simp only [mul_assoc, mul_inv_rev]
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ Group (AddAut A)
[PROOFSTEP]
refine'
  { mul := fun g h => AddEquiv.trans h g
    one := AddEquiv.refl A
    inv := AddEquiv.symm
    div := fun g h => AddEquiv.trans h.symm g
    npow := @npowRec _ ⟨AddEquiv.refl A⟩ ⟨fun g h => AddEquiv.trans h g⟩
    zpow := @zpowRec _ ⟨AddEquiv.refl A⟩ ⟨fun g h => AddEquiv.trans h g⟩ ⟨AddEquiv.symm⟩ .. }
[GOAL]
case refine'_1
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (a b c : AddAut A), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
case refine'_2
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (a : AddAut A), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
case refine'_3
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (a : AddAut A), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
case refine'_4
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (x : AddAut A), npowRec 0 x = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_5
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (n : ℕ) (x : AddAut A), npowRec (n + 1) x = x * npowRec n x
[PROOFSTEP]
intros
[GOAL]
case refine'_6
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (a b : AddAut A), a / b = a * b⁻¹
[PROOFSTEP]
intros
[GOAL]
case refine'_7
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (a : AddAut A), zpowRec 0 a = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_8
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (n : ℕ) (a : AddAut A), zpowRec (Int.ofNat (Nat.succ n)) a = a * zpowRec (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
case refine'_9
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (n : ℕ) (a : AddAut A), zpowRec (Int.negSucc n) a = (zpowRec (↑(Nat.succ n)) a)⁻¹
[PROOFSTEP]
intros
[GOAL]
case refine'_10
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (a : AddAut A), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ b✝ c✝ : AddAut A
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
ext
[GOAL]
case refine'_2
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
⊢ 1 * a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_3
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
⊢ a✝ * 1 = a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_4
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
x✝ : AddAut A
⊢ npowRec 0 x✝ = 1
[PROOFSTEP]
ext
[GOAL]
case refine'_5
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
n✝ : ℕ
x✝ : AddAut A
⊢ npowRec (n✝ + 1) x✝ = x✝ * npowRec n✝ x✝
[PROOFSTEP]
ext
[GOAL]
case refine'_6
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ b✝ : AddAut A
⊢ a✝ / b✝ = a✝ * b✝⁻¹
[PROOFSTEP]
ext
[GOAL]
case refine'_7
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
⊢ zpowRec 0 a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case refine'_8
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
n✝ : ℕ
a✝ : AddAut A
⊢ zpowRec (Int.ofNat (Nat.succ n✝)) a✝ = a✝ * zpowRec (Int.ofNat n✝) a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_9
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
n✝ : ℕ
a✝ : AddAut A
⊢ zpowRec (Int.negSucc n✝) a✝ = (zpowRec (↑(Nat.succ n✝)) a✝)⁻¹
[PROOFSTEP]
ext
[GOAL]
case refine'_10
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case refine'_1.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ b✝ c✝ : AddAut A
x✝ : A
⊢ ↑(a✝ * b✝ * c✝) x✝ = ↑(a✝ * (b✝ * c✝)) x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_1.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ b✝ c✝ : AddAut A
x✝ : A
⊢ ↑(a✝ * b✝ * c✝) x✝ = ↑(a✝ * (b✝ * c✝)) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
x✝ : A
⊢ ↑(1 * a✝) x✝ = ↑a✝ x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_2.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
x✝ : A
⊢ ↑(1 * a✝) x✝ = ↑a✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
x✝ : A
⊢ ↑(a✝ * 1) x✝ = ↑a✝ x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_3.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
x✝ : A
⊢ ↑(a✝ * 1) x✝ = ↑a✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_4.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
x✝¹ : AddAut A
x✝ : A
⊢ ↑(npowRec 0 x✝¹) x✝ = ↑1 x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_4.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
x✝¹ : AddAut A
x✝ : A
⊢ ↑(npowRec 0 x✝¹) x✝ = ↑1 x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_5.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
n✝ : ℕ
x✝¹ : AddAut A
x✝ : A
⊢ ↑(npowRec (n✝ + 1) x✝¹) x✝ = ↑(x✝¹ * npowRec n✝ x✝¹) x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_5.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
n✝ : ℕ
x✝¹ : AddAut A
x✝ : A
⊢ ↑(npowRec (n✝ + 1) x✝¹) x✝ = ↑(x✝¹ * npowRec n✝ x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_6.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ b✝ : AddAut A
x✝ : A
⊢ ↑(a✝ / b✝) x✝ = ↑(a✝ * b✝⁻¹) x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_6.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ b✝ : AddAut A
x✝ : A
⊢ ↑(a✝ / b✝) x✝ = ↑(a✝ * b✝⁻¹) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_7.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
x✝ : A
⊢ ↑(zpowRec 0 a✝) x✝ = ↑1 x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_7.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
x✝ : A
⊢ ↑(zpowRec 0 a✝) x✝ = ↑1 x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_8.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
n✝ : ℕ
a✝ : AddAut A
x✝ : A
⊢ ↑(zpowRec (Int.ofNat (Nat.succ n✝)) a✝) x✝ = ↑(a✝ * zpowRec (Int.ofNat n✝) a✝) x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_8.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
n✝ : ℕ
a✝ : AddAut A
x✝ : A
⊢ ↑(zpowRec (Int.ofNat (Nat.succ n✝)) a✝) x✝ = ↑(a✝ * zpowRec (Int.ofNat n✝) a✝) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_9.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
n✝ : ℕ
a✝ : AddAut A
x✝ : A
⊢ ↑(zpowRec (Int.negSucc n✝) a✝) x✝ = ↑(zpowRec (↑(Nat.succ n✝)) a✝)⁻¹ x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_9.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
n✝ : ℕ
a✝ : AddAut A
x✝ : A
⊢ ↑(zpowRec (Int.negSucc n✝) a✝) x✝ = ↑(zpowRec (↑(Nat.succ n✝)) a✝)⁻¹ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
x✝ : A
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
try rfl
[GOAL]
case refine'_10.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
x✝ : A
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
a✝ : AddAut A
x✝ : A
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
apply Equiv.left_inv
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ AddAut A →* Equiv.Perm A
[PROOFSTEP]
refine' { toFun := AddEquiv.toEquiv, .. }
[GOAL]
case refine'_1
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ 1.toEquiv = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_2
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ ∀ (x y : AddAut A),
    OneHom.toFun { toFun := AddEquiv.toEquiv, map_one' := ?refine'_1 } (x * y) =
      OneHom.toFun { toFun := AddEquiv.toEquiv, map_one' := ?refine'_1 } x *
        OneHom.toFun { toFun := AddEquiv.toEquiv, map_one' := ?refine'_1 } y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
⊢ 1.toEquiv = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
A : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Add A
x✝ y✝ : AddAut A
⊢ OneHom.toFun { toFun := AddEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } (x✝ * y✝) =
    OneHom.toFun { toFun := AddEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } x✝ *
      OneHom.toFun { toFun := AddEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } y✝
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
g x✝ : G
⊢ (fun h => -g + h + g) ((fun h => g + h + -g) x✝) = x✝
[PROOFSTEP]
simp only [add_assoc, neg_add_cancel_left, add_left_neg, add_zero]
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
g x✝ : G
⊢ (fun h => g + h + -g) ((fun h => -g + h + g) x✝) = x✝
[PROOFSTEP]
simp only [add_assoc, add_neg_cancel_left, add_right_neg, add_zero]
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
g : G
⊢ ∀ (x y : G),
    Equiv.toFun
        { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
          left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
          right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) }
        (x + y) =
      Equiv.toFun
          { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
            left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
            right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) }
          x +
        Equiv.toFun
          { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
            left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
            right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) }
          y
[PROOFSTEP]
simp only [add_assoc, neg_add_cancel_left, forall_const]
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
⊢ (fun g =>
        ↑Additive.ofMul
          {
            toEquiv :=
              { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
            map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
      0 =
    0
[PROOFSTEP]
apply Additive.toMul.injective
[GOAL]
case a
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
⊢ ↑Additive.toMul
      ((fun g =>
          ↑Additive.ofMul
            {
              toEquiv :=
                { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                  left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                  right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
              map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
        0) =
    ↑Additive.toMul 0
[PROOFSTEP]
ext
[GOAL]
case a.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
x✝ : G
⊢ ↑(↑Additive.toMul
          ((fun g =>
              ↑Additive.ofMul
                {
                  toEquiv :=
                    { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                      left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                      right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                  map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
            0))
      x✝ =
    ↑(↑Additive.toMul 0) x✝
[PROOFSTEP]
simp only [zero_add, neg_zero, add_zero, toMul_ofMul, toMul_zero, one_apply]
[GOAL]
case a.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
x✝ : G
⊢ ↑{
          toEquiv :=
            { toFun := fun h => h, invFun := fun h => h, left_inv := (_ : Function.LeftInverse (fun h => h) fun h => h),
              right_inv := (_ : Function.RightInverse (fun h => h) fun h => h) },
          map_add' :=
            (_ :
              ∀ (x y : G),
                Equiv.toFun
                    { toFun := fun h => h, invFun := fun h => h,
                      left_inv := (_ : Function.LeftInverse (fun h => h) fun h => h),
                      right_inv := (_ : Function.RightInverse (fun h => h) fun h => h) }
                    (x + y) =
                  Equiv.toFun
                      { toFun := fun h => h, invFun := fun h => h,
                        left_inv := (_ : Function.LeftInverse (fun h => h) fun h => h),
                        right_inv := (_ : Function.RightInverse (fun h => h) fun h => h) }
                      x +
                    Equiv.toFun
                      { toFun := fun h => h, invFun := fun h => h,
                        left_inv := (_ : Function.LeftInverse (fun h => h) fun h => h),
                        right_inv := (_ : Function.RightInverse (fun h => h) fun h => h) }
                      y) }
      x✝ =
    x✝
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
g₁ g₂ : G
⊢ ZeroHom.toFun
      {
        toFun := fun g =>
          ↑Additive.ofMul
            {
              toEquiv :=
                { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                  left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                  right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
              map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) },
        map_zero' :=
          (_ :
            (fun g =>
                  ↑Additive.ofMul
                    {
                      toEquiv :=
                        { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                          left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                          right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                      map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
                0 =
              0) }
      (g₁ + g₂) =
    ZeroHom.toFun
        {
          toFun := fun g =>
            ↑Additive.ofMul
              {
                toEquiv :=
                  { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                    left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                    right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) },
          map_zero' :=
            (_ :
              (fun g =>
                    ↑Additive.ofMul
                      {
                        toEquiv :=
                          { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                            left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                            right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                        map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
                  0 =
                0) }
        g₁ +
      ZeroHom.toFun
        {
          toFun := fun g =>
            ↑Additive.ofMul
              {
                toEquiv :=
                  { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                    left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                    right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) },
          map_zero' :=
            (_ :
              (fun g =>
                    ↑Additive.ofMul
                      {
                        toEquiv :=
                          { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                            left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                            right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                        map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
                  0 =
                0) }
        g₂
[PROOFSTEP]
apply Additive.toMul.injective
[GOAL]
case a
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
g₁ g₂ : G
⊢ ↑Additive.toMul
      (ZeroHom.toFun
        {
          toFun := fun g =>
            ↑Additive.ofMul
              {
                toEquiv :=
                  { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                    left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                    right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) },
          map_zero' :=
            (_ :
              (fun g =>
                    ↑Additive.ofMul
                      {
                        toEquiv :=
                          { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                            left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                            right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                        map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
                  0 =
                0) }
        (g₁ + g₂)) =
    ↑Additive.toMul
      (ZeroHom.toFun
          {
            toFun := fun g =>
              ↑Additive.ofMul
                {
                  toEquiv :=
                    { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                      left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                      right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                  map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) },
            map_zero' :=
              (_ :
                (fun g =>
                      ↑Additive.ofMul
                        {
                          toEquiv :=
                            { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                              left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                              right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                          map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
                    0 =
                  0) }
          g₁ +
        ZeroHom.toFun
          {
            toFun := fun g =>
              ↑Additive.ofMul
                {
                  toEquiv :=
                    { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                      left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                      right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                  map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) },
            map_zero' :=
              (_ :
                (fun g =>
                      ↑Additive.ofMul
                        {
                          toEquiv :=
                            { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                              left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                              right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                          map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
                    0 =
                  0) }
          g₂)
[PROOFSTEP]
ext h
[GOAL]
case a.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
g₁ g₂ h : G
⊢ ↑(↑Additive.toMul
          (ZeroHom.toFun
            {
              toFun := fun g =>
                ↑Additive.ofMul
                  {
                    toEquiv :=
                      { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                        left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                        right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                    map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) },
              map_zero' :=
                (_ :
                  (fun g =>
                        ↑Additive.ofMul
                          {
                            toEquiv :=
                              { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                                left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                                right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                            map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
                      0 =
                    0) }
            (g₁ + g₂)))
      h =
    ↑(↑Additive.toMul
          (ZeroHom.toFun
              {
                toFun := fun g =>
                  ↑Additive.ofMul
                    {
                      toEquiv :=
                        { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                          left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                          right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                      map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) },
                map_zero' :=
                  (_ :
                    (fun g =>
                          ↑Additive.ofMul
                            {
                              toEquiv :=
                                { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                                  left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                                  right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                              map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
                        0 =
                      0) }
              g₁ +
            ZeroHom.toFun
              {
                toFun := fun g =>
                  ↑Additive.ofMul
                    {
                      toEquiv :=
                        { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                          left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                          right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                      map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) },
                map_zero' :=
                  (_ :
                    (fun g =>
                          ↑Additive.ofMul
                            {
                              toEquiv :=
                                { toFun := fun h => g + h + -g, invFun := fun h => -g + h + g,
                                  left_inv := (_ : ∀ (x : G), -g + (g + x + -g) + g = x),
                                  right_inv := (_ : ∀ (x : G), g + (-g + x + g) + -g = x) },
                              map_add' := (_ : ∀ (a a_1 : G), g + (a + a_1) + -g = g + a + -g + (g + a_1 + -g)) })
                        0 =
                      0) }
              g₂))
      h
[PROOFSTEP]
show g₁ + g₂ + h + -(g₁ + g₂) = g₁ + (g₂ + h + -g₂) + -g₁
[GOAL]
case a.h
A : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : Add A
inst✝ : AddGroup G
g₁ g₂ h : G
⊢ g₁ + g₂ + h + -(g₁ + g₂) = g₁ + (g₂ + h + -g₂) + -g₁
[PROOFSTEP]
simp only [add_assoc, neg_add_rev]


[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a✝ b✝ c✝ d a b c : α
⊢ (a + b) / c = a / c + b / c
[PROOFSTEP]
simp_rw [div_eq_mul_inv, add_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
h : b ≠ 0
⊢ (b + a) / b = 1 + a / b
[PROOFSTEP]
rw [← div_self h, add_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
h : b ≠ 0
⊢ (a + b) / b = a / b + 1
[PROOFSTEP]
rw [← div_self h, add_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b
[PROOFSTEP]
rw [mul_add, one_div_mul_cancel ha, add_mul, one_mul, mul_assoc, mul_one_div_cancel hb, mul_one, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a✝ b✝ c d a b : α
hc : c ≠ 0
⊢ (a + b / c) * c = a * c + b
[PROOFSTEP]
rw [right_distrib, div_mul_cancel _ hc]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a✝ b✝ c✝ d a b c : α
hc : c ≠ 0
⊢ b + a / c = (b * c + a) / c
[PROOFSTEP]
rw [add_div, mul_div_cancel _ hc]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a✝ b✝ c✝ d a b c : α
hc : c ≠ 0
⊢ a / c + b = (a + b * c) / c
[PROOFSTEP]
rwa [add_comm, add_div', add_comm]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = (a * d + b * c) / (b * d)
[PROOFSTEP]
rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + 1 / b = (a + b) / (a * b)
[PROOFSTEP]
rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)
[PROOFSTEP]
rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a b : K
⊢ -1 * -1 = 1
[PROOFSTEP]
rw [neg_mul_neg, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / -a = 1 / (-1 * a)
[PROOFSTEP]
rw [neg_eq_neg_one_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / (-1 * a) = 1 / a * (1 / -1)
[PROOFSTEP]
rw [one_div_mul_one_div_rev]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / a * (1 / -1) = 1 / a * -1
[PROOFSTEP]
rw [one_div_neg_one_eq_neg_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / a * -1 = -(1 / a)
[PROOFSTEP]
rw [mul_neg, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ b / -a = b * (1 / -a)
[PROOFSTEP]
rw [← inv_eq_one_div, division_def]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ b * (1 / -a) = b * -(1 / a)
[PROOFSTEP]
rw [one_div_neg_eq_neg_one_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ b * -(1 / a) = -(b * (1 / a))
[PROOFSTEP]
rw [neg_mul_eq_mul_neg]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -(b * (1 / a)) = -(b / a)
[PROOFSTEP]
rw [mul_one_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -b / a = -(b / a)
[PROOFSTEP]
rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -(b / a) = -b / a
[PROOFSTEP]
simp [neg_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -a / -b = a / b
[PROOFSTEP]
rw [div_neg_eq_neg_div, neg_div, neg_neg]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a b : K
⊢ -a⁻¹ = (-a)⁻¹
[PROOFSTEP]
rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ a / -b = -(a / b)
[PROOFSTEP]
rw [← div_neg_eq_neg_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a b : K
⊢ (-a)⁻¹ = -a⁻¹
[PROOFSTEP]
rw [neg_inv]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a b : K
⊢ (-1)⁻¹ = -1
[PROOFSTEP]
rw [← neg_inv, inv_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b c d a : K
h : a ≠ 0
⊢ a / -a = -1
[PROOFSTEP]
rw [div_neg_eq_neg_div, div_self h]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b c d a : K
h : a ≠ 0
⊢ -a / a = -1
[PROOFSTEP]
rw [neg_div, div_self h]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b✝ c✝ d a b c : K
⊢ a / c - b / c = (a - b) / c
[PROOFSTEP]
rw [sub_eq_add_neg, ← neg_div, div_add_div_same, sub_eq_add_neg]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b✝ c d a b : K
h : b ≠ 0
⊢ (b - a) / b = 1 - a / b
[PROOFSTEP]
simpa only [← @div_self _ _ b h] using (div_sub_div_same b a b).symm
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b✝ c d a b : K
h : b ≠ 0
⊢ (a - b) / b = a / b - 1
[PROOFSTEP]
simpa only [← @div_self _ _ b h] using (div_sub_div_same a b b).symm
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b✝ c d a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹
[PROOFSTEP]
rw [mul_sub, sub_mul, mul_inv_cancel_right₀ hb, inv_mul_cancel ha, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a b c d : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b
[PROOFSTEP]
rw [mul_sub_left_distrib (1 / a), one_div_mul_cancel ha, mul_sub_right_distrib, one_mul, mul_assoc,
  mul_one_div_cancel hb, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)
[PROOFSTEP]
simpa only [mul_neg, neg_div, ← sub_eq_add_neg] using hbc.neg_right.div_add_div hbd hb hd
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a b c d : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
[PROOFSTEP]
simp only [inv_eq_one_div, (Commute.one_right a).div_sub_div hab ha hb, one_mul, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
[PROOFSTEP]
rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ b - a / c = (b * c - a) / c
[PROOFSTEP]
simpa using div_sub_div b a one_ne_zero hc
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ a / c - b = (a - c * b) / c
[PROOFSTEP]
simpa using div_sub_div a b hc one_ne_zero
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : DivisionRing K
K' : Type ?u.52132
inst✝¹⁵ : Zero K'
inst✝¹⁴ : One K'
inst✝¹³ : Add K'
inst✝¹² : Mul K'
inst✝¹¹ : Neg K'
inst✝¹⁰ : Sub K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : GroupWithZero K' := Injective.groupWithZero f hf zero one mul inv div npow zpow
src✝ : Ring K' := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ f ↑(Rat.mk' a b) = f (↑a * (↑b)⁻¹)
[PROOFSTEP]
erw [rat_cast, mul, inv, int_cast, nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : DivisionRing K
K' : Type ?u.52132
inst✝¹⁵ : Zero K'
inst✝¹⁴ : One K'
inst✝¹³ : Add K'
inst✝¹² : Mul K'
inst✝¹¹ : Neg K'
inst✝¹⁰ : Sub K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : GroupWithZero K' := Injective.groupWithZero f hf zero one mul inv div npow zpow
src✝ : Ring K' := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
exact DivisionRing.ratCast_mk a b h1 h2
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : DivisionRing K
K' : Type ?u.52132
inst✝¹⁵ : Zero K'
inst✝¹⁴ : One K'
inst✝¹³ : Add K'
inst✝¹² : Mul K'
inst✝¹¹ : Neg K'
inst✝¹⁰ : Sub K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : GroupWithZero K' := Injective.groupWithZero f hf zero one mul inv div npow zpow
src✝ : Ring K' := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℚ
x : K'
⊢ f ((fun x x_1 => x • x_1) a x) = f (↑a * x)
[PROOFSTEP]
erw [qsmul, mul, Rat.smul_def, rat_cast]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : Field K
K' : Type ?u.64255
inst✝¹⁵ : Zero K'
inst✝¹⁴ : Mul K'
inst✝¹³ : Add K'
inst✝¹² : Neg K'
inst✝¹¹ : Sub K'
inst✝¹⁰ : One K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : CommGroupWithZero K' := Injective.commGroupWithZero f hf zero one mul inv div npow zpow
src✝ : CommRing K' := Injective.commRing f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ f ↑(Rat.mk' a b) = f (↑a * (↑b)⁻¹)
[PROOFSTEP]
erw [rat_cast, mul, inv, int_cast, nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : Field K
K' : Type ?u.64255
inst✝¹⁵ : Zero K'
inst✝¹⁴ : Mul K'
inst✝¹³ : Add K'
inst✝¹² : Neg K'
inst✝¹¹ : Sub K'
inst✝¹⁰ : One K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : CommGroupWithZero K' := Injective.commGroupWithZero f hf zero one mul inv div npow zpow
src✝ : CommRing K' := Injective.commRing f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
exact DivisionRing.ratCast_mk a b h1 h2
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : Field K
K' : Type ?u.64255
inst✝¹⁵ : Zero K'
inst✝¹⁴ : Mul K'
inst✝¹³ : Add K'
inst✝¹² : Neg K'
inst✝¹¹ : Sub K'
inst✝¹⁰ : One K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : CommGroupWithZero K' := Injective.commGroupWithZero f hf zero one mul inv div npow zpow
src✝ : CommRing K' := Injective.commRing f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℚ
x : K'
⊢ f ((fun x x_1 => x • x_1) a x) = f (↑a * x)
[PROOFSTEP]
erw [qsmul, mul, Rat.smul_def, rat_cast]


[GOAL]
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
src✝ : (Π₀ (i : ι), M i) ≃ ((i : ι) → M i) := DFinsupp.equivFunOnFintype
f g : ⨁ (i : ι), M i
⊢ ↑(f + g) = ↑f + ↑g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
src✝ : (Π₀ (i : ι), M i) ≃ ((i : ι) → M i) := DFinsupp.equivFunOnFintype
f g : ⨁ (i : ι), M i
x✝ : ι
⊢ ↑(f + g) x✝ = (↑f + ↑g) x✝
[PROOFSTEP]
rw [add_apply, Pi.add_apply]
[GOAL]
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
src✝ : (Π₀ (i : ι), M i) ≃ ((i : ι) → M i) := DFinsupp.equivFunOnFintype
c : R
f : ⨁ (i : ι), M i
⊢ AddHom.toFun { toFun := FunLike.coe, map_add' := (_ : ∀ (f g : ⨁ (i : ι), M i), ↑(f + g) = ↑f + ↑g) } (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun { toFun := FunLike.coe, map_add' := (_ : ∀ (f g : ⨁ (i : ι), M i), ↑(f + g) = ↑f + ↑g) } f
[PROOFSTEP]
simp_rw [RingHom.id_apply]
[GOAL]
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
src✝ : (Π₀ (i : ι), M i) ≃ ((i : ι) → M i) := DFinsupp.equivFunOnFintype
c : R
f : ⨁ (i : ι), M i
⊢ ↑(c • f) = c • ↑f
[PROOFSTEP]
rw [DFinsupp.coe_smul]
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ ↑(linearEquivFunOnFintype R ι M) (↑(lof R ι M i) m) = Pi.single i m
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
a : ι
⊢ ↑(linearEquivFunOnFintype R ι M) (↑(lof R ι M i) m) a = Pi.single i m a
[PROOFSTEP]
change (DFinsupp.equivFunOnFintype (lof R ι M i m)) a = _
[GOAL]
case h
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
a : ι
⊢ ↑DFinsupp.equivFunOnFintype (↑(lof R ι M i) m) a = Pi.single i m a
[PROOFSTEP]
convert _root_.congr_fun (DFinsupp.equivFunOnFintype_single i m) a
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ ↑(LinearEquiv.symm (linearEquivFunOnFintype R ι M)) (Pi.single i m) = ↑(lof R ι M i) m
[PROOFSTEP]
change (DFinsupp.equivFunOnFintype.symm (Pi.single i m)) = _
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ ↑DFinsupp.equivFunOnFintype.symm (Pi.single i m) = ↑(lof R ι M i) m
[PROOFSTEP]
rw [DFinsupp.equivFunOnFintype_symm_single i m]
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ DFinsupp.single i m = ↑(lof R ι M i) m
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
f : ⨁ (i : ι), M i
⊢ ↑(LinearEquiv.symm (linearEquivFunOnFintype R ι M)) ↑f = f
[PROOFSTEP]
simp [linearEquivFunOnFintype]
[GOAL]
R : Type u
inst✝⁴ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
N : Type u₁
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
f g : ⨁ (i : ι), M i
h : f = g
x✝ : ι
⊢ ↑(component R ι M x✝) f = ↑(component R ι M x✝) g
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
α : ι → Type u_1
δ : (i : ι) → α i → Type w
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → Module R (δ i j)
src✝ : (⨁ (i : (_i : ι) × α _i), δ i.fst i.snd) →+ ⨁ (i : ι) (j : α i), δ i j := sigmaCurry
r : R
⊢ ∀ (x : ⨁ (i : (i : ι) × α i), δ i.fst i.snd),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : ⨁ (i : (_i : ι) × α _i), δ i.fst i.snd),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀ (x y : ⨁ (i : (_i : ι) × α _i), δ i.fst i.snd),
                  ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
          x
[PROOFSTEP]
convert DFinsupp.sigmaCurry_smul (δ := δ) r
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ iSup A = ⊤
[PROOFSTEP]
rw [Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top]
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ Function.Surjective ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (A i))
[PROOFSTEP]
exact Function.Bijective.surjective h
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
⊢ ↑(collectedBasis h v) = fun a => ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
funext a
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(collectedBasis h v) a = ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
simp only [IsInternal.collectedBasis, coeLinearMap, Basis.coe_ofRepr, LinearEquiv.trans_symm, LinearEquiv.symm_symm,
  LinearEquiv.trans_apply, sigmaFinsuppLequivDFinsupp_apply, sigmaFinsuppEquivDFinsupp_single,
  LinearEquiv.ofBijective_apply, sigmaFinsuppAddEquivDFinsupp_apply]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(toModule R ι M fun i => Submodule.subtype (A i))
      (↑(LinearEquiv.symm (DFinsupp.mapRange.linearEquiv fun i => (v i).repr))
        (DFinsupp.single a.fst (Finsupp.single a.snd 1))) =
    ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
rw [DFinsupp.mapRange.linearEquiv_symm]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(toModule R ι M fun i => Submodule.subtype (A i))
      (↑(DFinsupp.mapRange.linearEquiv fun i => LinearEquiv.symm (v i).repr)
        (DFinsupp.single a.fst (Finsupp.single a.snd 1))) =
    ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
erw [DFinsupp.mapRange.linearEquiv_apply]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(toModule R ι M fun i => Submodule.subtype (A i))
      (DFinsupp.mapRange (fun i x => ↑(LinearEquiv.symm (v i).repr) x)
        (_ : ∀ (i : ι), ↑(LinearEquiv.symm (v i).repr) 0 = 0) (DFinsupp.single a.fst (Finsupp.single a.snd 1))) =
    ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
simp only [DFinsupp.mapRange_single, Basis.repr_symm_apply, Finsupp.total_single, one_smul, toModule]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (A i)) (DFinsupp.single a.fst (↑(v a.fst) a.snd)) =
    ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
erw [DFinsupp.lsum_single]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(Submodule.subtype (A a.fst)) (↑(v a.fst) a.snd) = ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
simp only [Submodule.coeSubtype]
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(collectedBasis h v) a ∈ A a.fst
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A✝ A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ iSup A = A i ⊔ A j
[PROOFSTEP]
rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]
[GOAL]
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
⊢ IsInternal A ↔ IsCompl (A i) (A j)
[PROOFSTEP]
have : ∀ k, k = i ∨ k = j := fun k ↦ by simpa using Set.ext_iff.mp h k
[GOAL]
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
k : ι
⊢ k = i ∨ k = j
[PROOFSTEP]
simpa using Set.ext_iff.mp h k
[GOAL]
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ IsInternal A ↔ IsCompl (A i) (A j)
[PROOFSTEP]
rw [isInternal_submodule_iff_independent_and_iSup_eq_top, iSup, ← Set.image_univ, h, Set.image_insert_eq,
  Set.image_singleton, sSup_pair, CompleteLattice.independent_pair hij this]
[GOAL]
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)
[PROOFSTEP]
exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩


[GOAL]
R : Type u_1
G : Type u_2
inst✝ : CancelCommMonoid G
g : G
⊢ mulLeftEmbedding g = mulRightEmbedding g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
G : Type u_2
inst✝ : CancelCommMonoid G
g x✝ : G
⊢ ↑(mulLeftEmbedding g) x✝ = ↑(mulRightEmbedding g) x✝
[PROOFSTEP]
exact mul_comm _ _