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
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
p q : Submodule R E
h : IsCompl p q
φ₁ φ₂ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ₁ ψ₂ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
⊢ ∀ (u : ↥p),
    Eq.{u_3 + 1} (α := F) ((φ₁ + φ₂ : (a : ↥p) → F) u : F)
      ((ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂ : (a : E) → F) (↑u : E) : F)

Tactic:
simp
-- 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
p q : Submodule R E
h : IsCompl p q
φ₁ φ₂ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ₁ ψ₂ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
⊢ ∀ (u : ↥q),
    Eq.{u_3 + 1} (α := F) ((ψ₁ + ψ₂ : (a : ↥q) → F) u : F)
      ((ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂ : (a : E) → F) (↑u : E) : F)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_7
inst : CommRing R
E : Type u_8
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_9
inst_3 : AddCommGroup F
inst_4 : Module R F
p q : Submodule R E
h : IsCompl p q
φ : LinearMap.{u_7, u_7, u_8, u_9} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_7, u_7, u_8, u_9} (RingHom.id R) (↥q) F
c : R
⊢ ∀ (u : ↥p), Eq.{u_9 + 1} (α := F) ((c • φ : (a : ↥p) → F) u : F) ((c • ofIsCompl h φ ψ : (a : E) → F) (↑u : E) : F)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_7
inst : CommRing R
E : Type u_8
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_9
inst_3 : AddCommGroup F
inst_4 : Module R F
p q : Submodule R E
h : IsCompl p q
φ : LinearMap.{u_7, u_7, u_8, u_9} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_7, u_7, u_8, u_9} (RingHom.id R) (↥q) F
c : R
⊢ ∀ (u : ↥q), Eq.{u_9 + 1} (α := F) ((c • ψ : (a : ↥q) → F) u : F) ((c • ofIsCompl h φ ψ : (a : E) → F) (↑u : E) : F)

Tactic:
simp
-- 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 q : Submodule R E
M : Type u_6
inst_3 : AddCommMonoid M
h : IsCompl p q
inst_4 : Module R M
f : LinearMap.{u_1, u_1, u_6, u_2} (RingHom.id R) M ↥p
h₁ :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto q h ∘ₗ p.subtype ∘ₗ f : (a : M) → ↥p) x) : E)
      (↑((f : (a : M) → ↥p) x) : E)
⊢ p.projectionOnto q h ∘ₗ p.subtype ∘ₗ f = f

Tactic:
ext
-- 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 q : Submodule R E
M : Type u_6
inst_3 : AddCommMonoid M
h : IsCompl p q
inst_4 : Module R M
f : LinearMap.{u_1, u_1, u_6, u_2} (RingHom.id R) M ↥p
x : M
⊢ Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto q h ∘ₗ p.subtype ∘ₗ f : (a : M) → ↥p) x) : E) (↑((f : (a : M) → ↥p) x) : E)

Tactic:
simp
-- 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
M : Type u_6
inst_3 : AddCommMonoid M
h_1 : IsComplemented p
inst_4 : Module R M
q : Submodule R E
h : IsCompl p q
f : LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) (↥p) M
h₁ :
  ∀ (x : ↥p),
    Eq.{u_6 + 1} (α := M) (((fun (f : E →ₗ[R] M) ↦ f ∘ₗ p.subtype) (f ∘ₗ p.projectionOnto q h) : (a : ↥p) → M) x : M)
      ((f : (a : ↥p) → M) x : M)
⊢ (fun (f : E →ₗ[R] M) ↦ f ∘ₗ p.subtype) (f ∘ₗ p.projectionOnto q h) = f

Tactic:
ext
-- 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
M : Type u_6
inst_3 : AddCommMonoid M
h_1 : IsComplemented p
inst_4 : Module R M
q : Submodule R E
h : IsCompl p q
f : LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) (↥p) M
x : ↥p
⊢ Eq.{u_6 + 1} (α := M) (((fun (f : E →ₗ[R] M) ↦ f ∘ₗ p.subtype) (f ∘ₗ p.projectionOnto q h) : (a : ↥p) → M) x : M)
    ((f : (a : ↥p) → M) x : M)

Tactic:
simp
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
rw : (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range = φ.range ⊔ ψ.range
⊢ (ofIsCompl hpq φ ψ).range = φ.range ⊔ ψ.range

Tactic:
rw [ofIsCompl_eq_add]

Premises used: LinearMap.ofIsCompl_eq_add
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
a : (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range
a₁ : φ.range ⊔ ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range = φ.range ⊔ ψ.range

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
a : (φ ∘ₗ p.projectionOnto q hpq).range ⊔ (ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range

Tactic:
apply range_add_le _ _ |>.trans

Premises used: LE.le.trans, LinearMap.range_add_le
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
a : (φ ∘ₗ p.projectionOnto q hpq).range ≤ φ.range
a₁ : (ψ ∘ₗ q.projectionOnto p ⋯).range ≤ ψ.range
⊢ (φ ∘ₗ p.projectionOnto q hpq).range ⊔ (ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range

Tactic:
gcongr
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
⊢ (φ ∘ₗ p.projectionOnto q hpq).range ≤ φ.range

Tactic:
range_comp_le_range ..

Premises used: LinearMap.range_comp_le_range
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
⊢ (φ ∘ₗ p.projectionOnto q hpq).range ≤ φ.range

Tactic:
exact range_comp_le_range ..

Premises used: LinearMap.range_comp_le_range
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
⊢ (ψ ∘ₗ q.projectionOnto p ⋯).range ≤ ψ.range

Tactic:
range_comp_le_range ..

Premises used: LinearMap.range_comp_le_range
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
⊢ (ψ ∘ₗ q.projectionOnto p ⋯).range ≤ ψ.range

Tactic:
exact range_comp_le_range ..

Premises used: LinearMap.range_comp_le_range
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
a : φ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range
a₁ : ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range
⊢ φ.range ⊔ ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range

Tactic:
apply sup_le

Premises used: sup_le
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
x : ↥p
⊢ Eq.{u_3 + 1} (α := F) ((φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯ : (a : E) → F) (↑x : E) : F)
    ((φ : (a : ↥p) → F) x : F)

Tactic:
simp
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
x : ↥p
⊢ Membership.mem (α := F) (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range ((φ : (a : ↥p) → F) x : F)

Tactic:
exact ⟨x, by simp⟩
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
x : ↥q
⊢ Eq.{u_3 + 1} (α := F) ((φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯ : (a : E) → F) (↑x : E) : F)
    ((ψ : (a : ↥q) → F) x : F)

Tactic:
simp
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
x : ↥q
⊢ Membership.mem (α := F) (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range ((ψ : (a : ↥q) → F) x : F)

Tactic:
exact ⟨x, by simp⟩
-- 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 q : Submodule R E
hpq : IsCompl p q
⊢ ofIsCompl hpq p.subtype 0 = p.projection q hpq

Tactic:
simp [ofIsCompl_eq_add, projection]

Premises used: Submodule.projection, LinearMap.ofIsCompl_eq_add
-- 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
p q : Submodule R E
hpq : IsCompl p q
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
⊢ ofIsCompl ⋯ ψ φ = ofIsCompl hpq φ ψ

Tactic:
simp [ofIsCompl_eq_add, add_comm]

Premises used: add_comm, LinearMap.ofIsCompl_eq_add
-- 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_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
rw : ofIsCompl h (φ + ψ).1 (φ.2 + ψ.2) = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
rw₁ : ofIsCompl h (φ.1 + ψ.1) (φ.2 + ψ.2) = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
rw₂ rw₃ : ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2 = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
⊢ ofIsCompl h (φ + ψ).1 (φ + ψ).2 = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2

Tactic:
rw [Prod.snd_add, Prod.fst_add, ofIsCompl_add]

Premises used: LinearMap.ofIsCompl_add, Prod.fst_add, Prod.snd_add
-- 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_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
c : R₁
φ : 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
⊢ ofIsCompl h (c • φ).1 (c • φ).2 = HSMul.hSMul (α := R₁) ((RingHom.id R₁ : (a : R₁) → R₁) c : R₁) (ofIsCompl h φ.1 φ.2)

Tactic:
simp [Prod.smul_snd, Prod.smul_fst, ofIsCompl_smul]

Premises used: LinearMap.ofIsCompl_smul, Prod.smul_snd, Prod.smul_fst
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_2
inst : AddCommGroup E
F : Type u_3
inst_1 : AddCommGroup F
R₁ : Type u_7
inst_2 : CommRing R₁
inst_3 : Module R₁ E
inst_4 : 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
⊢ (ofIsComplProd h : (a : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)) → E →ₗ[R₁] F) φ = ofIsCompl h φ.1 φ.2

Tactic:
rfl

Premises used: LinearMap.ofIsCompl, 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_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)
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)
⊢ (fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) (AddHom.toFun (toAddHom (ofIsComplProd h)) φ) = φ

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
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
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)

Tactic:
ofIsCompl_apply_left h x

Premises used: LinearMap.ofIsCompl_apply_left
-- 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_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
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)

Tactic:
exact ofIsCompl_apply_left h x

Premises used: LinearMap.ofIsCompl_apply_left
-- 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_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
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:
ofIsCompl_apply_right h x

Premises used: LinearMap.ofIsCompl_apply_right
-- 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_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
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:
exact ofIsCompl_apply_right h x

Premises used: LinearMap.ofIsCompl_apply_right
-- 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_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
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)
⊢ AddHom.toFun (toAddHom (ofIsComplProd h)) ((fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) φ) = φ

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
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
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)
⊢ 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

Premises used: Submodule.existsUnique_add_of_isCompl
-- 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_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
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)
⊢ 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:
rw [← hab]
-- 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_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)
        ((↑a : E) + (↑b : E)) :
      F)
    ((φ : (a : E) → F) ((↑a : E) + (↑b : E)) : F)

Tactic:
simp
-- 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
h : ∀ (x : E), Eq.{u_2 + 1} (α := E) (↑((p.projectionOnto f.ker ⋯ : (a : E) → ↥p) x) : E) (↑((f : (a : E) → ↥p) x) : E)
⊢ p.projectionOnto f.ker ⋯ = f

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] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
⊢ x ∈ p ⊔ f.ker

Tactic:
simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]

Premises used: IsCompl.sup_eq_top, LinearMap.isCompl_of_proj, Submodule.mem_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
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
⊢ x ∈ p ⊔ f.ker

Tactic:
have : x ∈ p ⊔ (ker f) := by simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]