awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
rw : ⊤ ≤ map (p.projectionOnto q hpq) g.ker
⊢ Set.SurjOn (α := M) (β := ↥p) (⇑(p.projectionOnto q hpq) : (a : M) → ↥p)
    (Set.range.{u_2, u_3 + 1} (ι := K) (⇑f : (a : K) → M)) Set.univ

Tactic:
rw [← LinearMap.coe_range, ← Submodule.top_coe (R := R), surjOn_iff_le_map,
    ← hfg.linearMap_ker_eq]

Premises used: Function.Exact.linearMap_ker_eq, LinearMap.coe_range, Submodule.top_coe, Submodule.surjOn_iff_le_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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
x : ↥p
triv : Membership.mem (γ := Submodule R ↥p) ⊤ x
rwa rwa₁ rwa₂ rwa₃ : Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P) ⊤ ((g : (a : M) → P) (↑x : M) : P)
⊢ Membership.mem (α := P) (map g q) ((g : (a : M) → P) (↑x : M) : P)

Tactic:
rwa [hmap]
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
x : ↥p
triv : Membership.mem (γ := Submodule R ↥p) ⊤ x
obtain :
  ∀ (a : M) (haq : a ∈ (↑q : Set M))
    (ha : Eq.{u_4 + 1} (α := P) ((g : (a : M) → P) a : P) ((g : (a : M) → P) (↑x : M) : P)),
    x ∈ map (p.projectionOnto q hpq) g.ker
⊢ x ∈ map (p.projectionOnto q hpq) g.ker

Tactic:
obtain ⟨a, haq, ha⟩ : g x.val ∈ q.map g := by rwa [hmap]

Premises used: Submodule.map, Subtype.val, 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
x : ↥p
triv : Membership.mem (γ := Submodule R ↥p) ⊤ x
a : M
haq : a ∈ (↑q : Set M)
ha : Eq.{u_4 + 1} (α := P) ((g : (a : M) → P) a : P) ((g : (a : M) → P) (↑x : M) : P)
⊢ (↑x : M) - a ∈ (↑g.ker : Set M)

Tactic:
simp [← ha]
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
x : ↥p
triv : Membership.mem (γ := Submodule R ↥p) ⊤ x
a : M
haq : a ∈ (↑q : Set M)
ha : Eq.{u_4 + 1} (α := P) ((g : (a : M) → P) a : P) ((g : (a : M) → P) (↑x : M) : P)
⊢ (p.projectionOnto q hpq : (a : M) → ↥p) ((↑x : M) - a) = x

Tactic:
simpa
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
x : ↥p
triv : Membership.mem (γ := Submodule R ↥p) ⊤ x
a : M
haq : a ∈ (↑q : Set M)
ha : Eq.{u_4 + 1} (α := P) ((g : (a : M) → P) a : P) ((g : (a : M) → P) (↑x : M) : P)
⊢ x ∈ map (p.projectionOnto q hpq) g.ker

Tactic:
exact ⟨x - a, by simp [← ha], by simpa⟩
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := M) (⇑f : (a : K) → M)
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥p) (⇑(p.projectionOnto q hpq ∘ₗ f) : (a : K) → ↥p)

Tactic:
⟨?_, Submodule.projectionOnto_comp_surjective_of_exact hfg _ hmap⟩

Premises used: And.intro, Function.Bijective, Submodule.projectionOnto_comp_surjective_of_exact
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := M) (⇑f : (a : K) → M)
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
refine : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥p) (⇑(p.projectionOnto q hpq ∘ₗ f) : (a : K) → ↥p)
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥p) (⇑(p.projectionOnto q hpq ∘ₗ f) : (a : K) → ↥p)

Tactic:
refine ⟨?_, Submodule.projectionOnto_comp_surjective_of_exact hfg _ hmap⟩
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := M) (⇑f : (a : K) → M)
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
rwa : Set.InjOn (β := ↥p) (⇑(p.projectionOnto q hpq) : (a : M) → ↥p) (↑f.range : Set M)
⊢ Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥p) (⇑(p.projectionOnto q hpq ∘ₗ f) : (a : K) → ↥p)

Tactic:
rwa [LinearMap.coe_comp, Set.InjOn.injective_iff ↑(LinearMap.range f) _ subset_rfl]

Premises used: Set.InjOn.injective_iff, LinearMap.coe_comp
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := M) (⇑f : (a : K) → M)
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
⊢ Set.InjOn (β := ↥p) (⇑(p.projectionOnto q hpq) : (a : M) → ↥p) (↑f.range : Set M)

