awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p_1 q_1 : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
R₁ : Type u_7
inst_10 : CommRing R₁
inst_11 : Module R₁ E
inst_12 : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : LinearMap.{u_7, u_7, u_2, u_3} (RingHom.id R₁) (↥p) F × LinearMap.{u_7, u_7, u_2, u_3} (RingHom.id R₁) (↥q) F
fst :
  ∀ (x : ↥p),
    Eq.{u_3 + 1} (α := F)
      ((((fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) (AddHom.toFun (toAddHom (ofIsComplProd h)) φ)).1 :
            (a : ↥p) → F)
          x :
        F)
      ((φ.1 : (a : ↥p) → F) x : F)
⊢ (fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) (AddHom.toFun (toAddHom (ofIsComplProd h)) φ) = φ
have snd : ∀ (x : ↥q),
  Eq.{u_3 + 1} (α := F)
    ((((fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) (AddHom.toFun (toAddHom (ofIsComplProd h)) φ)).2 :
          (a : ↥q) → F)
        x :
      F)
    ((φ.2 : (a : ↥q) → F) x : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p_1 q_1 : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
R₁ : Type u_7
inst_10 : CommRing R₁
inst_11 : Module R₁ E
inst_12 : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : E →ₗ[R₁] F
⊢ AddHom.toFun (toAddHom (ofIsComplProd h)) ((fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) φ) = φ
have h₁ : ∀ (x : E),
  Eq.{u_3 + 1} (α := F)
    ((AddHom.toFun (toAddHom (ofIsComplProd h)) ((fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) φ) :
          (a : E) → F)
        x :
      F)
    ((φ : (a : E) → F) x : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p_1 q_1 : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
R₁ : Type u_7
inst_10 : CommRing R₁
inst_11 : Module R₁ E
inst_12 : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : E →ₗ[R₁] F
x : E
⊢ Eq.{u_3 + 1} (α := F)
    ((AddHom.toFun (toAddHom (ofIsComplProd h)) ((fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) φ) :
          (a : E) → F)
        x :
      F)
    ((φ : (a : E) → F) x : F)
have h₁ : ∀ (a : ↥p) (b : ↥q) (hab : (↑a : E) + (↑b : E) = x),
  (∀ (r : ↥p) (s : ↥q), (↑r : E) + (↑s : E) = x → r = a ∧ s = b) →
    Eq.{u_3 + 1} (α := F)
      ((AddHom.toFun (toAddHom (ofIsComplProd h)) ((fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) φ) :
            (a : E) → F)
          x :
        F)
      ((φ : (a : E) → F) x : F)
Tactic: obtain ⟨a, b, hab, _⟩ := existsUnique_add_of_isCompl h x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p_1 q_1 : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
R₁ : Type u_7
inst_10 : CommRing R₁
inst_11 : Module R₁ E
inst_12 : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : E →ₗ[R₁] F
x : E
a : ↥p
b : ↥q
hab : (↑a : E) + (↑b : E) = x
right : ∀ (r : ↥p) (s : ↥q), (↑r : E) + (↑s : E) = x → r = a ∧ s = b
⊢ Eq.{u_3 + 1} (α := F)
    ((AddHom.toFun (toAddHom (ofIsComplProd h)) ((fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) φ) :
          (a : E) → F)
        x :
      F)
    ((φ : (a : E) → F) x : F)
have h₁ : Eq.{u_3 + 1} (α := F)
  ((AddHom.toFun (toAddHom (ofIsComplProd h)) ((fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) φ) :
        (a : E) → F)
      ((↑a : E) + (↑b : E)) :
    F)
  ((φ : (a : E) → F) ((↑a : E) + (↑b : E)) : F)
Tactic: rw [← hab]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
⊢ p.projectionOnto f.ker ⋯ = f
have h : ∀ (x : E), Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto f.ker sorry : (a : E) → ↥p) x) : E) (↑((f : (a : E) → ↥p) x) : E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (hypothesis)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
⊢ Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto f.ker ⋯ : (a : E) → ↥p) x) : E) (↑((f : (a : E) → ↥p) x) : E)
have this : x ∈ p ⊔ f.ker
Tactic: have : x ∈ p ⊔ (ker f) := by simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
this : x ∈ p ⊔ f.ker
⊢ Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto f.ker ⋯ : (a : E) → ↥p) x) : E) (↑((f : (a : E) → ↥p) x) : E)
have h : ∀ (x : ↥p) (y : ↥f.ker) (this : (↑x : E) + (↑y : E) ∈ p ⊔ f.ker),
  Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto f.ker sorry : (a : E) → ↥p) ((↑x : E) + (↑y : E))) : E)
    (↑((f : (a : E) → ↥p) ((↑x : E) + (↑y : E))) : E)
