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 ≠ ⊥
k : ↥b.support
hk : p k
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := 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})
    ((P.root : (a : ι) → M) (↑k : ι) : M)

Tactic:
simpa
-- 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 ≠ ⊥
k : ↥b.support
refine : ∀ (hk : Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M)), p k
⊢ Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k

Tactic:
refine ⟨fun hk ↦ ?_, fun hk ↦ subset_span <| by simpa⟩
-- 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 ≠ ⊥
k : ↥b.support
hk : Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M)
contrapose : ∀ (hk : ¬p k), ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q
⊢ p k

Tactic:
contrapose 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 ≠ ⊥
k : ↥b.support
hk : ¬p k
⊢ ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q

Tactic:
b.linearIndepOn_root.linearIndependent.notMem_span_image hk

Premises used: Set.Mem, LinearIndepOn.linearIndependent, setOf, RootPairing.Base.linearIndepOn_root, LinearIndependent.notMem_span_image
-- 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 ≠ ⊥
k : ↥b.support
hk : ¬p k
⊢ ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q

Tactic:
exact b.linearIndepOn_root.linearIndependent.notMem_span_image hk

Premises used: LinearIndepOn.linearIndependent, RootPairing.Base.linearIndepOn_root, LinearIndependent.notMem_span_image
-- 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 ≠ ⊥
⊢ ∀ (k : ↥b.support), Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M) ↔ p k

Tactic:
have hq_mem (k : b.support) : P.root k ∈ q ↔ p k := by
    refine ⟨fun hk ↦ ?_, fun hk ↦ subset_span <| by simpa⟩
    contrapose hk
    exact b.linearIndepOn_root.linearIndependent.notMem_span_image 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
k : ↥b.support
hk : ((P.root : (a : ι) → M) (↑k : ι) : M) ∉ q
⊢ q ≤ LinearMap.ker (P.coroot' (↑k : ι))

Tactic:
fun x hx ↦ LinearMap.mem_ker.mpr ?_

Premises used: Iff.mpr, LinearMap.mem_ker
-- 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
refine : ∀ (x : M) (hx : x ∈ q), Eq.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R)
⊢ q ≤ LinearMap.ker (P.coroot' (↑k : ι))

Tactic:
refine fun x hx ↦ LinearMap.mem_ker.mpr ?_

Premises used: Iff.mpr, LinearMap.mem_ker
-- 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
x : M
hx : x ∈ q
contrapose! :
  ∀ (hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R)),
    Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M)
⊢ Eq.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R)

Tactic:
contrapose! 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
k : ↥b.support
x : M
hx : x ∈ q
hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R)
rw : p k
⊢ Membership.mem (α := M) q ((P.root : (a : ι) → M) (↑k : ι) : M)

Tactic:
rw [hq_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
k : ↥b.support
x_1 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)
⊢ ∃ (l : ↥b.support), p l ∧ (P.root : (a : ι) → M) (↑l : ι) = x

Tactic:
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
k : ↥b.support
x_1 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)
mem :
  ∀ (l : ↥b.support) (hl : p l)
    (hx :
      Membership.mem.{u_3, u_3} (α := M) (γ := 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})
        ((P.root : (a : ι) → M) (↑l : ι) : M))
    (hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) ((P.root : (a : ι) → M) (↑l : ι) : M) : R) (0 : R)),
    p k
⊢ p k

Tactic:
obtain ⟨l, hl, rfl⟩ : ∃ l : b.support, p l ∧ P.root l = x := by 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
x : M
l : ↥b.support
hl : p l
hx :
  Membership.mem.{u_3, u_3} (α := M) (γ := 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})
    ((P.root : (a : ι) → M) (↑l : ι) : M)
hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) ((P.root : (a : ι) → M) (↑l : ι) : M) : R) (0 : R)
rwa : ¬b.cartanMatrix k l = 0
rwa₁ : ¬b.cartanMatrix l k = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ¬P.pairing (↑l : ι) (↑k : ι) = 0
⊢ b.cartanMatrix k l ≠ 0

Tactic:
rwa [ne_eq, cartanMatrix_apply_eq_zero_iff_symm, cartanMatrix_apply_eq_zero_iff_pairing]

Premises used: RootPairing.Base.cartanMatrix_apply_eq_zero_iff_pairing, ne_eq, RootPairing.Base.cartanMatrix_apply_eq_zero_iff_symm
-- 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
l : ↥b.support
hl : p l
hx :
  Membership.mem.{u_3, u_3} (α := M) (γ := 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})
    ((P.root : (a : ι) → M) (↑l : ι) : M)
hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) ((P.root : (a : ι) → M) (↑l : ι) : M) : R) (0 : R)
mem : ∀ (hk : b.cartanMatrix k l ≠ 0), p k
⊢ p k

Tactic:
replace hk : b.cartanMatrix k l ≠ 0 := by
        rwa [ne_eq, cartanMatrix_apply_eq_zero_iff_symm, cartanMatrix_apply_eq_zero_iff_pairing]
-- 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
l : ↥b.support
hl : p l
hx :
  Membership.mem.{u_3, u_3} (α := M) (γ := 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})
    ((P.root : (a : ι) → M) (↑l : ι) : M)
hk : b.cartanMatrix k l ≠ 0
⊢ p k

Tactic:
tauto
-- 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
hk : Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) 0 : R) (0 : R)
⊢ p k

Tactic:
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
k : ↥b.support
x_1 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)
by_contra! :
  ∀
    (contra :
      Eq.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R) ∧
        Eq.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) y : R) (0 : R)),
    False
⊢ Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R) ∨
    Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) y : R) (0 : R)

Tactic:
by_contra! contra
-- 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_1 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)
contra :
  Eq.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R) ∧
    Eq.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) y : R) (0 : R)
⊢ False

Tactic:
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
k : ↥b.support
x_1 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)
add :
  ∀
    (hk :
      Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) x : R) (0 : R) ∨
        Ne.{u_2 + 1} (α := R) ((P.coroot' (↑k : ι) : (a : M) → R) y : R) (0 : R)),
    p k
⊢ p k

Tactic:
replace hk : P.coroot' k x ≠ 0 ∨ P.coroot' k y ≠ 0 := by by_contra! contra; 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
k : ↥b.support
x_1 : M
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

Tactic:
simp_all