Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (x : V ⧸ (↑(auxTransvection hf * e)).fixedSubmodule), (auxTransvection hf * e).fixedReduce x = a • x
hb : ∀ (x : V ⧸ (↑(auxTransvection hg * e)).fixedSubmodule), (auxTransvection hg * e).fixedReduce x = b • x
⊢ False

Tactic:
by
  simp only [fixedReduce_eq_smul_iff, auxTransvection_mul_fixed hfv] at ha
  simp only [fixedReduce_eq_smul_iff, auxTransvection_mul_fixed hfgv] at hb
  /- Since `auxTransvection hf = transvection f (v - e v)` and
    `auxTransvection hg = transvection (f + g) (v - e v)`,
    subtracting the relations `ha` and `hb` gives the following: -/
  set c := b - a with hc
  have key (x : V) : g (e x) • (v - e v) - c • x ∈ e.fixedSubmodule ⊔ K ∙ v := by
    have ha := ha x
    have hb := hb x
    simp only [LinearEquiv.mul_apply, transvection.apply, auxTransvection] at ha hb
    rw [LinearMap.add_apply, add_smul, ← add_assoc] at hb
    convert Submodule.sub_mem _ hb ha using 1
    -- should be taken care by a `module` tactic that handles noncommutative rings
    simp only [add_comm _ (g (e x) • _), ← add_assoc]
    rw [sub_eq_add_neg]
    simp only [add_sub_assoc, add_assoc, add_right_inj, sub_smul, smul_sub, hc]
    abel
  -- To get the contradiction, we distinguish whether `a = b` or not.
  rcases eq_or_ne c 0 with hc0 | hc0
  · -- When `c = 0`, we contradict the linear independence given by `hv`
    apply one_ne_zero (α := K)
    rw [LinearIndependent.pair_iff] at hv
    have hmem : v - e v ∈ e.fixedSubmodule ⊔ K ∙ v := by
      simp only [hc0, zero_smul, sub_zero] at key
      obtain ⟨w, hw⟩ : ∃ w, g w ≠ 0 := by
        contrapose! hg0
        exact LinearMap.ext hg0
      simpa [hw] using key ((g w)⁻¹ • e⁻¹ w)
    simp only [mem_sup, mem_span_singleton, exists_exists_eq_and] at hmem
    obtain ⟨y, hy, k, hk⟩ := hmem
    refine (hv (k - 1) 1 ?_).right
    simp only [Submodule.mkQ_apply, fixedReduce_mk]
    simp only [← e.fixedSubmodule.mkQ_apply, ← LinearMap.map_smul, ← map_add,
      ← LinearMap.mem_ker, Submodule.ker_mkQ]
    rw [← Submodule.neg_mem_iff] at hy
    convert hy using 1
    rw [eq_comm, ← sub_eq_iff_eq_add] at hk
    rw [← hk]
    simp only [sub_smul, one_smul]
    abel
  · -- When `c ≠ 0`, we contradict `hne_top`
    refine hne_top.ne ?_
    rw [eq_top_iff]
    intro x _
    have h1 : g (e x) • (v - e v) ∈ K ∙ (e v - v) :=
      mem_span_singleton.mpr ⟨-g (e x), by rw [neg_smul, smul_sub, smul_sub, neg_sub]⟩
    have hle : e.fixedSubmodule ⊔ K ∙ v ≤ e.fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v :=
      sup_le_sup_right le_sup_left _
    have h2 : c • x ∈ e.fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v := by
      rw [show c • x = g (e x) • (v - e v) - (g (e x) • (v - e v) - c • x) by abel]
      exact Submodule.sub_mem _ (mem_sup_left (mem_sup_right h1)) (hle (key x))
    simpa [smul_smul, inv_mul_cancel₀ hc0] using Submodule.smul_mem _ c⁻¹ h2

Goal state after: