[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : SmoothMul I G
g h✝ : G
X Y : LeftInvariantDerivation I G
h : ↑X = ↑Y
⊢ X = Y
[PROOFSTEP]
cases X
[GOAL]
case mk
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : SmoothMul I G
g h✝ : G
Y : LeftInvariantDerivation I G
toDerivation✝ : Derivation 𝕜 C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝ :
  ∀ (g : G), ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) toDerivation✝) = ↑(Derivation.evalAt g) toDerivation✝
h : ↑{ toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ } = ↑Y
⊢ { toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ } = Y
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : SmoothMul I G
g h✝ : G
toDerivation✝¹ : Derivation 𝕜 C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝¹ :
  ∀ (g : G), ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) toDerivation✝¹) = ↑(Derivation.evalAt g) toDerivation✝¹
toDerivation✝ : Derivation 𝕜 C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝ :
  ∀ (g : G), ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) toDerivation✝) = ↑(Derivation.evalAt g) toDerivation✝
h :
  ↑{ toDerivation := toDerivation✝¹, left_invariant'' := left_invariant''✝¹ } =
    ↑{ toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ }
⊢ { toDerivation := toDerivation✝¹, left_invariant'' := left_invariant''✝¹ } =
    { toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ }
[PROOFSTEP]
congr
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) 0) = ↑(Derivation.evalAt g) 0
[PROOFSTEP]
simp only [_root_.map_zero]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (↑X + ↑Y)) = ↑(Derivation.evalAt g) (↑X + ↑Y)
[PROOFSTEP]
simp only [map_add, Derivation.coe_add, left_invariant', Pi.add_apply]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (-↑X)) = ↑(Derivation.evalAt g) (-↑X)
[PROOFSTEP]
rw [map_neg (Derivation.evalAt (𝕜 := 𝕜) (1 : G)), map_neg (𝒅ₕ (smoothLeftMul_one I g)), left_invariant',
  map_neg (Derivation.evalAt (𝕜 := 𝕜) g)]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (↑X - ↑Y)) = ↑(Derivation.evalAt g) (↑X - ↑Y)
[PROOFSTEP]
rw [map_sub (Derivation.evalAt (𝕜 := 𝕜) (1 : G)), map_sub (𝒅ₕ (smoothLeftMul_one I g)),
  map_sub (Derivation.evalAt (𝕜 := 𝕜) g), left_invariant', left_invariant']
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : ℕ
X : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (r • ↑X)) = ↑(Derivation.evalAt g) (r • ↑X)
[PROOFSTEP]
simp_rw [LinearMap.map_smul_of_tower _ r, left_invariant']
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : ℤ
X : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (r • ↑X)) = ↑(Derivation.evalAt g) (r • ↑X)
[PROOFSTEP]
simp_rw [LinearMap.map_smul_of_tower _ r, left_invariant']
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
X : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (r • ↑X)) = ↑(Derivation.evalAt g) (r • ↑X)
[PROOFSTEP]
simp_rw [LinearMap.map_smul, left_invariant']
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑(evalAt (g * h)) X = ↑(𝒅ₕ (_ : ↑(𝑳 I g) h = g * h)) (↑(evalAt h) X)
[PROOFSTEP]
ext f
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ↑(↑(evalAt (g * h)) X) f = ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) h = g * h)) (↑(evalAt h) X)) f
[PROOFSTEP]
rw [← left_invariant, apply_hfdifferential, apply_hfdifferential, L_mul, fdifferential_comp, apply_fdifferential]
  -- Porting note: more agressive here
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ↑(↑(LinearMap.comp (𝒅 (𝑳 I g) (↑(𝑳 I h) 1)) (𝒅 (𝑳 I h) 1)) (↑(evalAt 1) X)) f =
    ↑(↑(evalAt h) X) (ContMDiffMap.comp f (𝑳 I g))
