awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i : ι
inl :
  ∀ (j : ι) (hj : j ∈ b.support) (hj₀ : P.pairingIn ℤ j i ≠ 0),
    ∃ x ∈ p, Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) x : K) (0 : K)
⊢ ∃ x ∈ p, Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) x : K) (0 : K)

Tactic:
obtain ⟨j, hj, hj₀⟩ := b.exists_mem_support_pos_pairingIn_ne_zero i

Premises used: RootPairing.Base.exists_mem_support_pos_pairingIn_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
hj : j ∈ b.support
hj₀ : P.pairingIn ℤ j i ≠ 0
⊢ ∃ x ∈ p, Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) x : K) (0 : K)

Tactic:
⟨fun i ↦ P.pairingIn ℤ i j, subset_span ⟨⟨j, hj⟩, rfl⟩, ?_⟩

Premises used: Int.cast, RootPairing.pairingIn, Int, Subtype.mk, And.intro, Exists.intro, Submodule.subset_span, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
hj : j ∈ b.support
hj₀ : P.pairingIn ℤ j i ≠ 0
inl :
  Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) fun (i : ι) ↦ (↑(P.pairingIn ℤ i j) : K) : K) (0 : K)
⊢ ∃ x ∈ p, Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) x : K) (0 : K)

Tactic:
refine ⟨fun i ↦ P.pairingIn ℤ i j, subset_span ⟨⟨j, hj⟩, rfl⟩, ?_⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
hj : j ∈ b.support
hj₀ : P.pairingIn ℤ j i ≠ 0
⊢ ¬P.pairingIn ℤ i j = 0

Tactic:
rw [ne_eq, P.pairingIn_eq_zero_iff] at hj₀

Premises used: ne_eq, RootPairing.pairingIn_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
hj : j ∈ b.support
hj₀ : ¬P.pairingIn ℤ i j = 0
⊢ Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) fun (i : ι) ↦ (↑(P.pairingIn ℤ i j) : K) : K) (0 : K)

Tactic:
simpa [f, ne_eq, Int.cast_eq_zero]

Premises used: ne_eq, Int.cast_eq_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
h : i ≠ j
contrapose! : ∀ (h : ∀ (k : ι) (_ : k ∈ b.support), P.pairingIn ℤ i k = P.pairingIn ℤ j k), i = j
⊢ ∃ k ∈ b.support, P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k

Tactic:
contrapose! h
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
h : ∀ (k : ι) (_ : k ∈ b.support), P.pairingIn ℤ i k = P.pairingIn ℤ j k
a :
  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)
⊢ i = j

Tactic:
apply b.injective_pairingIn

Premises used: RootPairing.Base.injective_pairingIn
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
h : ∀ (k : ι) (_ : k ∈ b.support), P.pairingIn ℤ i k = P.pairingIn ℤ j k
⊢ 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)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
h : i ≠ j
inr :
  ∀ (k : ι) (hk : k ∈ b.support) (hk' : P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k),
    ∃ x ∈ p,
      Ne.{u_6 + 1} (α := K)
        ((f
                (Sum.inr
                  (Subtype.mk (p := fun (x : ι × ι) ↦
                    Membership.mem (γ := Set (ι × ι))
                      {x : ι × ι |
                        match (motive := ι × ι → Prop) x with
                        | (i, j) => i ≠ j}
                      x)
                    (i, j) h)) :
              (a : (j : ι) → K) → K)
            x :
          K)
        (0 : K)
⊢ ∃ x ∈ p,
    Ne.{u_6 + 1} (α := K)
      ((f
              (Sum.inr
                (Subtype.mk (p := fun (x : ι × ι) ↦
                  Membership.mem (γ := Set (ι × ι))
                    {x : ι × ι |
                      match (motive := ι × ι → Prop) x with
                      | (i, j) => i ≠ j}
                    x)
                  (i, j) h)) :
            (a : (j : ι) → K) → K)
          x :
        K)
      (0 : K)

Tactic:
obtain ⟨k, hk, hk'⟩ : ∃ k ∈ b.support, P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k := by
      contrapose! h
      apply b.injective_pairingIn
      aesop

Premises used: RootPairing.Base.support
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
h : i ≠ j
k : ι
hk : k ∈ b.support
hk' : P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k
⊢ ¬Eq.{u_6 + 1} (α := K) ((fun (i : ι) ↦ ((↑(P.pairingIn ℤ i k) : K) : K)) i)
      ((fun (i : ι) ↦ ((↑(P.pairingIn ℤ i k) : K) : K)) j)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
i j : ι
h : i ≠ j
k : ι
hk : k ∈ b.support
hk' : P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k
⊢ ∃ x ∈ p,
    Ne.{u_6 + 1} (α := K)
      ((f
              (Sum.inr
                (Subtype.mk (p := fun (x : ι × ι) ↦
                  Membership.mem (γ := Set (ι × ι))
                    {x : ι × ι |
                      match (motive := ι × ι → Prop) x with
                      | (i, j) => i ≠ j}
                    x)
                  (i, j) h)) :
            (a : (j : ι) → K) → K)
          x :
        K)
      (0 : K)

Tactic:
simpa [f, sub_eq_zero] using ⟨fun i ↦ P.pairingIn ℤ i k, subset_span ⟨⟨k, hk⟩, rfl⟩, by simpa⟩

Premises used: sub_eq_zero
-- 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 ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : AddCommGroup N₂
inst_11 : Module R N₂
P : RootPairing ι R M N
inst_12 : P.IsRootSystem
inst_13 : P.IsCrystallographic
inst_14 : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst_15 : P₂.IsCrystallographic
b₂ : P₂.Base
e : Equiv.{u_1 + 1, u_6 + 1} ↥b.support ↥b₂.support
f : M ≃ₗ[R] M₂
hf :
  ∀ (i : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑i : ι) : M) : M₂)
      ((P₂.root : (a : ι₂) → M₂) (↑((e : (a : ↥b.support) → ↥b₂.support) i) : ι₂) : M₂)