Tactic:
simpa [← LinearMap.disjoint_ker_iff_injOn, ← hfg.linearMap_ker_eq]

Premises used: Function.Exact.linearMap_ker_eq, LinearMap.disjoint_ker_iff_injOn
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := M) (⇑f : (a : K) → M)
q : Submodule R M
E : Type u_8
inst_7 : AddCommGroup E
inst_8 : Module R E
i : E →ₗ[R] M
hi : Function.Injective.{u_8 + 1, u_2 + 1} (α := E) (β := M) (⇑i : (a : E) → M)
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
rw :
  Function.Bijective.{u_2 + 1, u_8 + 1} (α := ↥i.range) (β := E)
    (⇑((↑(LinearEquiv.symm (LinearEquiv.ofInjective i hi)) :
            LinearMap.{u_1, u_1, u_2, u_8} (RingHom.id R) (↥i.range) E) :
          LinearMap.{u_1, u_1, u_2, u_8} (RingHom.id R) (↥i.range) E) :
      (a : ↥i.range) → E)
hg :
  Function.Bijective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥i.range)
    (⇑(i.range.projectionOnto q h ∘ₗ f) : (a : K) → ↥i.range)
⊢ Function.Bijective.{u_3 + 1, u_8 + 1} (α := K) (β := E) (⇑(linearProjOfIsCompl q i hi h ∘ₗ f) : (a : K) → E)

Tactic:
rw [LinearMap.linearProjOfIsCompl, LinearMap.comp_assoc, LinearMap.coe_comp,
      Function.Bijective.of_comp_iff]

Premises used: LinearMap.comp_assoc, LinearMap.linearProjOfIsCompl, Function.Bijective.of_comp_iff, LinearMap.coe_comp
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := M) (⇑f : (a : K) → M)
q : Submodule R M
E : Type u_8
inst_7 : AddCommGroup E
inst_8 : Module R E
i : E →ₗ[R] M
hi : Function.Injective.{u_8 + 1, u_2 + 1} (α := E) (β := M) (⇑i : (a : E) → M)
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective.{u_2 + 1, u_8 + 1} (α := ↥i.range) (β := E)
    (⇑((↑(LinearEquiv.symm (LinearEquiv.ofInjective i hi)) :
            LinearMap.{u_1, u_1, u_2, u_8} (RingHom.id R) (↥i.range) E) :
          LinearMap.{u_1, u_1, u_2, u_8} (RingHom.id R) (↥i.range) E) :
      (a : ↥i.range) → E)

Tactic:
(LinearEquiv.ofInjective i hi).symm.bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, Set.Mem, LinearEquiv.ofInjective
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := M) (⇑f : (a : K) → M)
q : Submodule R M
E : Type u_8
inst_7 : AddCommGroup E
inst_8 : Module R E
i : E →ₗ[R] M
hi : Function.Injective.{u_8 + 1, u_2 + 1} (α := E) (β := M) (⇑i : (a : E) → M)
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective.{u_2 + 1, u_8 + 1} (α := ↥i.range) (β := E)
    (⇑((↑(LinearEquiv.symm (LinearEquiv.ofInjective i hi)) :
            LinearMap.{u_1, u_1, u_2, u_8} (RingHom.id R) (↥i.range) E) :
          LinearMap.{u_1, u_1, u_2, u_8} (RingHom.id R) (↥i.range) E) :
      (a : ↥i.range) → E)

Tactic:
exact (LinearEquiv.ofInjective i hi).symm.bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, LinearEquiv.ofInjective
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := M) (⇑f : (a : K) → M)
q : Submodule R M
E : Type u_8
inst_7 : AddCommGroup E
inst_8 : Module R E
i : E →ₗ[R] M
hi : Function.Injective.{u_8 + 1, u_2 + 1} (α := E) (β := M) (⇑i : (a : E) → M)
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥i.range)
    (⇑(i.range.projectionOnto q h ∘ₗ f) : (a : K) → ↥i.range)

Tactic:
Submodule.projectionOnto_comp_bijective_of_exact hfg hf h hker hmap

Premises used: Submodule.projectionOnto_comp_bijective_of_exact, Set.Mem
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := M) (⇑f : (a : K) → M)
q : Submodule R M
E : Type u_8
inst_7 : AddCommGroup E
inst_8 : Module R E
i : E →ₗ[R] M
hi : Function.Injective.{u_8 + 1, u_2 + 1} (α := E) (β := M) (⇑i : (a : E) → M)
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥i.range)
    (⇑(i.range.projectionOnto q h ∘ₗ f) : (a : K) → ↥i.range)

