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
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
suffices :
  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:
suffices P₂.pairing (e j) (e k) = P.pairing j k by simp [reflection_apply, hf, this]
-- 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
⊢ P₂.pairing (↑((e : (a : ↥b.support) → ↥b₂.support) j) : ι₂) (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂) =
    P.pairing (↑j : ι) (↑k : ι)

Tactic:
simpa only [cartanMatrixIn_def, algebraMap_pairingIn] using congr_arg (algebraMap ℤ R) (he j k)

Premises used: RootPairing.Base.cartanMatrixIn_def, Algebra.algebraMap, RootPairing.algebraMap_pairingIn, Int, congr_arg, 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
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),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))

Tactic:
have (k : b.support) : (P.reflection k).trans f = f.trans (P₂.reflection (e k)) := by
    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
    intro j
    suffices P₂.pairing (e j) (e k) = P.pairing j k by simp [reflection_apply, hf, this]
    simpa only [cartanMatrixIn_def, algebraMap_pairingIn] using congr_arg (algebraMap ℤ R) (he j k)
-- 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
this :
  ∀ (k : ↥b.support),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
obtain :
  ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
      ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
⊢ Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
    ((f : (a : M) → M₂) m : M₂)

Tactic:
obtain ⟨i, rfl⟩ := hm

Premises used: 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
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₂)
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
this :
  ∀ (k : ↥b.support),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
i : ι
h₀ :
  ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂) →
      Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι) : M) : M₂)
h₁ :
  ∀ i ∈ b.support,
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
      ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
h₂ :
  ∀ (i j : ι),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂) →
      j ∈ b.support →
        Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
          ((f : (a : M) → M₂) ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) i : ι) : M) : M₂)
⊢ Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
    ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)

Tactic:
apply b.induction_reflect i

Premises used: RootPairing.Base.induction_reflect
-- 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₂)
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
this :
  ∀ (k : ↥b.support),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
i j : ι
h :
  Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
    ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂)
k : ι₂
hk : Eq.{u_7 + 1} (α := M₂) ((P₂.root : (a : ι₂) → M₂) k : M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂)
⊢ Eq.{u_7 + 1} (α := M₂) ((P₂.root : (a : ι₂) → M₂) ((P₂.reflectionPerm k : (a : ι₂) → ι₂) k : ι₂) : M₂)
    ((f : (a : M) → M₂) ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : M) : 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
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₂)
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
this :
  ∀ (k : ↥b.support),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
i : ι
⊢ ∀ (i : ι),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂) →
      Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι) : M) : M₂)

Tactic:
exact fun j ⟨k, hk⟩ ↦ ⟨P₂.reflectionPerm k k, 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
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₂)
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
this :
  ∀ (k : ↥b.support),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
i : ι
⊢ ∀ i ∈ b.support,
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
      ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)

Tactic:
fun j hj ↦ ⟨e ⟨j, hj⟩, (hf _).symm⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, Set.range, Eq.symm, Subtype.val, 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
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₂)
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
this :
  ∀ (k : ↥b.support),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
i : ι
⊢ ∀ i ∈ b.support,
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
      ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)

Tactic:
exact fun j hj ↦ ⟨e ⟨j, hj⟩, (hf _).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
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₂)
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
this :
  ∀ (k : ↥b.support),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
i j k : ι
h₂ :
  ∀ (l : ι₂)
    (hl :
      Eq.{u_7 + 1} (α := M₂) ((P₂.root : (a : ι₂) → M₂) l : M₂)
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂)),
    k ∈ b.support →
      Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) ((P.reflectionPerm k : (a : ι) → ι) j : ι) : M) : M₂)
⊢ Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
      ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂) →
    k ∈ b.support →
      Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) ((P.reflectionPerm k : (a : ι) → ι) j : ι) : M) : M₂)

Tactic:
⟨l, hl⟩
-- 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₂)
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
this :
  ∀ (k : ↥b.support),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
i j k : ι
l : ι₂
hl : Eq.{u_7 + 1} (α := M₂) ((P₂.root : (a : ι₂) → M₂) l : M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂)
hk : k ∈ b.support
⊢ Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.reflection k : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M) : M₂)
    ((P₂.reflection
            (↑((e : (a : ↥b.support) → ↥b₂.support) (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) k hk)) : ι₂) :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂) :
      M₂)

Tactic:
simpa using LinearEquiv.congr_fun (this ⟨k, hk⟩) (P.root j)

Premises used: Subtype.mk, RootPairing.root, LinearEquiv.congr_fun, 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
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₂)
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
this :
  ∀ (k : ↥b.support),
    Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
      (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
i j k : ι
l : ι₂
hl : Eq.{u_7 + 1} (α := M₂) ((P₂.root : (a : ι₂) → M₂) l : M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂)
hk : k ∈ b.support
⊢ Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.reflection k : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M) : M₂)
    ((P₂.reflection
            (↑((e : (a : ↥b.support) → ↥b₂.support) (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) k hk)) : ι₂) :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂) :
      M₂)

Tactic:
replace this : f (P.reflection k (P.root j)) = (P₂.reflection (e ⟨k, hk⟩)) (f (P.root j)) := by
      simpa using LinearEquiv.congr_fun (this ⟨k, hk⟩) (P.root 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₂)
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
i j k : ι
l : ι₂
hl : Eq.{u_7 + 1} (α := M₂) ((P₂.root : (a : ι₂) → M₂) l : M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂)
hk : k ∈ b.support
this :
  Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.reflection k : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M) : M₂)
    ((P₂.reflection
            (↑((e : (a : ↥b.support) → ↥b₂.support) (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) k hk)) : ι₂) :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) ((P.root : (a : ι) → M) j : M) : M₂) :
      M₂)
h₂ :
  Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
    ((P₂.root : (a : ι₂) → M₂)
        ((P₂.reflectionPerm
                (↑((e : (a : ↥b.support) → ↥b₂.support) (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) k hk)) : ι₂) :
              (a : ι₂) → ι₂)
            l :
          ι₂) :
      M₂)
⊢ Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂))
    ((f : (a : M) → M₂) ((P.root : (a : ι) → M) ((P.reflectionPerm k : (a : ι) → ι) j : ι) : M) : M₂)

Tactic:
rw [root_reflectionPerm, this, ← hl, ← root_reflectionPerm]

Premises used: RootPairing.root_reflectionPerm