m : M
hm : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
he :
  ∀ (i j : ↥b.support),
    b₂.cartanMatrix ((e : (a : ↥b.support) → ↥b₂.support) i) ((e : (a : ↥b.support) → ↥b₂.support) j) =
      b.cartanMatrix i j
k : ↥b.support
this :
  ∀ (j : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((P.reflection (↑k : ι) ≪≫ₗ f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑j : ι) : M) : M₂)
      ((f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂) : (a : M) → M₂)
          ((P.root : (a : ι) → M) (↑j : ι) : M) :
        M₂)
rw :
  (↑(P.reflection (↑k : ι) ≪≫ₗ f) : M →ₗ[R] M₂) =
    (↑(f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂)) : M →ₗ[R] M₂)
⊢ Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
    (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))

Tactic:
rw [← LinearEquiv.toLinearMap_inj]

Premises used: LinearEquiv.toLinearMap_inj
-- 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 ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : AddCommGroup N₂
inst_11 : Module R N₂
P : RootPairing ι R M N
inst_12 : P.IsRootSystem
inst_13 : P.IsCrystallographic
inst_14 : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst_15 : P₂.IsCrystallographic
b₂ : P₂.Base
e : Equiv.{u_1 + 1, u_6 + 1} ↥b.support ↥b₂.support
f : M ≃ₗ[R] M₂
hf :
  ∀ (i : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑i : ι) : M) : M₂)
      ((P₂.root : (a : ι₂) → M₂) (↑((e : (a : ↥b.support) → ↥b₂.support) i) : ι₂) : M₂)
m : M
hm : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
he :
  ∀ (i j : ↥b.support),
    b₂.cartanMatrix ((e : (a : ↥b.support) → ↥b₂.support) i) ((e : (a : ↥b.support) → ↥b₂.support) j) =
      b.cartanMatrix i j
k : ↥b.support
this :
  ∀ (j : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((P.reflection (↑k : ι) ≪≫ₗ f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑j : ι) : M) : M₂)
      ((f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂) : (a : M) → M₂)
          ((P.root : (a : ι) → M) (↑j : ι) : M) :
        M₂)
j : ↥b.support
⊢ Eq.{u_7 + 1} (α := M₂)
    (((↑(P.reflection (↑k : ι) ≪≫ₗ f) : M →ₗ[R] M₂) : (a : M) → M₂) ((b.toWeightBasis : (a : ↥b.support) → M) j : M) :
      M₂)
    (((↑(f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂)) : M →ₗ[R] M₂) : (a : M) → M₂)
        ((b.toWeightBasis : (a : ↥b.support) → M) j : M) :
      M₂)

