awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
⊢ ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
have aux : ∀ (i : ι),
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
      ((P.root : (a : ι) → M) i : M) ∨
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
      (-(P.root : (a : ι) → M) i : M)
Tactic: have aux (i : ι) := mem_or_neg_mem_closure_baseOf P.root f i (hf' i) (by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
        (-(P.root : (a : ι) → M) i : M)
⊢ ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
have rw : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = finrank R M
Tactic: rw [P.ncard_eq_finrank_of_linearIndepOn_of hli hsp, P.ncard_eq_finrank_of_linearIndepOn_of
      (P.linearIndepOn_root_baseOf f hf') aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
        (-(P.root : (a : ι) → M) i : M)
rw : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = finrank R M
⊢ ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
have rw₁ : finrank R M = finrank R M
Tactic: rw [P.ncard_eq_finrank_of_linearIndepOn_of hli hsp, P.ncard_eq_finrank_of_linearIndepOn_of
      (P.linearIndepOn_root_baseOf f hf') aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
⊢ s = baseOf (⇑P.root : (a : ι) → M) f
have h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
Tactic: have h_card : (baseOf P.root f).ncard = s.ncard := by
    have hf' (i : ι) : f (P.root i) ≠ 0 := AddSubmonoid.apply_ne_zero_of_mem_or_neg_mem_closure
      P.root f s (by aesop) i (P.ne_zero i) (by simp) (hsp i)
    have aux (i : ι) := mem_or_neg_mem_closure_baseOf P.root f i (hf' i) (by simp)
    rw [P.ncard_eq_finrank_of_linearIndepOn_of hli hsp, P.ncard_eq_finrank_of_linearIndepOn_of
      (P.linearIndepOn_root_baseOf f hf') aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
this : s ⊆ baseOf (⇑P.root : (a : ι) → M) f
⊢ ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) ≤ s.ncard
have rw : s.ncard ≤ s.ncard
Tactic: rw [h_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
⊢ s = baseOf (⇑P.root : (a : ι) → M) f
have suffices : s ⊆ baseOf (⇑P.root : (a : ι) → M) f
Tactic: suffices s ⊆ baseOf P.root f from eq_of_subset_of_ncard_le this (by rw [h_card])
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
i : ι
⊢ ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
have inl : ∀
  (hi :
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
      ((P.root : (a : ι) → M) i : M)),
  ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
Tactic: rcases hsp i with hi | hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
i : ι
inl :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M)),
    ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
⊢ ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
have inr : ∀
  (hi :
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
      (-(P.root : (a : ι) → M) i : M)),
  ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
Tactic: rcases hsp i with hi | hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
    (-(P.root : (a : ι) → M) i : M)
this : ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) (-i) : M) : ℚ) ((↑z : ℚ) : ℚ)
⊢ ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
have obtain : ∀ (z : ℤ) (hz : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) (-i) : M) : ℚ) ((↑z : ℚ) : ℚ)),
  ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
Tactic: obtain ⟨z, hz⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
    (-(P.root : (a : ι) → M) i : M)
⊢ ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
have inr : ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) (-i) : M) : ℚ) ((↑z : ℚ) : ℚ)
Tactic: suffices ∃ z : ℤ, f (P.root (-i)) = z by obtain ⟨z, hz⟩ := this; exact ⟨-z, by simp [← hz]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
    (-(P.root : (a : ι) → M) i : M)
⊢ ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) (-i) : M) : ℚ) ((↑z : ℚ) : ℚ)
have hi₁ : Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
  ((P.root : (a : ι) → M) (-i) : M)
Tactic: replace hi : P.root (-i) ∈ AddSubmonoid.closure (P.root '' s) := by simpa
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
⊢ s ⊆ baseOf (⇑P.root : (a : ι) → M) f
have hsp₁ : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
Tactic: replace hsp (i : ι) : ∃ z : ℤ, f (P.root i) = z := by
    rcases hsp i with hi | hi
    · exact AddSubmonoid.closure_induction (fun x ⟨j, hj, hx⟩ ↦ ⟨1, by simp [hf _ hj, ← hx]⟩)
        ⟨0, by simp⟩ (fun x y hx hy ⟨n, hn⟩ ⟨m, hm⟩ ↦ ⟨n + m, by simp [hn, hm]⟩) hi
    · suffices ∃ z : ℤ, f (P.root (-i)) = z by obtain ⟨z, hz⟩ := this; exact ⟨-z, by simp [← hz]⟩
      replace hi : P.root (-i) ∈ AddSubmonoid.closure (P.root '' s) := by simpa
      exact AddSubmonoid.closure_induction (fun x ⟨j, hj, hx⟩ ↦ ⟨1, by simp [hf _ hj, ← hx]⟩)
        ⟨0, by simp⟩ (fun x y hx hy ⟨n, hn⟩ ⟨m, hm⟩ ↦ ⟨n + m, by simp [hn, hm]⟩) hi
Cleared hypotheses: hsp
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
⊢ s ⊆ baseOf (⇑P.root : (a : ι) → M) f
have refine : ∀ (i : ι) (hi : i ∈ s) (j : ι)
  (hj :
    Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)}
      j)
  (k : ι)
  (hk :
    Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)}
      k)
  (contra :
    (P.root : (a : ι) → M) i =
      HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)),
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)
Tactic: refine fun i hi ↦ ⟨by aesop, fun j hj k hk contra ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} k
contra :
  (P.root : (a : ι) → M) i = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)
have obtain : ∀ (n : ℤ) (hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)),
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)
Tactic: obtain ⟨n, hn⟩ := hsp j
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} k
contra :
  (P.root : (a : ι) → M) i = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)
have obtain : ∀ (m : ℤ) (hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)),
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)
Tactic: obtain ⟨m, hm⟩ := hsp k