awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
⊢ Subset.{u_1} (α := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) (baseOf (⇑P.coroot : (a : ι) → N) g)
have refine : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i) (j : ι)
  (hj :
    Membership.mem (γ := Set ι)
      {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)} j)
  (k : ι)
  (hk :
    Membership.mem (γ := Set ι)
      {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)} k)
  (contra :
    (P.coroot : (a : ι) → N) i =
      HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)),
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) j : N) (0 : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N) (0 : N)
Tactic: refine fun i hi ↦ ⟨by obtain ⟨hi, -⟩ := hi; 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) j : N) (0 : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N) (0 : N)
have suffices : i = j
Tactic: suffices i = j by grind
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
⊢ ∃ u > 0,
    ∃ v > 0,
      (P.root : (a : ι) → M) i =
        HSMul.hSMul (β := M) u ((P.root : (a : ι) → M) j : M) + HSMul.hSMul (β := M) v ((P.root : (a : ι) → M) k : M)
have hl : ∀ (i : ι), 0 < l i
Tactic: have hl (i : ι) : 0 < l i := by
      simpa only [l, ← posRootForm_eq] using RootPositiveForm.zero_lt_posForm_apply_root _ _
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
⊢ ∃ u > 0,
    ∃ v > 0,
      (P.root : (a : ι) → M) i =
        HSMul.hSMul (β := M) u ((P.root : (a : ι) → M) j : M) + HSMul.hSMul (β := M) v ((P.root : (a : ι) → M) k : M)
have refine : (P.root : (a : ι) → M) i =
  HSMul.hSMul (β := M) (l i / l j) ((P.root : (a : ι) → M) j : M) +
    HSMul.hSMul (β := M) (l i / l k) ((P.root : (a : ι) → M) k : M)
Tactic: refine ⟨l i / l j, by simp [hl], l i / l k, by simp [hl], ?_⟩
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
⊢ (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (l i / l j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (l i / l k) ((P.root : (a : ι) → M) k : M)
have contra₁ : HSMul.hSMul (β := M)
    (HDiv.hDiv (α := R) (β := R) (2 : R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R))
    ((P.root : (a : ι) → M) i : M) =
  HSMul.hSMul (β := M)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R))
      ((P.root : (a : ι) → M) j : M) +
    HSMul.hSMul (β := M)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) k : M) :
          R))
      ((P.root : (a : ι) → M) k : M)
Tactic: simp only [P.coroot_eq_polarizationEquiv_apply_root, ← map_smul, ← map_add,
      P.PolarizationEquiv.injective.eq_iff] at contra
Cleared hypotheses: contra
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
contra :
  HSMul.hSMul (β := M)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R))
      ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M)
        (HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R))
        ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M)
        (HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) k : M) :
            R))
        ((P.root : (a : ι) → M) k : M)
