awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projection
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
h :
  ∀ (x : ↥p) (y : ↥f.ker) (this : (↑x : E) + (↑y : E) ∈ p ⊔ f.ker),
    Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto f.ker ⋯ : (a : E) → ↥p) ((↑x : E) + (↑y : E))) : E)
      (↑((f : (a : E) → ↥p) ((↑x : E) + (↑y : E))) : E)
⊢ Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto f.ker ⋯ : (a : E) → ↥p) x) : E) (↑((f : (a : E) → ↥p) x) : E)

Tactic:
rcases mem_sup'.1 this with ⟨x, y, rfl⟩

Premises used: Submodule.mem_sup', Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.Projection
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 : ↥p
y : ↥f.ker
this : (↑x : E) + (↑y : E) ∈ p ⊔ f.ker
⊢ Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto f.ker ⋯ : (a : E) → ↥p) ((↑x : E) + (↑y : E))) : E)
    (↑((f : (a : E) → ↥p) ((↑x : E) + (↑y : E))) : E)

Tactic:
simp [hf]
-- Module: Mathlib.LinearAlgebra.Projection
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.Injective (α := E) (β := F × G) (⇑(f.prod g) : (a : E) → F × G)

Tactic:
simp [← ker_eq_bot, hfg.inf_eq_bot]

Premises used: LinearMap.ker_eq_bot, IsCompl.inf_eq_bot
-- Module: Mathlib.LinearAlgebra.Projection
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
rw : (f.prod g).range = ⊤
⊢ Function.Surjective (α := E) (β := F × G) (⇑(f.prod g) : (a : E) → F × G)

Tactic:
rw [← range_eq_top]

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.Projection
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
⊢ (f.prod g).range = ⊤

Tactic:
simp [range_prod_eq hfg.sup_eq_top, *]