[PROOFSTEP]
erw [LinearMap.comp_apply]
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ↑(↑(𝒅 (𝑳 I g) (↑(𝑳 I h) 1)) (↑(𝒅 (𝑳 I h) 1) (↑(evalAt 1) X))) f = ↑(↑(evalAt h) X) (ContMDiffMap.comp f (𝑳 I g))
[PROOFSTEP]
rw [apply_fdifferential, ← apply_hfdifferential, left_invariant]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ContMDiffMap.comp (↑X f) (𝑳 I g) = ↑X (ContMDiffMap.comp f (𝑳 I g))
[PROOFSTEP]
ext h
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h✝ : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
⊢ ↑(ContMDiffMap.comp (↑X f) (𝑳 I g)) h = ↑(↑X (ContMDiffMap.comp f (𝑳 I g))) h
[PROOFSTEP]
rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, apply_hfdifferential, apply_fdifferential,
  evalAt_apply]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ⁅↑X, ↑Y⁆) = ↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆
[PROOFSTEP]
ext f
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
⊢ ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ⁅↑X, ↑Y⁆)) f = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
have hX := Derivation.congr_fun (left_invariant' g X) (Y f)
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ↑X)) (↑Y f) = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
⊢ ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ⁅↑X, ↑Y⁆)) f = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
have hY := Derivation.congr_fun (left_invariant' g Y) (X f)
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ↑X)) (↑Y f) = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ↑Y)) (↑X f) = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ⁅↑X, ↑Y⁆)) f = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [apply_hfdifferential, apply_fdifferential, Derivation.evalAt_apply] at hX hY ⊢
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑↑X (ContMDiffMap.comp (↑Y f) (𝑳 I g))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑↑Y (ContMDiffMap.comp (↑X f) (𝑳 I g))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑⁅↑X, ↑Y⁆ (ContMDiffMap.comp f (𝑳 I g))) 1 = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [comp_L] at hX hY
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑⁅↑X, ↑Y⁆ (ContMDiffMap.comp f (𝑳 I g))) 1 = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [Derivation.commutator_apply, SmoothMap.coe_sub, Pi.sub_apply, coe_derivation]
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑X (↑↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 - ↑(↑↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 =
    ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [coe_derivation] at hX hY ⊢
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 - ↑(↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 =
    ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [hX, hY]
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑(Derivation.evalAt g) ↑X) (↑Y f) - ↑(↑(Derivation.evalAt g) ↑Y) (↑X f) = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
⊢ ⁅X + Y, Z⁆ = ⁅X, Z⁆ + ⁅Y, Z⁆
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅X + Y, Z⁆ f✝ = ↑(⁅X, Z⁆ + ⁅Y, Z⁆) f✝
[PROOFSTEP]
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑X (↑Z f✝) + ↑Y (↑Z f✝) - (↑Z (↑X f✝) + ↑Z (↑Y f✝)) = ↑X (↑Z f✝) - ↑Z (↑X f✝) + (↑Y (↑Z f✝) - ↑Z (↑Y f✝))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
⊢ ⁅X, Y + Z⁆ = ⁅X, Y⁆ + ⁅X, Z⁆
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅X, Y + Z⁆ f✝ = ↑(⁅X, Y⁆ + ⁅X, Z⁆) f✝
[PROOFSTEP]
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑X (↑Y f✝) + ↑X (↑Z f✝) - (↑Y (↑X f✝) + ↑Z (↑X f✝)) = ↑X (↑Y f✝) - ↑Y (↑X f✝) + (↑X (↑Z f✝) - ↑Z (↑X f✝))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
⊢ ⁅X, X⁆ = 0
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅X, X⁆ f✝ = ↑0 f✝
[PROOFSTEP]
simp only [commutator_apply, sub_self]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ 0 = ↑0 f✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
⊢ ⁅X, ⁅Y, Z⁆⁆ = ⁅⁅X, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅X, ⁅Y, Z⁆⁆ f✝ = ↑(⁅⁅X, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆) f✝
[PROOFSTEP]
simp only [commutator_apply, coe_add, coe_sub, map_sub, Pi.add_apply]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑X (↑Y (↑Z f✝)) - ↑X (↑Z (↑Y f✝)) - (↑Y (↑Z (↑X f✝)) - ↑Z (↑Y (↑X f✝))) =
    ↑X (↑Y (↑Z f✝)) - ↑Y (↑X (↑Z f✝)) - (↑Z (↑X (↑Y f✝)) - ↑Z (↑Y (↑X f✝))) +
      (↑Y (↑X (↑Z f✝)) - ↑Y (↑Z (↑X f✝)) - (↑X (↑Z (↑Y f✝)) - ↑Z (↑X (↑Y f✝))))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
Y Z : LeftInvariantDerivation I G
⊢ ⁅Y, r • Z⁆ = r • ⁅Y, Z⁆
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅Y, r • Z⁆ f✝ = ↑(r • ⁅Y, Z⁆) f✝
[PROOFSTEP]
simp only [commutator_apply, map_smul, smul_sub, coe_smul, Pi.smul_apply]


[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : ↑p ^ i = 0
⊢ i = n
[PROOFSTEP]
contrapose! hpi
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : i ≠ n
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
replace hin := lt_of_le_of_ne hin hpi
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hpi : i ≠ n
hin : i < n
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
clear hpi
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
have : (p : TruncatedWittVector p n R) ^ i = WittVector.truncate n ((p : 𝕎 R) ^ i) := by
  rw [RingHom.map_pow, map_natCast]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ↑p ^ i = ↑(WittVector.truncate n) (↑p ^ i)
[PROOFSTEP]
rw [RingHom.map_pow, map_natCast]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = ↑(WittVector.truncate n) (↑p ^ i)
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
rw [this, ne_eq, ext_iff, not_forall]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = ↑(WittVector.truncate n) (↑p ^ i)
⊢ ∃ x, ¬coeff x (↑(WittVector.truncate n) (↑p ^ i)) = coeff x 0
[PROOFSTEP]
clear this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ∃ x, ¬coeff x (↑(WittVector.truncate n) (↑p ^ i)) = coeff x 0
[PROOFSTEP]
use⟨i, hin⟩
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬coeff { val := i, isLt := hin } (↑(WittVector.truncate n) (↑p ^ i)) = coeff { val := i, isLt := hin } 0
[PROOFSTEP]
rw [WittVector.coeff_truncate, coeff_zero, Fin.val_mk, WittVector.coeff_p_pow]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬1 = 0
[PROOFSTEP]
haveI : Nontrivial R := CharP.nontrivial_of_char_ne_one hp.1.ne_one
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : Nontrivial R
⊢ ¬1 = 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n
[PROOFSTEP]
rw [card, ZMod.card]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : ZMod (p ^ n)
⊢ ?m.71174 ∣ p ^ n
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ↑(RingHom.comp (truncate hm) (RingEquiv.toRingHom (zmodEquivTrunc p m))) x =
    ↑(zmodEquivTrunc p n) (↑(ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n))) x)
[PROOFSTEP]
rw [commutes _ _ hm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ↑(RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p n)) (ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n)))) x =
    ↑(zmodEquivTrunc p n) (↑(ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n))) x)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ ↑(RingEquiv.symm (zmodEquivTrunc p n)) (↑(truncate hm) x) =
    ↑(ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n))) (↑(RingEquiv.symm (zmodEquivTrunc p m)) x)
[PROOFSTEP]
apply (zmodEquivTrunc p n).injective
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ ↑(zmodEquivTrunc p n) (↑(RingEquiv.symm (zmodEquivTrunc p n)) (↑(truncate hm) x)) =
    ↑(zmodEquivTrunc p n)
      (↑(ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n))) (↑(RingEquiv.symm (zmodEquivTrunc p m)) x))
[PROOFSTEP]
rw [← commutes' _ _ hm]
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ ↑(zmodEquivTrunc p n) (↑(RingEquiv.symm (zmodEquivTrunc p n)) (↑(truncate hm) x)) =
    ↑(truncate hm) (↑(zmodEquivTrunc p m) (↑(RingEquiv.symm (zmodEquivTrunc p m)) x))
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
⊢ RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate hm) =
    RingHom.comp (ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n)))
      (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m)))
[PROOFSTEP]
ext
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x✝ : TruncatedWittVector p m (ZMod p)
⊢ ↑(RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate hm)) x✝ =
    ↑(RingHom.comp (ZMod.castHom (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n)))
          (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))))
      x✝
[PROOFSTEP]
apply commutes_symm'
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m)))
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n)) =
    RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (TruncatedWittVector.truncate h))
      (truncate n)
[PROOFSTEP]
rw [commutes_symm, RingHom.comp_assoc]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (TruncatedWittVector.truncate h))
      (truncate n) =
    RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m)
