-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x) w ↔
      ∃ (k : ℕ), diagonal ((d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ x) 1) ^ k) *ᵥ w = 0
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
mp :
  Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) →
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
mpr :
  (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
    Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
mp₁ mp₂ :
  Membership.mem (γ := Submodule K ((j : ι) → K))
      (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
    (∀ (i : ι), d i ≠ 0) →
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) →
        (∀ (i : ι), d i ≠ 0) ∧
          Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
            Membership.mem (γ := Submodule K ((j : ι) → K))
              (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
mp₃ :
  Membership.mem (γ := Submodule K ((j : ι) → K))
      (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
    (∀ (i : ι), d i ≠ 0) → Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) → ∀ (i : ι), d i ≠ 0
mp₄ :
  Membership.mem (γ := Submodule K ((j : ι) → K))
      (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
    (∀ (i : ι), d i ≠ 0) → Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) → Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
⊢ Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ↔
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
have mp₅ : Membership.mem (γ := Submodule K ((j : ι) → K))
    (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
  (∀ (i : ι), d i ≠ 0) →
    Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) →
      Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
Tactic: tauto