Tactic: rcases mem_sup'.1 this with ⟨x, y, rfl⟩
Cleared hypotheses: x, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : f.range = ⊤
hg : g.range = ⊤
hfg : IsCompl f.ker g.ker
⊢ Function.Surjective (α := E) (β := F × G) (⇑(f.prod g) : (a : E) → F × G)
have rw : (f.prod g).range = ⊤
Tactic: rw [← range_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
f : { f : Module.End R E // IsIdempotentElem f ∧ range f = p }
x : E
⊢ Membership.mem (α := E) p (((↑f : Module.End R E) : (a : E) → E) x : E)
have simp_rw : Membership.mem (α := E) (range (↑f : Module.End R E)) (((↑f : Module.End R E) : (a : E) → E) x : E)
Tactic: simp_rw [← f.2.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
f : { f : Module.End R E // IsIdempotentElem f ∧ range f = p }
x_1 : ↥p
x : E
hx : x ∈ p
⊢ (↑((codRestrict p (↑f : Module.End R E) ⋯ : (a : E) → ↥p) (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p) x hx) : E)) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p) x hx) : E)
have obtain : ∀ (x : E) (hx : Membership.mem (α := E) p (((↑f : Module.End R E) : (a : E) → E) x : E)),
  Eq (α := E)
    ((↑((codRestrict p (↑f : Module.End R E) sorry : (a : E) → ↥p)
            (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p) (((↑f : Module.End R E) : (a : E) → E) x) hx) : E)) :
        E) :
      E)
    ((↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p) (((↑f : Module.End R E) : (a : E) → E) x) hx) : E) : E)
