awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ
have w₁ : #ι ≤ #(↑(range Φ) : Type w)
Tactic: have w₁ : #ι ≤ #(Set.range Φ) := by
    apply Cardinal.le_range_of_union_finset_eq_univ
    exact union_support_maximal_linearIndependent_eq_range_basis b v i m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
w₁ : #ι ≤ #(↑(range Φ) : Type w)
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ
have w₂ : Cardinal.lift.{w', w} #(↑(range Φ) : Type w) ≤ Cardinal.lift.{w, w'} #κ
Tactic: have w₂ : Cardinal.lift.{w'} #(Set.range Φ) ≤ Cardinal.lift.{w} #κ := Cardinal.mk_range_le_lift
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
⊢ LinearIndependent.{u_6, u_1, u_4} R (M := P) ((⇑g : (a : M) → P) ∘ v ∘ a)
have apply : Disjoint (Submodule.span R (Set.range (v ∘ a))) g.ker
Tactic: apply (LinearIndependent.comp hli a hainj).map
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
⊢ Disjoint (Submodule.span R (Set.range (v ∘ a))) g.ker
have rw : ∀ (x : M), Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x → x ∈ f.range → x = 0
Tactic: rw [Submodule.disjoint_def, hfg.linearMap_ker_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
hy : Membership.mem (α := M) (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) ((f : (a : K) → M) y : M)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) (0 : K)
have revert : ∀ (hy : Membership.mem (α := M) (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) ((f : (a : K) → M) y : M)),
  Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) (0 : K)
Tactic: revert hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
⊢ ∀
    (hy :
      Membership.mem (α := M) (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) ((f : (a : K) → M) y : M)),
    Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) (0 : K)
have generalize : ∀ (x : M) (hy : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x),
  Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x : K) (0 : K)
Tactic: generalize f y = x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
x m : M
hm : m ∈ Set.range (v ∘ a)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) m : K) (0 : K)
have mem : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((v ∘ a) i) : K) (0 : K)
Tactic: obtain ⟨i, rfl⟩ := hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
x : M
hy : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x : K) (0 : K)
have mem : ∀ (m : M) (hm : m ∈ Set.range (v ∘ a)), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) m : K) (0 : K)
Tactic: induction hy using Submodule.span_induction with
    | mem m hm => obtain ⟨i, rfl⟩ := hm; apply hsa
    | zero => simp_all
    | add => simp_all
    | smul => simp_all
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
x : M
hy : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x
mem : ∀ (m : M) (hm : m ∈ Set.range (v ∘ a)), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) m : K) (0 : K)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x : K) (0 : K)
have zero : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) 0 : K) (0 : K)
Tactic: induction hy using Submodule.span_induction with
    | mem m hm => obtain ⟨i, rfl⟩ := hm; apply hsa
    | zero => simp_all
    | add => simp_all
    | smul => simp_all
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
x : M
hy : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x
mem : ∀ (m : M) (hm : m ∈ Set.range (v ∘ a)), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) m : K) (0 : K)
zero : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) 0 : K) (0 : K)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x : K) (0 : K)
have add : ∀ (x y : M),
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x →
    Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) y →
      Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x : K) (0 : K) →
        Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) y : K) (0 : K) →
          Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (x + y) : K) (0 : K)
Tactic: induction hy using Submodule.span_induction with
    | mem m hm => obtain ⟨i, rfl⟩ := hm; apply hsa
    | zero => simp_all
    | add => simp_all
    | smul => simp_all
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
x : M
hy : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x
mem : ∀ (m : M) (hm : m ∈ Set.range (v ∘ a)), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) m : K) (0 : K)
zero : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) 0 : K) (0 : K)
add :
  ∀ (x y : M),
    Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x →
      Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) y →
        Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x : K) (0 : K) →
          Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) y : K) (0 : K) →
            Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (x + y) : K) (0 : K)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x : K) (0 : K)
have smul : ∀ (a_1 : R) (x : M),
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x →
    Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x : K) (0 : K) →
      Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (a_1 • x) : K) (0 : K)
