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
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
⊢ e ∈ transvections K V ^ (finrank K (V ⧸ (↑e).fixedSubmodule) - 1) * dilatransvections K V

Tactic:
induction h : finrank K (V ⧸ e.fixedSubmodule) generalizing e he with
  | zero => simp [mem_dilatransvections_iff_finrank_quotient, h]
  | succ n hind =>
    match n with
    | 0 => simp [mem_dilatransvections_iff_finrank_quotient, h]
    | n + 1 =>
      simp only [ne_eq, add_tsub_cancel_right] at hind ⊢
      simp only [add_assoc, Nat.reduceAdd] at h
      rw [pow_succ', mul_assoc, Set.mem_mul]
      /- The strategy is similar to the first non-exceptional case:
        we construct `f : Dual K V` and `v : V` such that,
        setting `t = auxTransvection hf`, we have `e = t⁻¹ * (t * e)`
        and `t * e` satisfies the induction hypothesis,
        after possibly replacing `f` by `f + g` for a suitable `g`. -/
      obtain ⟨f, v, hv, hf, hfv⟩ := exists_dual_of_fixedReduce_ne_smul he (by omega)
      have hv_notMem : v ∉ e.fixedSubmodule := by
        simpa [Submodule.Quotient.mk_eq_zero] using hv.ne_zero 0
      have hrank : finrank K (V ⧸ (e.fixedSubmodule ⊔ K ∙ v)) = n + 1 := by
        have := finrank_quotient_sup_span_singleton hv_notMem
        omega
      -- The case `n = 0` is easy
      rcases Nat.eq_zero_or_pos n with hn0 | hn_pos
      · simp only [hn0, pow_zero, one_mul]
        refine ⟨(auxTransvection hf)⁻¹, ?_, auxTransvection hf * e, ?_, by simp⟩
        · rw [inv_mem_transvections_iff]
          apply mem_transvections
        · rw [mem_dilatransvections_iff_finrank_quotient,
            auxTransvection_mul_fixed hfv, hrank, hn0, zero_add]
      by_cases he' : auxTransvection hf * e ∈ transvections K V ^ n * dilatransvections K V
      · -- This is the easy case where one knows that `auxTransvection hf * e` is
        -- the product of at most `n + 1` transvections
        refine ⟨(auxTransvection hf)⁻¹, ?_, auxTransvection hf * e, he', by simp⟩
        rw [inv_mem_transvections_iff]
        apply mem_transvections
      -- Otherwise, we will need to modify `auxTransvection hf` by changing `f`.
      have hne_top : e.fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤ := by
        rw [sup_right_comm]
        exact sup_span_singleton_lt_top _ (by rw [hrank]; omega)
      obtain ⟨g : Dual K V, hg0 : g ≠ 0, hg2⟩ :=
        Submodule.exists_dual_map_eq_bot_of_lt_top hne_top inferInstance
      rw [← le_ker_iff_map] at hg2
      have hg : e.fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g) := fun x hx ↦ by
        rw [mem_ker, LinearMap.add_apply, mem_ker.mp (hf hx),
          mem_ker.mp (hg2 (mem_sup_left hx)), add_zero]
      have hfgv : (f + g) v = 1 := by
        rw [LinearMap.add_apply, hfv,
          mem_ker.mp (hg2 (mem_sup_right (mem_span_singleton_self v))), add_zero]
      refine ⟨(auxTransvection hg)⁻¹, ?_, auxTransvection hg * e, ?_, by simp⟩
      · rw [inv_mem_transvections_iff]
        apply mem_transvections
      -- It remains to prove that `auxTransvection hg * e` satisfies the induction hypothesis
      apply hind ?_ (by rw [auxTransvection_mul_fixed hfgv, hrank])
      -- The induction hypothesis implies that `(auxTransvection hf * e).fixedReduce`
      -- is a homothety, for otherwise the previous case would apply.
      obtain ⟨a, ha⟩ : ∃ a : K, ∀ x, (auxTransvection hf * e).fixedReduce x = a • x := by
        contrapose! he'
        exact hind he' (by rw [auxTransvection_mul_fixed hfv, hrank])
      -- Then `(auxTransvection hg * e).fixedReduce` cannot also be a homothety.
      intro b
      by_contra! hb
      exact not_forall_fixedReduce_eq_smul hv hfv hfgv hg0 hne_top ha hb

Goal state after: