awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
k : ↥b.support
x : M
hx : x ∈ q
hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R)
mem :
  ∀ (x : M)
    (hx :
      Membership.mem (γ := Set M)
        (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
          {i : ↥b.support | p i})
        x)
    (hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R)), p k
zero : ∀ (hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) 0 : R) (0 : R)), p k
add :
  ∀ (x y : M)
    (hx :
      Membership.mem (γ := Submodule R M)
        (span R
          (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
            {i : ↥b.support | p i}))
        x)
    (hy :
      Membership.mem (γ := Submodule R M)
        (span R
          (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
            {i : ↥b.support | p i}))
        y)
    (hx' : ∀ (hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R)), p k)
    (hy' : ∀ (hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) y : R) (0 : R)), p k)
    (hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) (x + y) : R) (0 : R)), p k
smul :
  ∀ (a : R) (x : M)
    (hx :
      Membership.mem (γ := Submodule R M)
        (span R
          (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
            {i : ↥b.support | p i}))
        x)
    (hx' : ∀ (hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R)), p k)
    (hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) (a • x) : R) (0 : R)), p k
⊢ p k

Tactic:
induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨l, hl, rfl⟩ : ∃ l : b.support, p l ∧ P.root l = x := by simp_all
      replace hk : b.cartanMatrix k l ≠ 0 := by
        rwa [ne_eq, cartanMatrix_apply_eq_zero_iff_symm, cartanMatrix_apply_eq_zero_iff_pairing]
      tauto
    | zero => simp_all
    | add x y hx hy hx' hy' =>
      replace hk : P.coroot' k x ≠ 0 ∨ P.coroot' k y ≠ 0 := by by_contra! contra; simp_all
      tauto
    | smul a x hx hx' => simp_all

Premises used: RootPairing.Base.support, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
⊢ ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))

Tactic:
have hq_notMem (k : b.support) (hk : P.root k ∉ q) : q ≤ LinearMap.ker (P.coroot' k) := by
    refine fun x hx ↦ LinearMap.mem_ker.mpr ?_
    contrapose! hk
    rw [hq_mem]
    induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨l, hl, rfl⟩ : ∃ l : b.support, p l ∧ P.root l = x := by simp_all
      replace hk : b.cartanMatrix k l ≠ 0 := by
        rwa [ne_eq, cartanMatrix_apply_eq_zero_iff_symm, cartanMatrix_apply_eq_zero_iff_pairing]
      tauto
    | zero => simp_all
    | add x y hx hy hx' hy' =>
      replace hk : P.coroot' k x ≠ 0 ∨ P.coroot' k y ≠ 0 := by by_contra! contra; simp_all
      tauto
    | smul a x hx hx' => simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
rw : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
⊢ ∀ (k : ι), q ∈ invtSubmodule (↑(P.reflection k) : M →ₗ[R] M)

Tactic:
rw [← b.forall_mem_support_invtSubmodule_iff]

Premises used: RootPairing.Base.forall_mem_support_invtSubmodule_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
⊢ ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
fun k hkb ↦ (mem_invtSubmodule _).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Module.End.mem_invtSubmodule, LinearEquiv.toLinearMap, RootPairing.reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
refine : ∀ (k : ι) (hkb : k ∈ b.support) (x : M) (hx : x ∈ q), x ∈ Submodule.comap (↑(P.reflection k) : M →ₗ[R] M) q
⊢ ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
refine fun k hkb ↦ (mem_invtSubmodule _).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Module.End.mem_invtSubmodule
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
rw :
  x - HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' k : (a : M) → R) x : R) ((P.root : (a : ι) → M) k : M) ∈
    q
⊢ x ∈ Submodule.comap (↑(P.reflection k) : M →ₗ[R] M) q

Tactic:
rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply]

Premises used: Submodule.mem_comap, RootPairing.reflection_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
apply :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' k : (a : M) → R) x : R) ((P.root : (a : ι) → M) k : M) ∈ q
⊢ x - HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' k : (a : M) → R) x : R) ((P.root : (a : ι) → M) k : M) ∈
    q

Tactic:
apply q.sub_mem hx

Premises used: Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
pos :
  ∀ (hk : Membership.mem (α := M) q ((P.root : (a : ι) → M) k : M)),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' k : (a : M) → R) x : R) ((P.root : (a : ι) → M) k : M) ∈ q
neg :
  ∀ (hk : ((P.root : (a : ι) → M) k : M) ∉ q),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' k : (a : M) → R) x : R) ((P.root : (a : ι) → M) k : M) ∈ q
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' k : (a : M) → R) x : R) ((P.root : (a : ι) → M) k : M) ∈ q

Tactic:
by_cases hk : P.root k ∈ q

Premises used: RootPairing.root, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
hk : Membership.mem (α := M) q ((P.root : (a : ι) → M) k : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' k : (a : M) → R) x : R) ((P.root : (a : ι) → M) k : M) ∈ q

Tactic:
q.smul_mem _ hk

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
hk : Membership.mem (α := M) q ((P.root : (a : ι) → M) k : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' k : (a : M) → R) x : R) ((P.root : (a : ι) → M) k : M) ∈ q

Tactic:
exact q.smul_mem _ hk

Premises used: Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
hk : ((P.root : (a : ι) → M) k : M) ∉ q
⊢ Eq.{u_2 + 1} (α := R) ((P.coroot' k : (a : M) → R) x : R) (0 : R)

Tactic:
replace hk : P.coroot' k x = 0 := hq_notMem ⟨k, hkb⟩ hk hx
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
hk : Eq.{u_2 + 1} (α := R) ((P.coroot' k : (a : M) → R) x : R) (0 : R)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' k : (a : M) → R) x : R) ((P.root : (a : ι) → M) k : M) ∈ q

Tactic:
simp [hk]
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
⊢ ∀ (k : ι), q ∈ invtSubmodule (↑(P.reflection k) : M →ₗ[R] M)

Tactic:
have hq : ∀ k, q ∈ invtSubmodule (P.reflection k) := by
    rw [← b.forall_mem_support_invtSubmodule_iff]
    refine fun k hkb ↦ (mem_invtSubmodule _).mpr fun x hx ↦ ?_
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply]
    apply q.sub_mem hx
    by_cases hk : P.root k ∈ q
    · exact q.smul_mem _ hk
    · replace hk : P.coroot' k x = 0 := hq_notMem ⟨k, hkb⟩ hk hx
      simp [hk]
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
b : P.Base
inst_5 : P.IsCrystallographic
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : Finite ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M :=
  span R
    (image.{u_1, u_3} (α := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))
      {i : ↥b.support | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k
hq_notMem : ∀ (k : ↥b.support) (hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q), q ≤ LinearMap.ker (P.coroot' (↑k : ι))
hq : ∀ (k : ι), q ∈ invtSubmodule (↑(P.reflection k) : M →ₗ[R] M)
⊢ p j

Tactic:
simp [← hq_mem, IsIrreducible.eq_top_of_invtSubmodule_reflection q hq hq₀]

Premises used: RootPairing.IsIrreducible.eq_top_of_invtSubmodule_reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
obtain :
  ∀ (f : ι → ℤ)
    (hf :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)),
    i = j
⊢ i = j

Tactic:
obtain ⟨f, -, -, hf⟩ := b.exists_root_eq_sum_int i

Premises used: RootPairing.Base.exists_root_eq_sum_int
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
obtain :
  ∀ (g : ι → ℤ)
    (hg :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)),
    i = j
⊢ i = j

Tactic:
obtain ⟨g, -, -, hg⟩ := b.exists_root_eq_sum_int j

Premises used: RootPairing.Base.exists_root_eq_sum_int
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
this : f' = g'
rw :
  Eq.{u_3 + 1} (α := M) (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M))
⊢ i = j

Tactic:
rw [← P.root.apply_eq_iff_eq, hf, hg]

Premises used: RootPairing.root, Function.Embedding.apply_eq_iff_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
this : f' = g'
⊢ Eq.{u_3 + 1} (α := M) (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M))

Tactic:
Finset.sum_congr rfl fun k hk ↦ ?_

Premises used: Finset.sum_congr, rfl