-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i j : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
this :
  ∀ (i j : ι),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)) →
      Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M) →
        Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
aux :
  Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M) →
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
inl :
  ∀ (aux : ((P.root : (a : ι) → M) j : M) ∉ q),
    Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) i : M) ↔
      Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) j : M)
inr :
  ∀ (aux : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)),
    Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) i : M) ↔
      Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) j : M)
inl₁ :
  ∀ (aux : ((P.root : (a : ι) → M) j : M) ∉ q),
    Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) i : M) ↔
      Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) j : M)
inr₁ :
  ∀ (aux : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)),
    Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) i : M) ↔
      Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) j : M)
inl₂ :
  ∀ (aux : ((P.root : (a : ι) → M) j : M) ∉ q),
    Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) i : M) →
      Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) j : M)
⊢ Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) i : M) ↔
    Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) j : M)
have inl₃ : ∀ (aux : ((P.root : (a : ι) → M) j : M) ∉ q),
  Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) j : M) →
    Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) i : M)
Tactic: tauto
Cleared hypotheses: aux