Tactic:
exact Submodule.projectionOnto_comp_bijective_of_exact hfg hf h hker hmap

Premises used: Submodule.projectionOnto_comp_bijective_of_exact
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
rw : N = span R (image (α := ↥N) (⇑N.subtype : (a : ↥N) → M) (Set.range (ι := Fin n) (⇑b : (a : Fin n) → ↥N)))
rw₁ : N = map N.subtype (span R (Set.range (ι := Fin n) (⇑b : (a : Fin n) → ↥N)))
rw₂ : N = map N.subtype ⊤
rw₃ rw₄ : N = N
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))

Tactic:
rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]

Premises used: Set.range_comp, Submodule.map_subtype_top, Submodule.span_image, Module.Basis.span_eq
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
c : R
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))) x
hc : c • y + x = 0
⊢ x ∈ N

Tactic:
rw [← span_b] at hx
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
c : R
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))) x
hc : c • y + x = 0
hx₁ : x ∈ N
⊢ c • y + x = 0

Tactic:
rw [← span_b] at hx
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
c : R
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0

Tactic:
hli c x hx hc
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
c : R
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0

Tactic:
exact hli c x hx hc
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
x : M
h : Membership.mem (γ := Submodule R M) ⊤ x
⊢ Membership.mem (γ := Submodule R M)
    (span R
      (Set.range (ι := Fin (n + 1))
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) y
          (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))))
    x

Tactic:
simpa [Submodule.mem_span_insert', span_b] using hsp x

Premises used: Submodule.mem_span_insert'
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N : Submodule R M
y : M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
unfold :
  Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M)
    (⇑(have span_b := ⋯;
        Basis.mk ⋯ ⋯) :
      (a : Fin (n + 1)) → M)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ M) y
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)))
⊢ Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M) (⇑(mkFinCons y b hli hsp) : (a : Fin (n + 1)) → M)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ M) y
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)))

Tactic:
unfold mkFinCons

Premises used: Module.Basis.mkFinCons
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N : Submodule R M
y : M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
⊢ Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M)
    (⇑(have span_b := ⋯;
        Basis.mk ⋯ ⋯) :
      (a : Fin (n + 1)) → M)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ M) y
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)))

Tactic:
coe_mk (v := Fin.cons y (N.subtype ∘ b)) _ _

Premises used: Module.Basis.coe_mk
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N : Submodule R M
y : M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
⊢ Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M)
    (⇑(have span_b := ⋯;
        Basis.mk ⋯ ⋯) :
      (a : Fin (n + 1)) → M)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ M) y
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)))

Tactic:
exact coe_mk (v := Fin.cons y (N.subtype ∘ b)) _ _

Premises used: Module.Basis.coe_mk
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N O : Submodule R M
y : M
yO : y ∈ O
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hNO : N ≤ O
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ z ∈ O, ∃ (c : R), z + c • y ∈ N
⊢ Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → ↥O) (⇑(mkFinConsOfLE y yO b hNO hli hsp) : (a : Fin (n + 1)) → ↥O)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ ↥O) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO)
      (Function.comp (β := ↥N) (⇑(Submodule.inclusion hNO) : (a : ↥N) → ↥O) (⇑b : (a : Fin n) → ↥N)))

Tactic:
coe_mkFinCons _ _ _ _

Premises used: Module.Basis.coe_mkFinCons
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
rw : N = span R (image (α := ↥N) (⇑N.subtype : (a : ↥N) → M) (Set.range (ι := Fin n) (⇑b : (a : Fin n) → ↥N)))
rw₁ : N = map N.subtype (span R (Set.range (ι := Fin n) (⇑b : (a : Fin n) → ↥N)))
rw₂ : N = map N.subtype ⊤
rw₃ rw₄ : N = N
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))

Tactic:
rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]

Premises used: Set.range_comp, Submodule.map_subtype_top, Submodule.span_image, Module.Basis.span_eq
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
c : R
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))) x
hc : c • y + x = 0
⊢ x ∈ N

Tactic:
rw [← span_b] at hx
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
c : R
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))) x
hc : c • y + x = 0
hx₁ : x ∈ N
⊢ c • y + x = 0

Tactic:
rw [← span_b] at hx
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
c : R
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0

Tactic:
hli c x hx hc