awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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)
w₂ : Cardinal.lift.{w', w} #(↑(range Φ) : Type w) ≤ Cardinal.lift.{w, w'} #κ
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ

Tactic:
(Cardinal.lift_le.mpr w₁).trans w₂

Premises used: Iff.mpr, LE.le.trans, Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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)
w₂ : Cardinal.lift.{w', w} #(↑(range Φ) : Type w) ≤ Cardinal.lift.{w, w'} #κ
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ

Tactic:
exact (Cardinal.lift_le.mpr w₁).trans w₂

Premises used: Iff.mpr, LE.le.trans, Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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
⊢ #ι ≤ #κ

Tactic:
Cardinal.lift_le.mp (infinite_basis_le_maximal_linearIndependent' b v i m)

Premises used: Iff.mp, infinite_basis_le_maximal_linearIndependent', Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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
apply : Disjoint (Submodule.span R (Set.range (v ∘ a))) g.ker
⊢ LinearIndependent.{u_6, u_1, u_4} R (M := P) ((⇑g : (a : M) → P) ∘ v ∘ a)

Tactic:
apply (LinearIndependent.comp hli a hainj).map

Premises used: LinearIndependent.comp, LinearIndependent.map
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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
rw : ∀ (x : M), Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x → x ∈ f.range → x = 0
⊢ Disjoint (Submodule.span R (Set.range (v ∘ a))) g.ker

Tactic:
rw [Submodule.disjoint_def, hfg.linearMap_ker_eq]

Premises used: Function.Exact.linearMap_ker_eq, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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)
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)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) y : M) : K) (0 : K)

Tactic:
revert hy
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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
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)
⊢ ∀
    (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:
generalize f y = x

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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)
mem : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((v ∘ a) i) : K) (0 : K)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) m : K) (0 : K)

Tactic:
obtain ⟨i, rfl⟩ := hm

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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
i : κ
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((v ∘ a) i) : K) (0 : K)

Tactic:
apply hsa
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) 0 : K) (0 : K)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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 x_1 y_1 : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x_1
hy : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) y_1
h : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x_1 : K) (0 : K)
h_1 : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) y_1 : K) (0 : K)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (x_1 + y_1) : K) (0 : K)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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
a_1 : R
x_1 : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range (v ∘ a))) x_1
h : Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) x_1 : K) (0 : K)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (a_1 • x_1) : K) (0 : K)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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)
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)
⊢ Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) 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

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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)

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
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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 (α := K) ((s ∘ₗ f : (a : K) → K) y : K) ((LinearMap.id : (a : K) → K) y : K)

Tactic:
replace hs := DFunLike.congr_fun hs y
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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)
rw₂ rw₃ : Eq.{u_2 + 1} (α := M) 0 0
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : K) → M) y : M) (0 : M)

Tactic:
rw [← hs, hz, map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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
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)
⊢ Membership.mem (γ := Submodule R P) (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) p

Tactic:
obtain ⟨m, rfl⟩ := hg p

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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)
⊢ Eq.{u_4 + 1} (α := P) ((g : (a : M) → P) m : P)
    ((g : (a : M) → P) (HSub.hSub (β := M) m ((f : (a : K) → M) ((s : (a : M) → K) m : K) : M)) : P)

Tactic:
simp [hfg.apply_apply_eq_zero]

Premises used: Function.Exact.apply_apply_eq_zero
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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)
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)
⊢ 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:
rw [show g m = g (m - f (s m)) by simp [hfg.apply_apply_eq_zero]]
-- Module: Mathlib.LinearAlgebra.Basis.Exact
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)
inr : HSub.hSub (β := M) m ((f : (a : K) → M) ((s : (a : M) → K) m : K) : 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) (HSub.hSub (β := M) m ((f : (a : K) → M) ((s : (a : M) → K) m : K) : M)) : P)

Tactic:
apply this hs hfg v hg hslzero hli hsp