Tactic: induction hy using Submodule.span_induction with
    | mem m hm => obtain ⟨i, rfl⟩ := hm; apply hsa
    | zero => simp_all
    | add => simp_all
    | smul => simp_all
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (hypothesis)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
hy : Membership.mem (α := M) (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) ((f : (a : K) → M) y : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) y : M) (0 : M)
have hz : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) (0 : K)
Tactic: have hz : s (f y) = 0 := by
    revert hy
    generalize f y = x
    intro hy
    induction hy using Submodule.span_induction with
    | mem m hm => obtain ⟨i, rfl⟩ := hm; apply hsa
    | zero => simp_all
    | add => simp_all
    | smul => simp_all
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (hypothesis)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
hy : Membership.mem (α := M) (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) ((f : (a : K) → M) y : M)
hz : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) y : M) (0 : M)
have hs₁ : Eq (α := K) ((s ∘ₗ f : (a : K) → K) y : K) ((LinearMap.id : (a : K) → K) y : K)
Tactic: replace hs := DFunLike.congr_fun hs y
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
hy : Membership.mem (α := M) (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) ((f : (a : K) → M) y : M)
hz : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) (0 : K)
hs : (s : (a : M) → K) ((f : (a : K) → M) y : M) = y
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) y : M) (0 : M)
have rw : Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) : M) (0 : M)
Tactic: rw [← hs, hz, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
hy : Membership.mem (α := M) (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) ((f : (a : K) → M) y : M)
hz : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) (0 : K)
hs : (s : (a : M) → K) ((f : (a : K) → M) y : M) = y
rw : Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) y : M) (0 : M)
have rw₁ : Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) 0 : M) (0 : M)
Tactic: rw [← hs, hz, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hli : LinearIndependent R v
y : K
hy : Membership.mem (α := M) (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) ((f : (a : K) → M) y : M)
hz : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) (0 : K)
hs : (s : (a : M) → K) ((f : (a : K) → M) y : M) = y
rw : Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) : M) (0 : M)
rw₁ : Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) 0 : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) y : M) (0 : M)
have rw₂ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [← hs, hz, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
hslzero : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (Sum.inl i)) : K) (0 : K)
hli : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ Sum.inr)
hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))
p : P
⊢ Membership.mem (γ := Submodule R P) (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) p
have obtain : ∀ (m : M),
  Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P)
Tactic: obtain ⟨m, rfl⟩ := hg p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
hslzero : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (Sum.inl i)) : K) (0 : K)
hli : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ Sum.inr)
hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))
m : M
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P)
have inr : ∀
  (this :
    ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_7 : AddCommGroup M]
      [inst_8 : AddCommGroup K] [inst_9 : AddCommGroup P] [inst_10 : Module R M] [inst_11 : Module R K]
      [inst_12 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K} (hs : s ∘ₗ f = LinearMap.id)
      (hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P))
      {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M)
      (hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P))
      (hslzero : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (Sum.inl i)) : K) (0 : K))
      (hli : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ Sum.inr))
      (hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))) (m : M) (h : m ∈ s.ker),
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P))
  (h : m ∉ s.ker),
  Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P)
Tactic: wlog h : m ∈ LinearMap.ker s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup K
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R K
inst_6 : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
hslzero : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (Sum.inl i)) : K) (0 : K)
hli : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ Sum.inr)
hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))
m : M
this :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_7 : AddCommGroup M]
    [inst_8 : AddCommGroup K] [inst_9 : AddCommGroup P] [inst_10 : Module R M] [inst_11 : Module R K]
    [inst_12 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K} (hs : s ∘ₗ f = LinearMap.id)
    (hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P))
    {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M)
    (hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P))
    (hslzero : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (Sum.inl i)) : K) (0 : K))
    (hli : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ Sum.inr))
    (hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))) (m : M) (h : m ∈ s.ker),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
      (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P)
h : m ∉ s.ker
x : M := (f : (a : K) → M) ((s : (a : M) → K) m : K)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P)
have inr : Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
  (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl)))
  ((g : (a : M) → P) (HSub.hSub (β := M) m ((f : (a : K) → M) ((s : (a : M) → K) m : K) : M)) : P)
Tactic: rw [show g m = g (m - f (s m)) by simp [hfg.apply_apply_eq_zero]]