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₂)
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₂))
    ((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:
mem_range_self _

Premises used: Set.mem_range_self
-- 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₂)
⊢ 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:
exact mem_range_self _

Premises used: Set.mem_range_self
-- 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
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

Tactic:
fun m ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
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
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₂)
⊢ ∀ (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

Tactic:
refine fun m ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
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
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₂)
⊢ ∀ (i : ↥b₂.support),
    Eq.{u_3 + 1} (α := M) ((f.symm : (a : M₂) → M) ((P₂.root : (a : ι₂) → M₂) (↑i : ι₂) : M₂) : M)
      ((P.root : (a : ι) → M) (↑((e.symm : (a : ↥b₂.support) → ↥b.support) i) : ι) : M)

Tactic:
simp [f, Module.Basis.equiv]

Premises used: Module.Basis.equiv
-- 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
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
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₂)
⊢ ∀ (i j : ↥b₂.support),
    b.cartanMatrix ((e.symm : (a : ↥b₂.support) → ↥b.support) i) ((e.symm : (a : ↥b₂.support) → ↥b.support) j) =
      b₂.cartanMatrix i j

Tactic:
simp [(he _ _).symm]

Premises used: Eq.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
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
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:
simpa using apply_mem_range_root_of_cartanMatrixEq _ b e.symm f.symm
        (by simp [f, Module.Basis.equiv]) (f m) h (by simp [(he _ _).symm])

Premises used: LinearEquiv.symm, RootPairing.Base.apply_mem_range_root_of_cartanMatrixEq, Equiv.symm, 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
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
h : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
⊢ ∀ (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₂)

Tactic:
simp [f, Module.Basis.equiv]

Premises used: Module.Basis.equiv
-- 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
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
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:
exact apply_mem_range_root_of_cartanMatrixEq b b₂ e f (by simp [f, Module.Basis.equiv]) m h he

Premises used: RootPairing.Base.apply_mem_range_root_of_cartanMatrixEq
-- 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
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
hf :
  ∀ (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
this_1 : Fintype ι := Fintype.ofFinite ι
this_2 : Fintype ι₂ := Fintype.ofFinite ι₂
this_3 : DecidableEq M
this : DecidableEq M₂
e' : ι ≃ ι₂ :=
  P.root.toEquivRange.trans
    ((BijOn.equiv (s := range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (t :=
          range.{u_7, u_6 + 1} (ι := ι₂) (⇑P₂.root : (a : ι₂) → M₂)) (⇑f.toAddEquiv.toEquiv : (a : M) → M₂) ⋯).trans
      P₂.root.toEquivRange.symm)
i : ι
⊢ Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
    ((P₂.root : (a : ι₂) → M₂) ((e' : (a : ι) → ι₂) i : ι₂) : M₂)

Tactic:
simp [f, e', BijOn.equiv, Embedding.toEquivRange]

Premises used: Function.Embedding.toEquivRange, Set.BijOn.equiv
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0

Tactic:
replace h := LinearIndependent.pair_iff.mp <| h.restrict_scalars' ℤ
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
set :
  let S : Set ℤ :=
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))};
  ∀
    (S_def :
      S =
        {z : ℤ |
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}),
    ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p
⊢ ∃ q ≤ 0,
    ∃ p ≥ 0,
      {z : ℤ |
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))} =
        Icc q p

Tactic:
set S : Set ℤ := {z | P.root j + z • P.root i ∈ range P.root} with S_def

Premises used: Int, RootPairing.root, Set.range, DFunLike.coe, Set
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
⊢ 0 ∈ S

Tactic:
simp [S]
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
⊢ 0 ∈ S

Tactic:
have hS₀ : 0 ∈ S := by simp [S]
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
suffices :
  Injective.{1, u_1 + 1} (β := ι) fun (z : (↑S : Type)) ↦
    Exists.choose (p := fun (y : ι) ↦
      (P.root : (a : ι) → M) y =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
          (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
      ⋯
⊢ S.Finite

Tactic:
suffices Injective (fun z : S ↦ z.property.choose) from Finite.of_injective _ this