awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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) : ι₂))
have 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₂)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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
⊢ 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₂)
have suffices : P₂.pairing (↑((e : (a : ↥b.support) → ↥b₂.support) j) : ι₂) (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂) =
  P.pairing (↑j : ι) (↑k : ι)
Tactic: suffices P₂.pairing (e j) (e k) = P.pairing j k by simp [reflection_apply, hf, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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
⊢ 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₂)
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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) : ι₂))
⊢ 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₂)
have 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₂)
Tactic: obtain ⟨i, rfl⟩ := hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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 : ι
⊢ 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₂)
have 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₂)
Tactic: apply b.induction_reflect i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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₂)
⊢ 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₂)
have 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₂)
Tactic: apply b.induction_reflect i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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₂)
⊢ 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₂)
have 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₂)
Tactic: apply b.induction_reflect i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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 : ι
⊢ 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₂)
have 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₂)
Tactic: ⟨l, hl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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
⊢ 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₂)
have 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₂)
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)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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₂)
⊢ 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₂)
have 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₂)
Tactic: rw [root_reflectionPerm, this, ← hl, ← root_reflectionPerm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
P_1 : RootPairing ι R M N
inst_7 : P_1.IsValuedIn S
b_1 : P_1.Base
inst_8 : P_1.IsCrystallographic
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst_12 : AddCommGroup M₂
inst_13 : Module R M₂
inst_14 : AddCommGroup N₂
inst_15 : Module R N₂
P : RootPairing ι R M N
inst_16 : P.IsRootSystem
inst_17 : P.IsCrystallographic
inst_18 : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst_19 : P₂.IsCrystallographic
b₂ : P₂.Base
e : Equiv.{u_1 + 1, u_6 + 1} ↥b.support ↥b₂.support
inst_20 : Finite ι₂
inst_21 : P₂.IsRootSystem
inst_22 : P₂.IsReduced
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
f : M ≃ₗ[R] M₂ := b.toWeightBasis.equiv b₂.toWeightBasis e
⊢ ∀ (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₂) ↔
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
have refine_1 : ∀ (m : M)
  (h :
    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₂)),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
Tactic: refine fun m ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
P_1 : RootPairing ι R M N
inst_7 : P_1.IsValuedIn S
b_1 : P_1.Base
inst_8 : P_1.IsCrystallographic
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst_12 : AddCommGroup M₂
inst_13 : Module R M₂
inst_14 : AddCommGroup N₂
inst_15 : Module R N₂
P : RootPairing ι R M N
inst_16 : P.IsRootSystem
inst_17 : P.IsCrystallographic
inst_18 : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst_19 : P₂.IsCrystallographic
b₂ : P₂.Base
e : Equiv.{u_1 + 1, u_6 + 1} ↥b.support ↥b₂.support
inst_20 : Finite ι₂
inst_21 : P₂.IsRootSystem
inst_22 : P₂.IsReduced
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
f : M ≃ₗ[R] M₂ := b.toWeightBasis.equiv b₂.toWeightBasis e
refine_1 :
  ∀ (m : M)
    (h :
      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₂)),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
⊢ ∀ (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₂) ↔
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
have refine_2 : ∀ (m : M) (h : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → 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: refine fun m ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