[PROOFSTEP]
rw [RingHom.comp_assoc, truncate_comp_wittVector_truncate]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
⊢ RingHom.comp (TruncatedWittVector.truncate hk)
      (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₂)) (PadicInt.toZModPow k₂)) =
    RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁)
[PROOFSTEP]
rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc, PadicInt.zmod_cast_comp_toZModPow _ _ hk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ RingHom.comp (toPadicInt p) (fromPadicInt p) = RingHom.id ℤ_[p]
[PROOFSTEP]
rw [← PadicInt.toZModPow_eq_iff_ext]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    RingHom.comp (PadicInt.toZModPow n) (RingHom.comp (toPadicInt p) (fromPadicInt p)) =
      RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p])
[PROOFSTEP]
intro n
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (PadicInt.toZModPow n) (RingHom.comp (toPadicInt p) (fromPadicInt p)) =
    RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p])
[PROOFSTEP]
rw [← RingHom.comp_assoc, toPadicInt, PadicInt.lift_spec]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (toZModPow p n) (fromPadicInt p) = RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p])
[PROOFSTEP]
simp only [fromPadicInt, toZModPow, RingHom.comp_id]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n))
      (lift (fun k => RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k)) (PadicInt.toZModPow k))
        (_ :
          ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂),
            RingHom.comp (TruncatedWittVector.truncate hk)
                (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₂)) (PadicInt.toZModPow k₂)) =
              RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))) =
    PadicInt.toZModPow n
[PROOFSTEP]
rw [RingHom.comp_assoc, truncate_comp_lift, ← RingHom.comp_assoc]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n)))
        (RingEquiv.toRingHom (zmodEquivTrunc p n)))
      (PadicInt.toZModPow n) =
    PadicInt.toZModPow n
[PROOFSTEP]
simp only [RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.id_comp]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ↑(RingHom.comp (toPadicInt p) (fromPadicInt p)) x = ↑(RingHom.id ℤ_[p]) x
[PROOFSTEP]
rw [toPadicInt_comp_fromPadicInt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ RingHom.comp (fromPadicInt p) (toPadicInt p) = RingHom.id (𝕎 (ZMod p))
[PROOFSTEP]
apply WittVector.hom_ext
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (k : ℕ),
    RingHom.comp (truncate k) (RingHom.comp (fromPadicInt p) (toPadicInt p)) =
      RingHom.comp (truncate k) (RingHom.id (𝕎 (ZMod p)))
[PROOFSTEP]
intro n
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (truncate n) (RingHom.comp (fromPadicInt p) (toPadicInt p)) =
    RingHom.comp (truncate n) (RingHom.id (𝕎 (ZMod p)))
[PROOFSTEP]
rw [fromPadicInt, ← RingHom.comp_assoc, truncate_comp_lift, RingHom.comp_assoc]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p n)) (RingHom.comp (PadicInt.toZModPow n) (toPadicInt p)) =
    RingHom.comp (truncate n) (RingHom.id (𝕎 (ZMod p)))
[PROOFSTEP]
simp only [toPadicInt, toZModPow, RingHom.comp_id, PadicInt.lift_spec, RingHom.id_comp, ← RingHom.comp_assoc,
  RingEquiv.toRingHom_comp_symm_toRingHom]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ ↑(RingHom.comp (fromPadicInt p) (toPadicInt p)) x = ↑(RingHom.id (𝕎 (ZMod p))) x
[PROOFSTEP]
rw [fromPadicInt_comp_toPadicInt]


