awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 = ⊤
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥p) (⇑(p.projectionOnto q hpq ∘ₗ f) : (a : K) → ↥p)
have rw : 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 [← Set.surjOn_univ, LinearMap.coe_comp, Set.surjOn_comp_iff, Set.image_univ]
-- 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
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 = ⊤
⊢ 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
have rw : ⊤ ≤ map (p.projectionOnto q hpq) g.ker
Tactic: rw [← LinearMap.coe_range, ← Submodule.top_coe (R := R), surjOn_iff_le_map,
    ← 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
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
⊢ Membership.mem (α := P) (map g q) ((g : (a : M) → P) (↑x : M) : P)
have rwa : Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P) ⊤ ((g : (a : M) → P) (↑x : M) : P)
Tactic: rwa [hmap]
-- 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
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
⊢ x ∈ map (p.projectionOnto q hpq) g.ker
have 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
Tactic: obtain ⟨a, haq, ha⟩ : g x.val ∈ q.map g := by rwa [hmap]
-- 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
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)
have refine : Function.Injective.{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⟩
-- 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
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.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥p) (⇑(p.projectionOnto q hpq ∘ₗ f) : (a : K) → ↥p)
have rwa : Set.InjOn (β := ↥p) (⇑(p.projectionOnto q hpq) : (a : M) → ↥p) (↑f.range : Set M)
Tactic: rwa [LinearMap.coe_comp, Set.InjOn.injective_iff ↑(LinearMap.range f) _ subset_rfl]
-- 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
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_8 + 1} (α := K) (β := E) (⇑(linearProjOfIsCompl q i hi h ∘ₗ f) : (a : K) → E)
have 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)
Tactic: rw [LinearMap.linearProjOfIsCompl, LinearMap.comp_assoc, LinearMap.coe_comp,
      Function.Bijective.of_comp_iff]
-- 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
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)
⊢ Function.Bijective.{u_3 + 1, u_8 + 1} (α := K) (β := E) (⇑(linearProjOfIsCompl q i hi h ∘ₗ f) : (a : K) → E)
have hg : Function.Bijective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥i.range) (⇑(i.range.projectionOnto q h ∘ₗ f) : (a : K) → ↥i.range)
Tactic: rw [LinearMap.linearProjOfIsCompl, LinearMap.comp_assoc, LinearMap.coe_comp,
      Function.Bijective.of_comp_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
have rw : N = span R (image (α := ↥N) (⇑N.subtype : (a : ↥N) → M) (Set.range (ι := Fin n) (⇑b : (a : Fin n) → ↥N)))
Tactic: rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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)))
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
have rw₁ : N = map N.subtype (span R (Set.range (ι := Fin n) (⇑b : (a : Fin n) → ↥N)))
Tactic: rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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)))
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
have rw₂ : N = map N.subtype ⊤
Tactic: rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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 ⊤
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
have rw₃ : N = N
Tactic: rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (hypothesis)
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
⊢ c = 0
have hx₁ : x ∈ N
Tactic: rw [← span_b] at hx
Cleared hypotheses: hx, hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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) (⇑(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)))
have unfold : Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M)
  (⇑(have span_b := sorry;
      Basis.mk sorry sorry) :
    (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
have rw : N = span R (image (α := ↥N) (⇑N.subtype : (a : ↥N) → M) (Set.range (ι := Fin n) (⇑b : (a : Fin n) → ↥N)))
Tactic: rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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)))
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
have rw₁ : N = map N.subtype (span R (Set.range (ι := Fin n) (⇑b : (a : Fin n) → ↥N)))
Tactic: rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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)))
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
have rw₂ : N = map N.subtype ⊤
Tactic: rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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 ⊤
⊢ N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
have rw₃ : N = N
Tactic: rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (hypothesis)
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
⊢ c = 0
have hx₁ : x ∈ N
Tactic: rw [← span_b] at hx
Cleared hypotheses: hx, hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Fin (goal)
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
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
⊢ Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M) (⇑(b.mkFinSnoc y hli hsp) : (a : Fin (n + 1)) → M)
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ M)
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)) y)
have unfold : Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M)
  (⇑(have span_b := sorry;
      Basis.mk sorry sorry) :
    (a : Fin (n + 1)) → M)
  (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ M)
    (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)) y)
