awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
x : M
h : P.pairing i j = 0 ∧ P.pairing j i = 0
⊢ Eq (α := M) ((P.reflection i * P.reflection j : (a : M) → M) x : M)
    ((P.reflection j * P.reflection i : (a : M) → M) x : M)
have h₁ : x -
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M) -
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
      ((P.root : (a : ι) → M) j : M) =
  x -
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
        ((P.root : (a : ι) → M) j : M) -
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      ((P.root : (a : ι) → M) i : M)
Tactic: simp only [LinearEquiv.mul_apply, reflection_apply, LinearMap.flip_apply, map_sub,
    map_smul, root_coroot_eq_pairing, h, zero_smul, sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
⊢ Eq (α := M) ((P.reflection j : (a : M) → M) 0 : M) (0 : M)
have zero : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x u v : M
hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u
hv : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) v
hu' : (P.reflection j : (a : M) → M) u = u
hv' : (P.reflection j : (a : M) → M) v = v
⊢ (P.reflection j : (a : M) → M) (u + v) = u + v
have add : HAdd.hAdd (α := M) (β := M) ((P.reflection j : (a : M) → M) u : M) ((P.reflection j : (a : M) → M) v : M) = u + v
Tactic: rw [map_add, hu', hv']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x u v : M
hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u
hv : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) v
hu' : (P.reflection j : (a : M) → M) u = u
hv' : (P.reflection j : (a : M) → M) v = v
add : HAdd.hAdd (α := M) (β := M) ((P.reflection j : (a : M) → M) u : M) ((P.reflection j : (a : M) → M) v : M) = u + v
⊢ (P.reflection j : (a : M) → M) (u + v) = u + v
have add₁ : HAdd.hAdd (β := M) u ((P.reflection j : (a : M) → M) v : M) = u + v
Tactic: rw [map_add, hu', hv']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x u v : M
hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u
hv : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) v
hu' : (P.reflection j : (a : M) → M) u = u
hv' : (P.reflection j : (a : M) → M) v = v
add : HAdd.hAdd (α := M) (β := M) ((P.reflection j : (a : M) → M) u : M) ((P.reflection j : (a : M) → M) v : M) = u + v
add₁ : HAdd.hAdd (β := M) u ((P.reflection j : (a : M) → M) v : M) = u + v
⊢ (P.reflection j : (a : M) → M) (u + v) = u + v
have add₂ : u + v = u + v
Tactic: rw [map_add, hu', hv']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
t : R
u : M
hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u
hu' : (P.reflection j : (a : M) → M) u = u
⊢ (P.reflection j : (a : M) → M) (t • u) = t • u
have smul : HSMul.hSMul (β := M) t ((P.reflection j : (a : M) → M) u : M) = t • u
Tactic: rw [map_smul, hu']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
t : R
u : M
hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u
hu' : (P.reflection j : (a : M) → M) u = u
smul : HSMul.hSMul (β := M) t ((P.reflection j : (a : M) → M) u : M) = t • u
⊢ (P.reflection j : (a : M) → M) (t • u) = t • u
have smul₁ : t • u = t • u
Tactic: rw [map_smul, hu']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x u : M
hu : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) u
⊢ (P.reflection j : (a : M) → M) u = u
have mem : ∀ (i : ι) (his : i ∈ s),
  Eq (α := M) ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) ((P.root : (a : ι) → M) i : M)
Tactic: obtain ⟨i, his, rfl⟩ := hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
hx : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) x
⊢ (P.reflection j : (a : M) → M) x = x
have zero : Eq (α := M) ((P.reflection j : (a : M) → M) 0 : M) (0 : M)
Tactic: induction hx using Submodule.span_induction with
  | zero => rw [map_zero]
  | add u v hu hv hu' hv' => rw [map_add, hu', hv']
  | smul t u hu hu' => rw [map_smul, hu']
  | mem u hu =>
      obtain ⟨i, his, rfl⟩ := hu
      exact IsOrthogonal.reflection_apply_right <| hj i his
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
hx : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) x
zero : Eq (α := M) ((P.reflection j : (a : M) → M) 0 : M) (0 : M)
⊢ (P.reflection j : (a : M) → M) x = x
have add : ∀ (u v : M) (hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u)
  (hv : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) v)
  (hu' : (P.reflection j : (a : M) → M) u = u) (hv' : (P.reflection j : (a : M) → M) v = v),
  (P.reflection j : (a : M) → M) (u + v) = u + v
Tactic: induction hx using Submodule.span_induction with
  | zero => rw [map_zero]
  | add u v hu hv hu' hv' => rw [map_add, hu', hv']
  | smul t u hu hu' => rw [map_smul, hu']
  | mem u hu =>
      obtain ⟨i, his, rfl⟩ := hu
      exact IsOrthogonal.reflection_apply_right <| hj i his
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
hx : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) x
zero : Eq (α := M) ((P.reflection j : (a : M) → M) 0 : M) (0 : M)
add :
  ∀ (u v : M) (hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u)
    (hv : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) v)
    (hu' : (P.reflection j : (a : M) → M) u = u) (hv' : (P.reflection j : (a : M) → M) v = v),
    (P.reflection j : (a : M) → M) (u + v) = u + v
⊢ (P.reflection j : (a : M) → M) x = x
have smul : ∀ (t : R) (u : M) (hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u)
  (hu' : (P.reflection j : (a : M) → M) u = u), (P.reflection j : (a : M) → M) (t • u) = t • u
Tactic: induction hx using Submodule.span_induction with
  | zero => rw [map_zero]
  | add u v hu hv hu' hv' => rw [map_add, hu', hv']
  | smul t u hu hu' => rw [map_smul, hu']
  | mem u hu =>
      obtain ⟨i, his, rfl⟩ := hu
      exact IsOrthogonal.reflection_apply_right <| hj i his
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
hx : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) x
zero : Eq (α := M) ((P.reflection j : (a : M) → M) 0 : M) (0 : M)
add :
  ∀ (u v : M) (hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u)
    (hv : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) v)
    (hu' : (P.reflection j : (a : M) → M) u = u) (hv' : (P.reflection j : (a : M) → M) v = v),
    (P.reflection j : (a : M) → M) (u + v) = u + v
smul :
  ∀ (t : R) (u : M) (hu : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) u)
    (hu' : (P.reflection j : (a : M) → M) u = u), (P.reflection j : (a : M) → M) (t • u) = t • u
⊢ (P.reflection j : (a : M) → M) x = x
have mem : ∀ (u : M) (hu : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) u), (P.reflection j : (a : M) → M) u = u
Tactic: induction hx using Submodule.span_induction with
  | zero => rw [map_zero]
  | add u v hu hv hu' hv' => rw [map_add, hu', hv']
  | smul t u hu hu' => rw [map_smul, hu']
  | mem u hu =>
      obtain ⟨i, his, rfl⟩ := hu
      exact IsOrthogonal.reflection_apply_right <| hj i his
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0
have suffices : ∀ {i j : ι}, P.pairing i j = 0 → P.pairing j i = 0
Tactic: suffices ∀ {i j : ι}, P.pairing i j = 0 → P.pairing j i = 0 from ⟨this, this⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0
have this : IsReflexive R M
Tactic: have : IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
⊢ P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j
have this : IsReflexive R M
Tactic: have : IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
⊢ (↑(f.symm ≪≫ₗ P.toPerfPair ≪≫ₗ g.symm.dualMap) : M₂ →ₗ[R] Dual R N₂).IsPerfPair
have this : IsReflexive R N
Tactic: have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
this : IsReflexive R N
⊢ (↑(f.symm ≪≫ₗ P.toPerfPair ≪≫ₗ g.symm.dualMap) : M₂ →ₗ[R] Dual R N₂).IsPerfPair
have this₁ : IsReflexive R N₂
Tactic: have : IsReflexive R N₂ := equiv g
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
x : N
⊢ Eq (α := N →ₗ[R] R) ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.CoPolarization : (a : N) → M) x) : N →ₗ[R] R)
    ((P.CorootForm : (a : N) → N →ₗ[R] R) x : N →ₗ[R] R)
have h : ∀ (y : N),
  Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.CoPolarization : (a : N) → M) x) : N →ₗ[R] R) : (a : N) → R) y : R)
    ((((P.CorootForm : (a : N) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)
Tactic: ext y
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
⊢ P.flip.toLinearMap ∘ₗ P.Polarization = P.RootForm
have h : ∀ (x x_1 : M),
  Eq.{u_2 + 1} (α := R)
    ((((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x_1 : R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
m : M
⊢ Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N) ↔
    Eq (α := M →ₗ[R] R) ((P.RootForm : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) (0 : M →ₗ[R] R)
have rw : Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N) ↔
  Eq (α := M →ₗ[R] R) ((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) (0 : M →ₗ[R] R)
Tactic: rw [← flip_comp_polarization_eq_rootForm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
m : M
⊢ Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N) ↔
    Eq (α := M →ₗ[R] R) ((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) (0 : M →ₗ[R] R)
have refine : Eq (α := M →ₗ[R] R) ((P.flip.toLinearMap ∘ₗ P.Polarization : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) (0 : M →ₗ[R] R) →
  Eq.{u_4 + 1} (α := N) ((P.Polarization : (a : M) → N) m : N) (0 : N)
Tactic: refine ⟨fun h ↦ by simp [h], ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
⊢ P.Polarization.ker = LinearMap.ker P.RootForm
have h : ∀ (x : M), x ∈ P.Polarization.ker ↔ x ∈ LinearMap.ker P.RootForm
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
i : ι
x y : M
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.reflection i : (a : M) → M) x) : M →ₗ[R] R) : (a : M) → R)
        ((P.reflection i : (a : M) → M) y : M) :
      R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have simp : Eq.{u_2 + 1} (α := R)
  (∑ x_1 : ι,
    HMul.hMul (α := R) (β := R) ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) x_1) : (a : M) → R) x : R)
      ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) x_1) : (a : M) → R) y : R))
  (∑ i : ι, HMul.hMul (α := R) (β := R) ((P.coroot' i : (a : M) → R) x : R) ((P.coroot' i : (a : M) → R) y : R))
Tactic: simp only [rootForm_apply_apply, coroot'_reflection]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
y : N
hy : y ∈ LinearMap.range (M := ↥(P.rootSpan R)) (P.Polarization.domRestrict (P.rootSpan R))
⊢ Membership.mem (γ := Submodule R N) (P.corootSpan R) y
have obtain : ∀ (x : ↥(P.rootSpan R)) (hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y),
  Membership.mem (γ := Submodule R N) (P.corootSpan R) y
Tactic: obtain ⟨x, hx⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y
⊢ Membership.mem (γ := Submodule R N) (P.corootSpan R) y
have rw : Membership.mem (γ := Submodule R N) (P.corootSpan R)
  (∑ i : ι,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
      ((P.coroot : (a : ι) → N) i : N))
Tactic: rw [← hx, LinearMap.domRestrict_apply, Polarization_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y
⊢ Membership.mem (γ := Submodule R N) (P.corootSpan R)
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
        ((P.coroot : (a : ι) → N) i : N))
have refine : ∃ (c : ι → R),
  Eq.{u_4 + 1} (α := N) (∑ i : ι, HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) i : N))
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
        ((P.coroot : (a : ι) → N) i : N))
Tactic: refine (Submodule.mem_span_range_iff_exists_fun R).mpr ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R) : (a : ↥(P.rootSpan R)) → N) x = y
⊢ ∃ (c : ι → R),
    Eq.{u_4 + 1} (α := N) (∑ i : ι, HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) i : N))
      (∑ i : ι,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
          ((P.coroot : (a : ι) → N) i : N))
have h : Eq.{u_4 + 1} (α := N)
  (∑ i : ι,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((fun (i : ι) ↦
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) (↑x : M) : N →ₗ[R] R) : (a : N) → R)
              ((P.coroot : (a : ι) → N) i : N) :
            R))
        i)
      ((P.coroot : (a : ι) → N) i : N))
  (∑ i : ι,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
      ((P.coroot : (a : ι) → N) i : N))
Tactic: use fun i => P.toLinearMap x (P.coroot i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
⊢ Submodule.map (↑P.toPerfPair.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R)) ≤
    LinearMap.ker P.RootForm
have rw : ⨅ (i : ι), LinearMap.ker (P.coroot' i) ≤ LinearMap.ker P.RootForm
Tactic: rw [P.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Fintype ι
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), LinearMap.ker (P.coroot' i)) x
⊢ x ∈ LinearMap.ker P.RootForm
have h : ∀ (y : M),
  Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((0 : (a : M) → R) y : R)
Tactic: ext y
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
x : ↥(P.rootSpan S)
⊢ Eq.{u_4 + 1} (α := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) x : N)
    ((P.Polarization : (a : M) → N) (↑x : M) : N)
have simp : Eq.{u_4 + 1} (α := N)
  (∑ x_1 : ι,
    HSMul.hSMul.{u_5, u_4, u_4} (α := S) (β := N) ((P.coroot'In S x_1 : (a : ↥(P.rootSpan S)) → S) x : S)
      ((P.coroot : (a : ι) → N) x_1 : N))
  (∑ i : ι,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.coroot' i : (a : M) → R) (↑x : M) : R)
      ((P.coroot : (a : ι) → N) i : N))
Tactic: simp only [PolarizationIn, LinearMap.coe_sum, LinearMap.coe_comp, Finset.sum_apply, comp_apply,
    LinearMap.toSpanSingleton_apply, Polarization_apply]