[GOAL]
R : Type u
S : Type v
T : Type w
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : SubringClass S R
s : S
n : ℤ
⊢ ↑n ∈ s
[PROOFSTEP]
simp only [← zsmul_one, zsmul_mem, one_mem]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
p q : Subring R
h : (fun s => s.carrier) p = (fun s => s.carrier) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
q : Subring R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
h : (fun s => s.carrier) { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ } = (fun s => s.carrier) q
⊢ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
toSubsemiring✝¹ : Subsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toSubsemiring✝¹.carrier → -x ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toSubsemiring := toSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s => s.carrier) { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSubsemiring
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
toSubsemiring✝¹ : Subsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toSubsemiring✝¹.carrier → -x ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toSubsemiring := toSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s => s.carrier) { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝
[PROOFSTEP]
exact SetLike.ext' h
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -x✝ ∈ s.carrier
[PROOFSTEP]
rw [← neg_one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -1 * x✝ ∈ s.carrier
[PROOFSTEP]
exact mul_mem hneg h
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s✝ : Subring R
f : R →+* S
s : Subring R
y : S
⊢ (∃ x x_1, ↑f x = y) ↔ ∃ x, x ∈ s ∧ ↑f x = y
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f✝ f : R →+* S
⊢ range f = Subring.map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f✝ f : R →+* S
x✝ : S
⊢ x✝ ∈ range f ↔ x✝ ∈ Subring.map f ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f : R →+* S
⊢ Subring.map g (range f) = range (comp g f)
[PROOFSTEP]
simpa only [range_eq_map] using (⊤ : Subring R).map_map g f
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set (Subring R)
⊢ ↑(⨅ (t : Subring R) (_ : t ∈ s), t.toSubmonoid) = ⋂ (t : Subring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set (Subring R)
⊢ ↑(⨅ (t : Subring R) (_ : t ∈ s), toAddSubgroup t) = ⋂ (t : Subring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
S : ι → Subring R
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp only [iInf, coe_sInf, Set.biInter_range]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
S : ι → Subring R
x : R
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hneg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) (_ : -x ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ p a ha
[PROOFSTEP]
refine Exists.elim ?_ fun (ha : a ∈ closure s) (hc : p a ha) => hc
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hneg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) (_ : -x ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ ∃ x, p a x
[PROOFSTEP]
refine
  closure_induction ha (fun m hm => ⟨subset_closure hm, Hs m hm⟩) ⟨zero_mem _, H0⟩ ⟨one_mem _, H1⟩ ?_
    (fun x hx => hx.elim fun hx' hx => ⟨neg_mem hx', Hneg _ _ hx⟩) ?_
[GOAL]
case refine_1
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hneg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) (_ : -x ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ ∀ (x y : R), (∃ x_1, p x x_1) → (∃ x, p y x) → ∃ x_1, p (x + y) x_1
[PROOFSTEP]
exact (fun x y hx hy => hx.elim fun hx' hx => hy.elim fun hy' hy => ⟨add_mem hx' hy', Hadd _ _ _ _ hx hy⟩)
[GOAL]
case refine_2
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hneg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) (_ : -x ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ ∀ (x y : R), (∃ x_1, p x x_1) → (∃ x, p y x) → ∃ x_1, p (x * y) x_1
[PROOFSTEP]
exact (fun x y hx hy => hx.elim fun hx' hx => hy.elim fun hy' hy => ⟨mul_mem hx' hy', Hmul _ _ _ _ hx hy⟩)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ p a b
[PROOFSTEP]
refine' closure_induction hb _ (H0_right _) (H1_right _) (Hadd_right a) (Hneg_right a) (Hmul_right a)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), x ∈ s → p a x
[PROOFSTEP]
refine' closure_induction ha Hs (fun x _ => H0_left x) (fun x _ => H1_left x) _ _ _
[GOAL]
case refine'_1
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x + y) x_1
[PROOFSTEP]
exact fun x y H₁ H₂ z zs => Hadd_left x y z (H₁ z zs) (H₂ z zs)
[GOAL]
case refine'_2
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → ∀ (x_1 : R), x_1 ∈ s → p (-x) x_1
[PROOFSTEP]
exact fun x hx z zs => Hneg_left x z (hx z zs)
[GOAL]
case refine'_3
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x * y) x_1
[PROOFSTEP]
exact fun x y H₁ H₂ z zs => Hmul_left x y z (H₁ z zs) (H₂ z zs)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
⊢ 0 * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [zero_mul q]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
⊢ 0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.zero_mem _
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
p₁ p₂ : R
ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ (p₁ + p₂) * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [add_mul p₁ p₂ q]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
p₁ p₂ : R
ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ p₁ * q + p₂ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.add_mem _ ihp₁ ihp₂
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ -x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
have f : -x * q = -(x * q) := by simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ -x * q = -(x * q)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
f : -x * q = -(x * q)
⊢ -x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [f]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
f : -x * q = -(x * q)
⊢ -(x * q) ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.neg_mem _ hx
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * 0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [mul_zero x]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ 0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.zero_mem _
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q₁ q₂ : R
ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * (q₁ + q₂) ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [mul_add x q₁ q₂]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q₁ q₂ : R
ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * q₁ + x * q₂ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.add_mem _ ihq₁ ihq₂
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * -z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
have f : x * -z = -(x * z) := by simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * -z = -(x * z)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
f : x * -z = -(x * z)
⊢ x * -z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [f]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
f : x * -z = -(x * z)
⊢ -(x * z) ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.neg_mem _ hz
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y : { x // x ∈ closure s }
⊢ x * y = y * x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y : { x // x ∈ closure s }
⊢ ↑(x * y) = ↑(y * x)
[PROOFSTEP]
simp only [Subring.coe_mul]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y : { x // x ∈ closure s }
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
refine'
  closure_induction₂ x.prop y.prop hcomm (fun x => by simp only [mul_zero, zero_mul])
    (fun x => by simp only [mul_zero, zero_mul]) (fun x => by simp only [mul_one, one_mul])
    (fun x => by simp only [mul_one, one_mul]) (fun x y hxy => by simp only [mul_neg, neg_mul, hxy])
    (fun x y hxy => by simp only [mul_neg, neg_mul, hxy]) (fun x₁ x₂ y h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun x₁ x₂ y h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun x₁ x₂ y h₁ h₂ => by rw [← mul_assoc, ← h₁, mul_assoc x₁ y x₂, ← h₂, mul_assoc]) fun x₁ x₂ y h₁ h₂ => by
    rw [← mul_assoc, h₁, mul_assoc, h₂, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ 0 * x = x * 0
[PROOFSTEP]
simp only [mul_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ x * 0 = 0 * x
[PROOFSTEP]
simp only [mul_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ 1 * x = x * 1
[PROOFSTEP]
simp only [mul_one, one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ x * 1 = 1 * x
[PROOFSTEP]
simp only [mul_one, one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y : R
hxy : x * y = y * x
⊢ -x * y = y * -x
[PROOFSTEP]
simp only [mul_neg, neg_mul, hxy]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y : R
hxy : x * y = y * x
⊢ x * -y = -y * x
[PROOFSTEP]
simp only [mul_neg, neg_mul, hxy]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * y = y * x₁
h₂ : x₂ * y = y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * x₂ = x₂ * x₁
h₂ : x₁ * y = y * x₁
⊢ x₁ * (x₂ + y) = (x₂ + y) * x₁
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * y = y * x₁
h₂ : x₂ * y = y * x₂
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
[PROOFSTEP]
rw [← mul_assoc, ← h₁, mul_assoc x₁ y x₂, ← h₂, mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * x₂ = x₂ * x₁
h₂ : x₁ * y = y * x₁
⊢ x₁ * (x₂ * y) = x₂ * y * x₁
[PROOFSTEP]
rw [← mul_assoc, h₁, mul_assoc, h₂, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ (∀ (t : List R), t ∈ [l] → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod [l]) = x
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ ∀ (y : R), y ∈ l → y ∈ s ∨ y = -1
[PROOFSTEP]
clear_aux_decl
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ ∀ (y : R), y ∈ l → y ∈ s ∨ y = -1
[PROOFSTEP]
tauto
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x : R
h : x ∈ closure s
⊢ (∀ (t : List R), t ∈ [] → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod []) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝² : R
h : x✝² ∈ closure s
x y : R
x✝¹ :
  (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) x
x✝ : (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) y
l : List (List R)
hl1 : ∀ (t : List R), t ∈ l → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hl2 : List.sum (List.map List.prod l) = x
m : List (List R)
hm1 : ∀ (t : List R), t ∈ m → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hm2 : List.sum (List.map List.prod m) = y
⊢ List.sum (List.map List.prod (l ++ m)) = x + y
[PROOFSTEP]
simp [hl2, hm2]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x : R
x✝ : (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) x
L : List (List R)
hL : (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x
⊢ List.sum (List.map List.prod (List.map (List.cons (-1)) [])) = -List.sum (List.map List.prod [])
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x : R
x✝ : (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) x
L : List (List R)
hL : (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x
⊢ ∀ (head : List R) (tail : List (List R)),
    List.sum (List.map List.prod (List.map (List.cons (-1)) tail)) = -List.sum (List.map List.prod tail) →
      List.sum (List.map List.prod (List.map (List.cons (-1)) (head :: tail))) =
        -List.sum (List.map List.prod (head :: tail))
[PROOFSTEP]
simp (config := { contextual := true }) [List.map_cons, add_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subring R
x : R × S
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (RingHom.fst R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_fst]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subring S
x : R × S
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (RingHom.snd R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_snd]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i ↔ ∃ i, x ∈ S i
[PROOFSTEP]
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
let U : Subring R :=
  Subring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup)
    (Submonoid.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
    (AddSubgroup.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
suffices ⨆ i, S i ≤ U by intro h; simpa using (this h)
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
this : ⨆ (i : ι), S i ≤ U
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
intro h
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
this : ⨆ (i : ι), S i ≤ U
h : x ∈ ⨆ (i : ι), S i
⊢ ∃ i, x ∈ S i
[PROOFSTEP]
simpa using (this h)
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ ⨆ (i : ι), S i ≤ U
[PROOFSTEP]
exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
[PROOFSTEP]
simp [mem_iSup_of_directed hS]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
S : Set (Subring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
haveI : Nonempty S := Sne.to_subtype
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
S : Set (Subring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk, exists_prop]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
S : Set (Subring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : Subring R) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp [mem_sSup_of_directedOn Sne hS]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subring R
f : R →+* S
⊢ ↑(range f) = ↑⊤ ↔ Set.range ↑f = Set.univ
[PROOFSTEP]
rw [coe_range, coe_top]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s t : Subring R
g : S → R
f : R →+* S
h : Function.LeftInverse g ↑f
src✝ : R →+* { x // x ∈ RingHom.range f } := RingHom.rangeRestrict f
x : { x // x ∈ RingHom.range f }
x' : R
hx' : ↑f x' = ↑x
⊢ ↑f (g ↑x) = ↑x
[PROOFSTEP]
rw [← hx', h x']
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
⊢ C x
[PROOFSTEP]
have h0 : C 0 := add_neg_self (1 : R) ▸ ha h1 hneg1
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
⊢ C x
[PROOFSTEP]
rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hx : List.sum (List.map List.prod L) ∈ closure s
⊢ C (List.sum (List.map List.prod L))
[PROOFSTEP]
clear hx
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod L))
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.nil
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
HL : ∀ (t : List R), t ∈ [] → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod []))
[PROOFSTEP]
exact h0
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : ∀ (t : List R), t ∈ hd :: tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
rw [List.forall_mem_cons] at HL
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (y : R), y ∈ x → y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
suffices C (List.prod hd) by
  rw [List.map_cons, List.sum_cons]
  exact ha this (ih HL.2)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (y : R), y ∈ x → y ∈ s ∨ y = -1
this : C (List.prod hd)
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
rw [List.map_cons, List.sum_cons]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (y : R), y ∈ x → y ∈ s ∨ y = -1
this : C (List.prod hd)
⊢ C (List.prod hd + List.sum (List.map List.prod tl))
[PROOFSTEP]
exact ha this (ih HL.2)
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (y : R), y ∈ x → y ∈ s ∨ y = -1
⊢ C (List.prod hd)
[PROOFSTEP]
replace HL := HL.1
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
⊢ C (List.prod hd)
[PROOFSTEP]
clear ih tl
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
⊢ C (List.prod hd)
[PROOFSTEP]
obtain ⟨L, HL', HP | HP⟩ : ∃ L : List R, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
case intro.intro.cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod hd)
case intro.intro.cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rotate_left
[GOAL]
case intro.intro.cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rw [HP]
[GOAL]
case intro.intro.cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod L)
[PROOFSTEP]
clear HP HL hd
[GOAL]
case intro.intro.cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
⊢ C (List.prod L)
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.cons.intro.intro.inl.nil
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
HL' : ∀ (x : R), x ∈ [] → x ∈ s
⊢ C (List.prod [])
[PROOFSTEP]
exact h1
[GOAL]
case intro.intro.cons.intro.intro.inl.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (List.prod (hd :: tl))
[PROOFSTEP]
rw [List.forall_mem_cons] at HL'
[GOAL]
case intro.intro.cons.intro.intro.inl.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (List.prod (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
case intro.intro.cons.intro.intro.inl.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (hd * List.prod tl)
[PROOFSTEP]
exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
case intro.intro.cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rw [HP]
[GOAL]
case intro.intro.cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (-List.prod L)
[PROOFSTEP]
clear HP HL hd
[GOAL]
case intro.intro.cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
⊢ C (-List.prod L)
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.cons.intro.intro.inr.nil
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
HL' : ∀ (x : R), x ∈ [] → x ∈ s
⊢ C (-List.prod [])
[PROOFSTEP]
exact hneg1
[GOAL]
case intro.intro.cons.intro.intro.inr.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (-List.prod (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons, neg_mul_eq_mul_neg]
[GOAL]
case intro.intro.cons.intro.intro.inr.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (hd * -List.prod tl)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL'
[GOAL]
case intro.intro.cons.intro.intro.inr.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (hd * -List.prod tl)
[PROOFSTEP]
exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
[PROOFSTEP]
induction' hd with hd tl ih
[GOAL]
case nil
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL✝ : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
HL : ∀ (y : R), y ∈ [] → y ∈ s ∨ y = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod [] = List.prod L ∨ List.prod [] = -List.prod L)
[PROOFSTEP]
exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
[GOAL]
case cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : ∀ (y : R), y ∈ hd :: tl → y ∈ s ∨ y = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL
[GOAL]
case cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
rcases ih HL.2 with ⟨L, HL', HP | HP⟩
[GOAL]
case cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
cases' HL.1 with hhd hhd
[GOAL]
case cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
cases' HL.1 with hhd hhd
[GOAL]
case cons.intro.intro.inl.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd ∈ s
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨hd :: L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, Or.inl <| by rw [List.prod_cons, List.prod_cons, HP]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd ∈ s
⊢ List.prod (hd :: tl) = List.prod (hd :: L)
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, HP]
[GOAL]
case cons.intro.intro.inl.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd = -1
⊢ List.prod (hd :: tl) = -List.prod L
[PROOFSTEP]
rw [List.prod_cons, hhd, neg_one_mul, HP]
[GOAL]
case cons.intro.intro.inr.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd ∈ s
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact
  ⟨hd :: L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, Or.inr <| by rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd ∈ s
⊢ List.prod (hd :: tl) = -List.prod (hd :: L)
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]
[GOAL]
case cons.intro.intro.inr.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨L, HL', Or.inl <| by rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (t : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd = -1
⊢ List.prod (hd :: tl) = List.prod L
[PROOFSTEP]
rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g ∈ G
[PROOFSTEP]
convert AddSubgroup.zsmul_mem G h k using 1
[GOAL]
case h.e'_4
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g = k • g
[PROOFSTEP]
simp