awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
x : M
h : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x
j : ι
hj : j ∈ s
hx : (P.root : (a : ι) → M) j = x
⊢ Eq (α := ℚ) ((f : (a : M) → ℚ) x : ℚ) ((↑1 : ℚ) : ℚ)

Tactic:
simp [hf _ hj, ← hx]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
⊢ Eq (α := ℚ) ((f : (a : M) → ℚ) 0 : ℚ) ((↑0 : ℚ) : ℚ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s)) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s)) y
h : ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) x : ℚ) ((↑z : ℚ) : ℚ)
h_1 : ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) y : ℚ) ((↑z : ℚ) : ℚ)
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) x : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) y : ℚ) ((↑m : ℚ) : ℚ)
⊢ Eq (α := ℚ) ((f : (a : M) → ℚ) (x + y) : ℚ) ((↑(n + m) : ℚ) : ℚ)

Tactic:
simp [hn, hm]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℚ) : ℚ)

Tactic:
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
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℚ) : ℚ)
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 : ℚ) : ℚ)
⊢ ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)

Tactic:
obtain ⟨z, hz⟩ := this
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℤ
hz : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) (-i) : M) : ℚ) ((↑z : ℚ) : ℚ)
⊢ Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑(-z) : ℚ) : ℚ)

Tactic:
simp [← hz]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℤ
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:
exact ⟨-z, by simp [← hz]⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
inr : ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) (-i) : M) : ℚ) ((↑z : ℚ) : ℚ)
⊢ ∃ (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]⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
    ((P.root : (a : ι) → M) (-i) : M)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
x : M
h : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x
j : ι
hj : j ∈ s
hx : (P.root : (a : ι) → M) j = x
⊢ Eq (α := ℚ) ((f : (a : M) → ℚ) x : ℚ) ((↑1 : ℚ) : ℚ)

Tactic:
simp [hf _ hj, ← hx]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
⊢ Eq (α := ℚ) ((f : (a : M) → ℚ) 0 : ℚ) ((↑0 : ℚ) : ℚ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s)) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s)) y
h : ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) x : ℚ) ((↑z : ℚ) : ℚ)
h_1 : ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) y : ℚ) ((↑z : ℚ) : ℚ)
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) x : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) y : ℚ) ((↑m : ℚ) : ℚ)
⊢ Eq (α := ℚ) ((f : (a : M) → ℚ) (x + y) : ℚ) ((↑(n + m) : ℚ) : ℚ)

Tactic:
simp [hn, hm]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℚ) : ℚ)

Tactic:
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
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℚ) : ℚ)

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
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
⊢ Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} i

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℚ) : ℚ)
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)
⊢ s ⊆ baseOf (⇑P.root : (a : ι) → M) f

Tactic:
refine fun i hi ↦ ⟨by aesop, fun j hj k hk contra ↦ ?_⟩