l' : (i : ι) → R :=
  fun (i : ι) ↦
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
⊢ (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (l i / l j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (l i / l k) ((P.root : (a : ι) → M) k : M)
have hll' : ∀ (i : ι), (↑(l i) : R) = l' i
Tactic: have hll' (i : ι) : l i = l' i := P.algebraMap_rootFormIn ℚ _ _
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
l' : (i : ι) → R :=
  fun (i : ι) ↦
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hll' : ∀ (i : ι), (↑(l i) : R) = l' i
contra :
  HSMul.hSMul (β := M) (2 / l' i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M) (2 / l' j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)
⊢ (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (l i / l j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (l i / l k) ((P.root : (a : ι) → M) k : M)
have contra₁ : Eq.{u_3 + 1} (α := M)
  ((fun (x : M) ↦ (2 / l' i)⁻¹ • x) (HSMul.hSMul (β := M) (2 / l' i) ((P.root : (a : ι) → M) i : M)))
  ((fun (x : M) ↦ (2 / l' i)⁻¹ • x)
    (HSMul.hSMul (β := M) (2 / l' j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)))
Tactic: replace contra := congr_arg ((2 / l' i)⁻¹ • ·) contra
Cleared hypotheses: contra
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
l' : (i : ι) → R :=
  fun (i : ι) ↦
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hll' : ∀ (i : ι), (↑(l i) : R) = l' i
contra :
  Eq.{u_3 + 1} (α := M)
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x) (HSMul.hSMul (β := M) (2 / l' i) ((P.root : (a : ι) → M) i : M)))
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x)
      (HSMul.hSMul (β := M) (2 / l' j) ((P.root : (a : ι) → M) j : M) +
        HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)))
⊢ (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (l i / l j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (l i / l k) ((P.root : (a : ι) → M) k : M)
have aux₁ : 2 / l' i ≠ 0
Tactic: have aux₁ : 2 / l' i ≠ 0 := by simpa using IsAnisotropic.rootForm_root_ne_zero i
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j_1 : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j_1
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
l' : (i : ι) → R :=
  fun (i : ι) ↦
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hll' : ∀ (i : ι), (↑(l i) : R) = l' i
contra :
  Eq.{u_3 + 1} (α := M)
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x) (HSMul.hSMul (β := M) (2 / l' i) ((P.root : (a : ι) → M) i : M)))
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x)
      (HSMul.hSMul (β := M) (2 / l' j_1) ((P.root : (a : ι) → M) j_1 : M) +
        HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)))
aux₁ : 2 / l' i ≠ 0
j : ι
⊢ (2 / l' i)⁻¹ * (2 / l' j) = HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)
have ring_nf : (l' i)⁻¹⁻¹ * (l' j)⁻¹ = HMul.hMul (α := R) (↑(l i) : R) (↑(l j) : R)⁻¹
Tactic: ring_nf
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
l' : (i : ι) → R :=
  fun (i : ι) ↦
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hll' : ∀ (i : ι), (↑(l i) : R) = l' i
contra :
  Eq.{u_3 + 1} (α := M)
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x) (HSMul.hSMul (β := M) (2 / l' i) ((P.root : (a : ι) → M) i : M)))
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x)
      (HSMul.hSMul (β := M) (2 / l' j) ((P.root : (a : ι) → M) j : M) +
        HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)))
aux₁ : 2 / l' i ≠ 0
⊢ (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (l i / l j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (l i / l k) ((P.root : (a : ι) → M) k : M)
have aux₂ : ∀ (j : ι), (2 / l' i)⁻¹ * (2 / l' j) = HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)
Tactic: have aux₂ (j : ι) : (2 / l' i)⁻¹ * (2 / l' j) = l i / l j := by ring_nf; simp [hll']
-- 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
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
l : (i : ι) → ℚ :=
  fun (i : ι) ↦
    (((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
l' : (i : ι) → R :=
  fun (i : ι) ↦
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hll' : ∀ (i : ι), (↑(l i) : R) = l' i
contra :
  Eq.{u_3 + 1} (α := M)
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x) (HSMul.hSMul (β := M) (2 / l' i) ((P.root : (a : ι) → M) i : M)))
    ((fun (x : M) ↦ (2 / l' i)⁻¹ • x)
      (HSMul.hSMul (β := M) (2 / l' j) ((P.root : (a : ι) → M) j : M) +
        HSMul.hSMul (β := M) (2 / l' k) ((P.root : (a : ι) → M) k : M)))
aux₁ : 2 / l' i ≠ 0
aux₂ : ∀ (j : ι), (2 / l' i)⁻¹ * (2 / l' j) = HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)
⊢ (P.root : (a : ι) → M) i =
    HSMul.hSMul (β := M) (l i / l j) ((P.root : (a : ι) → M) j : M) +
      HSMul.hSMul (β := M) (l i / l k) ((P.root : (a : ι) → M) k : M)
have contra₁ : (P.root : (a : ι) → M) i =
  HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l j) : R)) ((P.root : (a : ι) → M) j : M) +
    HSMul.hSMul (β := M) (HDiv.hDiv (α := R) (↑(l i) : R) (↑(l k) : R)) ((P.root : (a : ι) → M) k : M)
Tactic: simp only [smul_add, smul_smul, inv_mul_cancel₀ aux₁, aux₂, one_smul] at contra
Cleared hypotheses: contra