awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this : InvolutiveNeg ι := P.indexNeg
z : ℤ
⊢ Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
      z ↔
    Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
        (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
      z
have rw : Membership.mem (γ := Set ℤ)
    (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
    z ↔
  Membership.mem (γ := Set ℤ)
    (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
    z
Tactic: rw [P.chainCoeff_reflectionPerm_left_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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 : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j =
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have this₁ : ∀ (z : ℤ),
  Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
      z ↔
    Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
        (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
      z
Tactic: have (z : ℤ) : z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
      z ∈ Icc (-P.chainBotCoeff (-i) j : ℤ) (P.chainTopCoeff (-i) j) := by
    rw [P.chainCoeff_reflectionPerm_left_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        z ↔
      Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
          (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
        z
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j =
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have refine_1 : chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j ≤
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        z ↔
      Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
          (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
        z
refine_1 :
  chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j ≤
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j =
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have refine_2 : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
  chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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 : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j =
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have this₁ : ∀ (z : ℤ),
  Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
      z ↔
    Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
        (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
      z
Tactic: have (z : ℤ) : z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
      z ∈ Icc (-P.chainBotCoeff (-i) j : ℤ) (P.chainTopCoeff (-i) j) := by
    rw [P.chainCoeff_reflectionPerm_left_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        z ↔
      Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
          (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
        z
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j =
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have refine_1 : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j ≤
  chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        z ↔
      Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
          (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (-i) j) : ℤ))
        z
refine_1 :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j ≤
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j =
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have refine_2 : chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) ((P.reflectionPerm i : (a : ι) → ι) i) j
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this : InvolutiveNeg ι := P.indexNeg
z : ℤ
⊢ Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
      z ↔
    Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
        (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
      z
have rw : Membership.mem (γ := Set ℤ)
    (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
    z ↔
  Membership.mem (γ := Set ℤ)
    (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
    z
Tactic: rw [P.chainCoeff_reflectionPerm_right_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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 : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) =
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have this₁ : ∀ (z : ℤ),
  Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
      z ↔
    Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
        (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
      z
Tactic: have (z : ℤ) : z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
      z ∈ Icc (-P.chainBotCoeff i (-j) : ℤ) (P.chainTopCoeff i (-j)) := by
    rw [P.chainCoeff_reflectionPerm_right_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        z ↔
      Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
          (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
        z
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) =
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have refine_1 : chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) ≤
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        z ↔
      Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
          (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
        z
refine_1 :
  chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) ≤
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) =
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have refine_2 : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
  chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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 : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) =
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have this₁ : ∀ (z : ℤ),
  Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
      z ↔
    Membership.mem (γ := Set ℤ)
      (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
        (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
      z
Tactic: have (z : ℤ) : z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
      z ∈ Icc (-P.chainBotCoeff i (-j) : ℤ) (P.chainTopCoeff i (-j)) := by
    rw [P.chainCoeff_reflectionPerm_right_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        z ↔
      Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
          (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
        z
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) =
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have refine_1 : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) ≤
  chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
        z ↔
      Membership.mem (γ := Set ℤ)
        (Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
          (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i (-j)) : ℤ))
        z
refine_1 :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) ≤
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j) =
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
have refine_2 : chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i ((P.reflectionPerm j : (a : ι) → ι) j)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0 ↔
    ¬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) ∨
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M) ∉
        range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
have pos : ∀
  (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)),
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0 ↔
    ¬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) ∨
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M) ∉
        range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
Tactic: by_cases h : LinearIndependent R ![P.root i, P.root j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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 : ι
pos :
  ∀
    (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)),
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0 ↔
      ¬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) ∨
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M) ∉
          range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0 ↔
    ¬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) ∨
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M) ∉
        range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
have neg : ∀
  (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)),
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0 ↔
    ¬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) ∨
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M) ∉
        range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
Tactic: by_cases h : LinearIndependent R ![P.root i, P.root j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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_1 :
  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)
h : ∀ (x : ℕ), x ≤ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ↔ x = 0
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0
have rw : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
Tactic: rw [← h]