Tactic: unfold mkFinSnoc
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Flag (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.succ = span R (singleton (α := M) ((b : (a : Fin n) → M) k : M)) ⊔ b.flag k.castSucc
have simp : Eq (α := Submodule R M) (span R (image (α := Fin n) (⇑b : (a : Fin n) → M) {i : Fin n | i.castSucc < k.succ}))
  (span R (singleton (α := M) ((b : (a : Fin n) → M) k : M)) ⊔
    span R (image (α := Fin n) (⇑b : (a : Fin n) → M) {i : Fin n | i < k}))
Tactic: simp only [flag, Fin.castSucc_lt_castSucc_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Flag (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ b.flag k.succ
have rw : b.flag k.castSucc ≤ span R (singleton (α := M) ((b : (a : Fin n) → M) k : M)) ⊔ b.flag k.castSucc
Tactic: rw [flag_succ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Flag (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
h : k ≤ l.castSucc
⊢ b.flag k ≤ (b.coord l).ker
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Flag (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((b.dualBasis : (a : Fin n) → Dual R M) k)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Flag (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
h : Nontrivial R
⊢ b.flag k.castSucc ≤ LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((b.dualBasis : (a : Fin n) → Dual R M) k)
have rw : b.flag k.castSucc ≤ (b.coord k).ker
Tactic: rw [coe_dualBasis, b.flag_le_ker_coord_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Flag (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
h : Nontrivial R
rw : b.flag k.castSucc ≤ (b.coord k).ker
⊢ b.flag k.castSucc ≤ LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((b.dualBasis : (a : Fin n) → Dual R M) k)
have rw₁ : k.castSucc ≤ k.castSucc
Tactic: rw [coe_dualBasis, b.flag_le_ker_coord_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Flag (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ b.flag i.castSucc ⋖ b.flag i.succ
have rw : b.flag i.castSucc ⋖ span K (singleton (α := V) ((b : (a : Fin n) → V) i : V)) ⊔ b.flag i.castSucc
Tactic: rw [flag_succ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Flag (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ b.flag i.castSucc ⋖ span K (singleton (α := V) ((b : (a : Fin n) → V) i : V)) ⊔ b.flag i.castSucc
have h : ((b : (a : Fin n) → V) i : V) ∉ b.flag i.castSucc
Tactic: apply covBy_span_singleton_sup
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.MulOpposite (goal)
Goal:
R : Type u_1
H : Type u_2
inst : DivisionRing R
inst_1 : AddCommGroup H
inst_2 : Module R H
b : Basis (↑(Basis.ofVectorSpaceIndex R H) : Type u_2) R H := Basis.ofVectorSpace R H
⊢ Module.finrank.{u_1, u_2} R Hᵐᵒᵖ = Module.finrank R H
have rw : Module.finrank.{u_1, u_2} R Hᵐᵒᵖ = Nat.card.{u_2} (↑(Basis.ofVectorSpaceIndex R H) : Type u_2)
Tactic: rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b.mulOpposite]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.MulOpposite (goal)
Goal:
R : Type u_1
H : Type u_2
inst : DivisionRing R
inst_1 : AddCommGroup H
inst_2 : Module R H
b : Basis (↑(Basis.ofVectorSpaceIndex R H) : Type u_2) R H := Basis.ofVectorSpace R H
rw : Module.finrank.{u_1, u_2} R Hᵐᵒᵖ = Nat.card.{u_2} (↑(Basis.ofVectorSpaceIndex R H) : Type u_2)
⊢ Module.finrank.{u_1, u_2} R Hᵐᵒᵖ = Module.finrank R H
have rw₁ : Nat.card.{u_2} (↑(Basis.ofVectorSpaceIndex R H) : Type u_2) =
  Nat.card.{u_2} (↑(Basis.ofVectorSpaceIndex R H) : Type u_2)
Tactic: rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b.mulOpposite]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
⊢ Eq (α := ι →₀ R) ((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).1 : ι →₀ R)
    ((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R)
have h : ∀ (j : ι),
  Eq.{u_3 + 1} (α := R)
    (((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).1 : (a : ι) → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) : (a : ι) → R) j : R)
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i j : ι
⊢ Eq.{u_3 + 1} (α := R)
    (((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).1 : (a : ι) → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) : (a : ι) → R) j : R)
have h : Eq.{u_3 + 1} (α := R) ((single (Sum.inl i) 1 : (a : ι ⊕ ι') → R) (Sum.inl j) : R) ((single i 1 : (a : ι) → R) j : R)
Tactic: simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Finsupp.fst_sumFinsuppLEquivProdFinsupp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι'
⊢ Eq (α := ι →₀ R) ((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr i)).1)
    ((b.repr : (a : M) → ι →₀ R) 0)
have h : ∀ (i_1 : ι),
  Eq.{u_3 + 1} (α := R)
    (((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr i)).1 : (a : ι) → R) i_1 : R)
    (((b.repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i_1 : R)
Tactic: ext i