Tactic:
simpa using this j
-- 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 ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : AddCommGroup N₂
inst_11 : Module R N₂
P : RootPairing ι R M N
inst_12 : P.IsRootSystem
inst_13 : P.IsCrystallographic
inst_14 : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst_15 : P₂.IsCrystallographic
b₂ : P₂.Base
e : Equiv.{u_1 + 1, u_6 + 1} ↥b.support ↥b₂.support
f : M ≃ₗ[R] M₂
hf :
  ∀ (i : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑i : ι) : M) : M₂)
      ((P₂.root : (a : ι₂) → M₂) (↑((e : (a : ↥b.support) → ↥b₂.support) i) : ι₂) : M₂)
m : M
hm : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
he :
  ∀ (i j : ↥b.support),
    b₂.cartanMatrix ((e : (a : ↥b.support) → ↥b₂.support) i) ((e : (a : ↥b.support) → ↥b₂.support) j) =
      b.cartanMatrix i j
k : ↥b.support
this :
  ∀ (j : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((P.reflection (↑k : ι) ≪≫ₗ f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑j : ι) : M) : M₂)
      ((f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂) : (a : M) → M₂)
          ((P.root : (a : ι) → M) (↑j : ι) : M) :
        M₂)
⊢ (↑(P.reflection (↑k : ι) ≪≫ₗ f) : M →ₗ[R] M₂) =
    (↑(f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂)) : M →ₗ[R] M₂)

Tactic:
exact b.toWeightBasis.ext fun j ↦ by simpa using this j

Premises used: RootPairing.Base.toWeightBasis, Module.Basis.ext
-- 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 ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : AddCommGroup N₂
inst_11 : Module R N₂
P : RootPairing ι R M N
inst_12 : P.IsRootSystem
inst_13 : P.IsCrystallographic
inst_14 : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst_15 : P₂.IsCrystallographic
b₂ : P₂.Base
e : Equiv.{u_1 + 1, u_6 + 1} ↥b.support ↥b₂.support
f : M ≃ₗ[R] M₂
hf :
  ∀ (i : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑i : ι) : M) : M₂)
      ((P₂.root : (a : ι₂) → M₂) (↑((e : (a : ↥b.support) → ↥b₂.support) i) : ι₂) : M₂)
m : M
hm : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
he :
  ∀ (i j : ↥b.support),
    b₂.cartanMatrix ((e : (a : ↥b.support) → ↥b₂.support) i) ((e : (a : ↥b.support) → ↥b₂.support) j) =
      b.cartanMatrix i j
k : ↥b.support
suffices :
  ∀ (j : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((P.reflection (↑k : ι) ≪≫ₗ f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑j : ι) : M) : M₂)
      ((f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂) : (a : M) → M₂)
          ((P.root : (a : ι) → M) (↑j : ι) : M) :
        M₂)
⊢ Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
    (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))

Tactic:
suffices ∀ j : b.support,
        (P.reflection k).trans f (P.root j) = f.trans (P₂.reflection (e k)) (P.root j) by
      rw [← LinearEquiv.toLinearMap_inj]
      exact b.toWeightBasis.ext fun j ↦ by simpa using this j
-- 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 ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : AddCommGroup N₂
inst_11 : Module R N₂
P : RootPairing ι R M N
inst_12 : P.IsRootSystem
inst_13 : P.IsCrystallographic
inst_14 : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst_15 : P₂.IsCrystallographic
b₂ : P₂.Base
e : Equiv.{u_1 + 1, u_6 + 1} ↥b.support ↥b₂.support
f : M ≃ₗ[R] M₂
hf :
  ∀ (i : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑i : ι) : M) : M₂)
      ((P₂.root : (a : ι₂) → M₂) (↑((e : (a : ↥b.support) → ↥b₂.support) i) : ι₂) : M₂)
m : M
hm : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
he :
  ∀ (i j : ↥b.support),
    b₂.cartanMatrix ((e : (a : ↥b.support) → ↥b₂.support) i) ((e : (a : ↥b.support) → ↥b₂.support) j) =
      b.cartanMatrix i j
k j : ↥b.support
this :
  P₂.pairing (↑((e : (a : ↥b.support) → ↥b₂.support) j) : ι₂) (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂) =
    P.pairing (↑j : ι) (↑k : ι)
⊢ Eq.{u_7 + 1} (α := M₂) ((P.reflection (↑k : ι) ≪≫ₗ f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑j : ι) : M) : M₂)
    ((f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂) : (a : M) → M₂)
        ((P.root : (a : ι) → M) (↑j : ι) : M) :
      M₂)

Tactic:
simp [reflection_apply, hf, this]

Premises used: RootPairing.reflection_apply