Tactic: obtain ⟨x, rfl⟩ := f.2.2.symm ▸ hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
hf : IsIdempotentElem f
x : M
h : x ∈ f.range
y : M
hy : (f : (a : M) → M) y = x
⊢ (f : (a : M) → M) x = x
have rw : Eq (α := M) ((f : (a : M) → M) ((f : (a : M) → M) y : M) : M) ((f : (a : M) → M) y : M)
Tactic: rw [← hy, ← Module.End.mul_apply, hf.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
hf : IsIdempotentElem f
x : M
h : x ∈ f.range
y : M
hy : (f : (a : M) → M) y = x
rw : Eq (α := M) ((f : (a : M) → M) ((f : (a : M) → M) y : M) : M) ((f : (a : M) → M) y : M)
⊢ (f : (a : M) → M) x = x
have rw₁ : Eq (α := M) ((f * f : (a : M) → M) y : M) ((f : (a : M) → M) y : M)
Tactic: rw [← hy, ← Module.End.mul_apply, hf.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
hf : IsIdempotentElem f
x : M
h : x ∈ f.range
y : M
hy : (f : (a : M) → M) y = x
rw : Eq (α := M) ((f : (a : M) → M) ((f : (a : M) → M) y : M) : M) ((f : (a : M) → M) y : M)
rw₁ : Eq (α := M) ((f * f : (a : M) → M) y : M) ((f : (a : M) → M) y : M)
⊢ (f : (a : M) → M) x = x
have rw₂ : Eq (α := M) ((f : (a : M) → M) y : M) ((f : (a : M) → M) y : M)
Tactic: rw [← hy, ← Module.End.mul_apply, hf.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
⊢ IsProj f.range f ↔ IsIdempotentElem f
have refine : IsProj f.range f →
  ∀ (h1 : ∀ (x : M), Membership.mem (α := M) f.range ((f : (a : M) → M) x : M))
    (h2 : ∀ x ∈ f.range, (f : (a : M) → M) x = x), IsIdempotentElem f
Tactic: refine ⟨fun ⟨h1, h2⟩ => ?_, fun hf =>
    ⟨fun x => mem_range_self f x, fun x ⟨y, hy⟩ => by rw [← hy, ← Module.End.mul_apply, hf.eq]⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
h : IsProj f.range f
h1 : ∀ (x : M), Membership.mem (α := M) f.range ((f : (a : M) → M) x : M)
h2 : ∀ x ∈ f.range, (f : (a : M) → M) x = x
⊢ IsIdempotentElem f
have h : ∀ (x : M), Eq (α := M) ((f * f : (a : M) → M) x : M) ((f : (a : M) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
⊢ (∃ (p : Submodule S M), IsProj p f) ↔ IsIdempotentElem f
have refine : (∃ (p : Submodule S M), IsProj p f) → ∀ (p : Submodule S M) (hp : IsProj p f), IsIdempotentElem f
Tactic: refine ⟨fun ⟨p, hp⟩ => ?_, fun h => ⟨_, IsIdempotentElem.isProj_range _ h⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
h : ∃ (p : Submodule S M), IsProj p f
p : Submodule S M
hp : IsProj p f
⊢ IsIdempotentElem f
have h : ∀ (x : M), Eq (α := M) ((f * f : (a : M) → M) x : M) ((f : (a : M) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : ↥m
⊢ (h.codRestrict : (a : M) → ↥m) (↑x : M) = x
have a : (↑((h.codRestrict : (a : M) → ↥m) (↑x : M)) : M) = (↑x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : ↥m
⊢ (↑((h.codRestrict : (a : M) → ↥m) (↑x : M)) : M) = (↑x : M)
have a : (f : (a : M) → M) (↑x : M) = (↑x : M)
Tactic: rw [codRestrict_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p f.ker
have rw : IsCompl p h.codRestrict.ker
Tactic: rw [← codRestrict_ker h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f =
    (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ
      prodMap id 0 ∘ₗ (↑(p.prodEquivOfIsCompl f.ker ⋯).symm : E →ₗ[R] ↥p × ↥f.ker)
have rw : f ∘ₗ (↑(p.prodEquivOfIsCompl f.ker sorry) : ↥p × ↥f.ker →ₗ[R] E) =
  (↑(p.prodEquivOfIsCompl f.ker sorry) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0
Tactic: rw [← LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f ∘ₗ (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) =
    (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0
have hl : ∀ (x : ↥p),
  Eq (α := E) (((f ∘ₗ (↑(p.prodEquivOfIsCompl f.ker sorry) : ↥p × ↥f.ker →ₗ[R] E)) ∘ₗ inl R ↥p ↥f.ker : (a : ↥p) → E) x : E)
    ((((↑(p.prodEquivOfIsCompl f.ker sorry) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0) ∘ₗ inl R ↥p ↥f.ker : (a : ↥p) → E) x :
      E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
hl :
  ∀ (x : ↥p),
    Eq (α := E)
      (((f ∘ₗ (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E)) ∘ₗ inl R ↥p ↥f.ker : (a : ↥p) → E) x : E)
      ((((↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0) ∘ₗ inl R ↥p ↥f.ker : (a : ↥p) → E) x :
        E)
⊢ f ∘ₗ (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) =
    (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0
have hr : ∀ (x : ↥f.ker),
  Eq (α := E)
    (((f ∘ₗ (↑(p.prodEquivOfIsCompl f.ker sorry) : ↥p × ↥f.ker →ₗ[R] E)) ∘ₗ inr R ↥p ↥f.ker : (a : ↥f.ker) → E) x : E)
    ((((↑(p.prodEquivOfIsCompl f.ker sorry) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0) ∘ₗ inr R ↥p ↥f.ker : (a : ↥f.ker) → E)
        x :
      E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
m₁ m₂ : Submodule S M
hf₁ : IsProj m₁ f
hf₂ : IsProj m₂ f
⊢ m₁ = m₂
have h : ∀ (x : M), x ∈ m₁ ↔ x ∈ m₂
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
⊢ m = ⊤ ↔ f = id
have mp : m = ⊤ → f = id
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
mp : m = ⊤ → f = id
⊢ m = ⊤ ↔ f = id
have mpr : f = id → m = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
hf : IsProj.{u_5, u_6, u_6} (S := S) (M := M) ⊤ f
⊢ f = id
have mp : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((id : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
hf : IsProj m (F := M →ₗ[S] M) id
⊢ m = ⊤
have mpr : Eq.{u_6 + 1} (α := Submodule S M) (range id) ⊤
Tactic: rw [← hf.range, range_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
hf : IsProj m (F := M →ₗ[S] M) id
mpr : Eq.{u_6 + 1} (α := Submodule S M) (range id) ⊤
⊢ m = ⊤
have mpr₁ : Eq.{u_6 + 1} (α := Submodule S M) ⊤ ⊤
Tactic: rw [← hf.range, range_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
⊢ m = ⊥ ↔ f = 0
have mp : m = ⊥ → f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
mp : m = ⊥ → f = 0
⊢ m = ⊥ ↔ f = 0
have mpr : f = 0 → m = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
hf : IsProj.{u_5, u_6, u_6} (S := S) (M := M) ⊥ f
⊢ f = 0
have mp : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
hf : IsProj m (F := M →ₗ[S] M) 0
⊢ m = ⊥
have mpr : Eq.{u_6 + 1} (α := Submodule S M) (range (R := S) (M := M) (τ₁₂ := RingHom.id S) 0) ⊥
Tactic: rw [← hf.range, range_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
hf : IsProj m (F := M →ₗ[S] M) 0
mpr : Eq.{u_6 + 1} (α := Submodule S M) (range (R := S) (M := M) (τ₁₂ := RingHom.id S) 0) ⊥
⊢ m = ⊥
have mpr₁ : Eq.{u_6 + 1} (α := Submodule S M) ⊥ ⊥
Tactic: rw [← hf.range, range_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ T = T.range.projection T.ker ⋯
have h : T = ofIsCompl sorry T.range.subtype 0
Tactic: convert! ofIsCompl_subtype_zero_eq hT.isCompl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst_3 : AddCommMonoid E
inst_4 : Module S E
p : E →ₗ[S] M
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range
have simp_rw : (∀ (x : E), Eq.{u_6 + 1} (α := M) ((q ∘ₗ p : (a : E) → M) x : M) ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
Tactic: simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff,
    SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst_3 : AddCommMonoid E
inst_4 : Module S E
p : E →ₗ[S] M
simp_rw :
  (∀ (x : E), Eq.{u_6 + 1} (α := M) ((q ∘ₗ p : (a : E) → M) x : M) ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range
have simp_rw₁ : (∀ (x : E), Eq (α := M) ((q : (a : M) → M) ((p : (a : E) → M) x : M) : M) ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
Tactic: simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff,
    SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst_3 : AddCommMonoid E
inst_4 : Module S E
p : E →ₗ[S] M
simp_rw :
  (∀ (x : E), Eq.{u_6 + 1} (α := M) ((q ∘ₗ p : (a : E) → M) x : M) ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
simp_rw₁ :
  (∀ (x : E), Eq (α := M) ((q : (a : M) → M) ((p : (a : E) → M) x : M) : M) ((p : (a : E) → M) x : M)) ↔
    p.range ≤ q.range
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range
have simp_rw₂ : (∀ (x : E), Membership.mem (α := M) q.range ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
Tactic: simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff,
    SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst_3 : AddCommMonoid E
inst_4 : Module S E
p : E →ₗ[S] M
simp_rw :
  (∀ (x : E), Eq.{u_6 + 1} (α := M) ((q ∘ₗ p : (a : E) → M) x : M) ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
simp_rw₁ :
  (∀ (x : E), Eq (α := M) ((q : (a : M) → M) ((p : (a : E) → M) x : M) : M) ((p : (a : E) → M) x : M)) ↔
    p.range ≤ q.range
simp_rw₂ : (∀ (x : E), Membership.mem (α := M) q.range ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range
have simp_rw₃ : (∀ (x : E), Membership.mem (α := M) q.range ((p : (a : E) → M) x : M)) ↔ ∀ ⦃x : M⦄, x ∈ p.range → x ∈ q.range
Tactic: simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff,
    SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst_3 : AddCommMonoid E
inst_4 : Module S E
p : E →ₗ[S] M
simp_rw :
  (∀ (x : E), Eq.{u_6 + 1} (α := M) ((q ∘ₗ p : (a : E) → M) x : M) ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
simp_rw₁ :
  (∀ (x : E), Eq (α := M) ((q : (a : M) → M) ((p : (a : E) → M) x : M) : M) ((p : (a : E) → M) x : M)) ↔
    p.range ≤ q.range
simp_rw₂ : (∀ (x : E), Membership.mem (α := M) q.range ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
simp_rw₃ : (∀ (x : E), Membership.mem (α := M) q.range ((p : (a : E) → M) x : M)) ↔ ∀ ⦃x : M⦄, x ∈ p.range → x ∈ q.range
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range
have simp_rw₄ : (∀ (x : E), ∃ (y : M), Eq (α := M) ((q : (a : M) → M) y : M) ((p : (a : E) → M) x : M)) ↔
  ∀ ⦃x : M⦄, (∃ (y : E), (p : (a : E) → M) y = x) → ∃ (y : M), (q : (a : M) → M) y = x
Tactic: simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff,
    SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst_3 : AddCommMonoid E
inst_4 : Module S E
p : E →ₗ[S] M
simp_rw :
  (∀ (x : E), Eq.{u_6 + 1} (α := M) ((q ∘ₗ p : (a : E) → M) x : M) ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
simp_rw₁ :
  (∀ (x : E), Eq (α := M) ((q : (a : M) → M) ((p : (a : E) → M) x : M) : M) ((p : (a : E) → M) x : M)) ↔
    p.range ≤ q.range
simp_rw₂ : (∀ (x : E), Membership.mem (α := M) q.range ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
simp_rw₃ : (∀ (x : E), Membership.mem (α := M) q.range ((p : (a : E) → M) x : M)) ↔ ∀ ⦃x : M⦄, x ∈ p.range → x ∈ q.range
simp_rw₄ :
  (∀ (x : E), ∃ (y : M), Eq (α := M) ((q : (a : M) → M) y : M) ((p : (a : E) → M) x : M)) ↔
    ∀ ⦃x : M⦄, (∃ (y : E), (p : (a : E) → M) y = x) → ∃ (y : M), (q : (a : M) → M) y = x
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range
have simp_rw₅ : (∀ (x : E), ∃ (y : M), Eq (α := M) ((q : (a : M) → M) y : M) ((p : (a : E) → M) x : M)) ↔
  ∀ ⦃x : M⦄ (x_1 : E) (h : (p : (a : E) → M) x_1 = x), ∃ (y : M), (q : (a : M) → M) y = x
Tactic: simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff,
    SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]