Premises used: IsCompl.sup_eq_top, LinearMap.range_prod_eq
-- Module: Mathlib.LinearAlgebra.Projection
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
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : f.range = ⊤
hg : g.range = ⊤
hfg : IsCompl f.ker g.ker
⊢ (↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) : E →ₗ[R] F × G) = f.prod g

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl
-- Module: Mathlib.LinearAlgebra.Projection
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
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : f.range = ⊤
hg : g.range = ⊤
hfg : IsCompl f.ker g.ker
x : E
⊢ Eq (α := F × G) ((f.equivProdOfSurjectiveOfIsCompl g hf hg hfg : (a : E) → F × G) x : F × G)
    (((f : (a : E) → F) x, (g : (a : E) → G) x) : F × G)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.LinearAlgebra.Projection
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_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
x : { q : Submodule R E // IsCompl p q }
q : Submodule R E
hq : IsCompl p q
⊢ (fun (f : { f : E →ₗ[R] ↥p // ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x }) ↦
        Subtype.mk (p := fun (q : Submodule R E) ↦ IsCompl p q) (↑f : E →ₗ[R] ↥p).ker ⋯)
      ((fun (q : { q : Submodule R E // IsCompl p q }) ↦
          (Subtype.mk (p := fun (f : E →ₗ[R] ↥p) ↦ ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x)
              (p.projectionOnto (↑q : Submodule R E) ⋯) ⋯ :
            { f : E →ₗ[R] ↥p // ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x }))
        (Subtype.mk (p := fun (q : Submodule R E) ↦ IsCompl p q) q hq)) =
    Subtype.mk (p := fun (q : Submodule R E) ↦ IsCompl p q) q hq

Tactic:
simp only [ker_projectionOnto]

Premises used: Submodule.ker_projectionOnto
-- Module: Mathlib.LinearAlgebra.Projection
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
q : { q : Submodule R E // IsCompl p q }
⊢ (↑((p.isComplEquivProj :
            (a : { q : Submodule R E // IsCompl p q }) →
              { f : E →ₗ[R] ↥p // ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x })
          q) :
      E →ₗ[R] ↥p) =
    p.projectionOnto (↑q : Submodule R E) ⋯

Tactic:
rfl

Premises used: Submodule.projectionOnto, rfl
-- Module: Mathlib.LinearAlgebra.Projection
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 : { f : E →ₗ[R] ↥p // ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x }
⊢ (↑((p.isComplEquivProj.symm :
            (a : { f : E →ₗ[R] ↥p // ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x }) →
              { q : Submodule R E // IsCompl p q })
          f) :
      Submodule R E) =
    (↑f : E →ₗ[R] ↥p).ker

Tactic:
rfl

Premises used: LinearMap.ker, Submodule.comap, rfl
-- Module: Mathlib.LinearAlgebra.Projection
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
simp_rw : Membership.mem (α := E) (range (↑f : Module.End R E)) (((↑f : Module.End R E) : (a : E) → E) x : E)
⊢ Membership.mem (α := E) p (((↑f : Module.End R E) : (a : E) → E) x : E)

Tactic:
simp_rw [← f.2.2]

Premises used: And.right, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projection
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) (range (↑f : Module.End R E)) (((↑f : Module.End R E) : (a : E) → E) x : E)

Tactic:
mem_range_self f.1 x

Premises used: LinearMap.mem_range_self, Subtype.val
-- Module: Mathlib.LinearAlgebra.Projection
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) (range (↑f : Module.End R E)) (((↑f : Module.End R E) : (a : E) → E) x : E)

Tactic:
exact mem_range_self f.1 x

Premises used: LinearMap.mem_range_self, Subtype.val
-- Module: Mathlib.LinearAlgebra.Projection
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
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) ⋯ : (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)
⊢ (↑((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)

Tactic:
obtain ⟨x, rfl⟩ := f.2.2.symm ▸ hx

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Projection
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 : Membership.mem (α := E) p (((↑f : Module.End R E) : (a : E) → E) x : E)
⊢ Eq (α := E)
    ((↑((codRestrict p (↑f : Module.End R E) ⋯ : (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:
DFunLike.congr_fun f.2.1 x

Premises used: DFunLike.congr_fun, And.left, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projection
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 : Membership.mem (α := E) p (((↑f : Module.End R E) : (a : E) → E) x : E)
⊢ Eq (α := E)
    ((↑((codRestrict p (↑f : Module.End R E) ⋯ : (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:
exact DFunLike.congr_fun f.2.1 x

Premises used: DFunLike.congr_fun, And.left, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projection
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 : E →ₗ[R] ↥p // ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x }
x : E
⊢ Eq (α := E) ((p.subtype ∘ₗ (↑f : E →ₗ[R] ↥p) * p.subtype ∘ₗ (↑f : E →ₗ[R] ↥p) : (a : E) → E) x : E)
    ((p.subtype ∘ₗ (↑f : E →ₗ[R] ↥p) : (a : E) → E) x : E)

Tactic:
simp [f.2]

Premises used: Subtype.property
-- Module: Mathlib.LinearAlgebra.Projection
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)
rw₂ rw₃ : Eq (α := M) ((f : (a : M) → M) y : M) ((f : (a : M) → M) y : M)
⊢ (f : (a : M) → M) x = x

Tactic:
rw [← hy, ← Module.End.mul_apply, hf.eq]

Premises used: IsIdempotentElem.eq, Module.End.mul_apply
-- Module: Mathlib.LinearAlgebra.Projection
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
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
⊢ IsProj f.range f ↔ 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]⟩⟩
-- Module: Mathlib.LinearAlgebra.Projection
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_1 : 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
h : ∀ (x : M), Eq (α := M) ((f * f : (a : M) → M) x : M) ((f : (a : M) → M) x : M)
⊢ IsIdempotentElem f

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Projection
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
x : M
⊢ Eq (α := M) ((f * f : (a : M) → M) x : M) ((f : (a : M) → M) x : M)

Tactic:
h2 (f x) (h1 x)

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Projection
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
x : M
⊢ Eq (α := M) ((f * f : (a : M) → M) x : M) ((f : (a : M) → M) x : M)

Tactic:
exact h2 (f x) (h1 x)

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Projection
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

Tactic:
⟨fun ⟨p, hp⟩ => ?_, fun h => ⟨_, IsIdempotentElem.isProj_range _ h⟩⟩

Premises used: _private.0.LinearMap.isProj_iff_isIdempotentElem.match_1, LinearMap.range, IsIdempotentElem, Iff.intro, LinearMap.IsIdempotentElem.isProj_range, Exists.intro
-- Module: Mathlib.LinearAlgebra.Projection
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
refine : (∃ (p : Submodule S M), IsProj p f) → ∀ (p : Submodule S M) (hp : IsProj p f), IsIdempotentElem f
⊢ (∃ (p : Submodule S M), IsProj p f) ↔ IsIdempotentElem f

Tactic:
refine ⟨fun ⟨p, hp⟩ => ?_, fun h => ⟨_, IsIdempotentElem.isProj_range _ h⟩⟩
-- Module: Mathlib.LinearAlgebra.Projection
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_1 : ∃ (p : Submodule S M), IsProj p f
p : Submodule S M
hp : IsProj p f
h : ∀ (x : M), Eq (α := M) ((f * f : (a : M) → M) x : M) ((f : (a : M) → M) x : M)
⊢ IsIdempotentElem f

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Projection
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
x : M
⊢ Eq (α := M) ((f * f : (a : M) → M) x : M) ((f : (a : M) → M) x : M)

Tactic:
hp.map_id (f x) (hp.map_mem x)

Premises used: LinearMap.IsProj.map_mem, LinearMap.IsProj.map_id, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Projection
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
x : M
⊢ Eq (α := M) ((f * f : (a : M) → M) x : M) ((f : (a : M) → M) x : M)

Tactic:
exact hp.map_id (f x) (hp.map_mem x)

Premises used: LinearMap.IsProj.map_mem, LinearMap.IsProj.map_id, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Projection
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
⊢ IsIdempotentElem f

Tactic:
f.isProj_iff_isIdempotentElem.mp ⟨m, h⟩

Premises used: Exists.intro, Iff.mp, LinearMap.isProj_iff_isIdempotentElem
-- Module: Mathlib.LinearAlgebra.Projection
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
x : M
⊢ x ∈ m ↔ (f : (a : M) → M) x = x

Tactic:
⟨hf.map_id x, fun h ↦ h ▸ hf.map_mem x⟩

Premises used: LinearMap.IsProj.map_mem, Eq.rec, LinearMap.IsProj.map_id, Iff.intro
-- Module: Mathlib.LinearAlgebra.Projection
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
⊢ Eq (α := M) ((↑((h.codRestrict : (a : M) → ↥m) x) : M) : M) ((f : (a : M) → M) x : M)

Tactic:
f.codRestrict_apply m x

Premises used: LinearMap.codRestrict_apply
-- Module: Mathlib.LinearAlgebra.Projection
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
a : (↑((h.codRestrict : (a : M) → ↥m) (↑x : M)) : M) = (↑x : M)
⊢ (h.codRestrict : (a : M) → ↥m) (↑x : M) = x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Projection
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
a : (f : (a : M) → M) (↑x : M) = (↑x : M)
⊢ (↑((h.codRestrict : (a : M) → ↥m) (↑x : M)) : M) = (↑x : M)

Tactic:
rw [codRestrict_apply]

Premises used: LinearMap.IsProj.codRestrict_apply
-- Module: Mathlib.LinearAlgebra.Projection
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
⊢ (f : (a : M) → M) (↑x : M) = (↑x : M)

Tactic:
h.map_id x x.2

Premises used: LinearMap.IsProj.map_id, Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projection
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
⊢ (f : (a : M) → M) (↑x : M) = (↑x : M)

Tactic:
exact h.map_id x x.2

Premises used: LinearMap.IsProj.map_id, Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projection
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
⊢ h.codRestrict.ker = f.ker

Tactic:
f.ker_codRestrict m _

Premises used: LinearMap.ker_codRestrict, LinearMap.IsProj.codRestrict
-- Module: Mathlib.LinearAlgebra.Projection
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
rw : IsCompl p h.codRestrict.ker
⊢ IsCompl p f.ker

Tactic:
rw [← codRestrict_ker h]

Premises used: LinearMap.IsProj.codRestrict_ker
-- Module: Mathlib.LinearAlgebra.Projection
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 h.codRestrict.ker

Tactic:
isCompl_of_proj h.codRestrict_apply_cod

Premises used: LinearMap.IsProj.codRestrict_apply_cod, LinearMap.isCompl_of_proj
-- Module: Mathlib.LinearAlgebra.Projection
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 h.codRestrict.ker

Tactic:
exact isCompl_of_proj h.codRestrict_apply_cod

Premises used: LinearMap.IsProj.codRestrict_apply_cod, LinearMap.isCompl_of_proj
-- Module: Mathlib.LinearAlgebra.Projection
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
rw :
  f ∘ₗ (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) =
    (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0
⊢ f =
    (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ
      prodMap id 0 ∘ₗ (↑(p.prodEquivOfIsCompl f.ker ⋯).symm : E →ₗ[R] ↥p × ↥f.ker)

Tactic:
rw [← LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]

Premises used: LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm
-- Module: Mathlib.LinearAlgebra.Projection
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)
hr :
  ∀ (x : ↥f.ker),
    Eq (α := E)
      (((f ∘ₗ (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E)) ∘ₗ inr R ↥p ↥f.ker : (a : ↥f.ker) → E) x : E)
      ((((↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0) ∘ₗ inr R ↥p ↥f.ker : (a : ↥f.ker) → 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

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Projection
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
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)

Tactic:
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inl, coprod_apply, coe_subtype,
      map_zero, add_zero, h.map_id x x.2, prodMap_apply, id_apply]

Premises used: LinearMap.prodMap_apply, LinearMap.id_apply, Submodule.coe_prodEquivOfIsCompl, LinearMap.coprod_apply, LinearMap.comp_apply, map_zero, LinearMap.IsProj.map_id, LinearMap.coe_inl, Submodule.coe_subtype, add_zero, Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projection
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
x : ↥f.ker
⊢ Eq (α := E)
    (((f ∘ₗ (↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E)) ∘ₗ inr R ↥p ↥f.ker : (a : ↥f.ker) → E) x : E)
    ((((↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0) ∘ₗ inr R ↥p ↥f.ker : (a : ↥f.ker) → E)
        x :
      E)

Tactic:
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, map_zero,
      coe_subtype, zero_add, map_coe_ker, prodMap_apply, zero_apply, add_zero]

Premises used: LinearMap.zero_apply, LinearMap.prodMap_apply, LinearMap.coe_inr, Submodule.coe_prodEquivOfIsCompl, LinearMap.coprod_apply, LinearMap.comp_apply, map_zero, zero_add, LinearMap.map_coe_ker, Submodule.coe_subtype, add_zero
-- Module: Mathlib.LinearAlgebra.Projection
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
h : ∀ (x : M), x ∈ m₁ ↔ x ∈ m₂
⊢ m₁ = m₂

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Projection
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
x : M
⊢ x ∈ m₁ ↔ x ∈ m₂

Tactic:
simp [hf₁.mem_iff_map_id, hf₂.mem_iff_map_id]

Premises used: LinearMap.IsProj.mem_iff_map_id
-- Module: Mathlib.LinearAlgebra.Projection
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
⊢ f.range = m

Tactic:
h.isIdempotentElem.isProj_range.submodule_unique h

Premises used: LinearMap.IsProj.isIdempotentElem, LinearMap.IsIdempotentElem.isProj_range, LinearMap.IsProj.submodule_unique