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 q : Submodule R E
h : IsCompl p q
⊢ p.projectionOnto q h ∘ₗ p.subtype = LinearMap.id

Tactic:
LinearMap.ext <| projectionOnto_apply_left h

Premises used: LinearMap.ext, Submodule.projectionOnto_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
p q : Submodule R E
h : IsCompl p q
x : E
⊢ Eq (α := ↥p) ((p.projectionOnto q h : (a : E) → ↥p) ((p.projection q h : (a : E) → E) x) : ↥p)
    ((p.projectionOnto q h : (a : E) → ↥p) x : ↥p)

Tactic:
projectionOnto_apply_left h _

Premises used: Submodule.projectionOnto_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
p q : Submodule R E
hpq : IsCompl p q
⊢ IsIdempotentElem (p.projection q hpq)

Tactic:
LinearMap.ext fun _ ↦ congr($(projectionOnto_projection hpq _))

Premises used: LinearMap.ext, congrArg, Submodule.projectionOnto_projection, id, IsIdempotentElem, 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
p q : Submodule R E
hc : IsCompl p q
x : E
⊢ ∃! u : ↥p × ↥q, (↑u.1 : E) + (↑u.2 : E) = x

Tactic:
(prodEquivOfIsCompl _ _ hc).toEquiv.bijective.existsUnique _

Premises used: Submodule.prodEquivOfIsCompl, Equiv.bijective, Function.Bijective.existsUnique, LinearEquiv.toEquiv
-- 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
hc : IsCompl p q
x : E
⊢ ∃ (u : ↥p) (v : ↥q), (↑u : E) + (↑v : E) = x ∧ ∀ (r : ↥p) (s : ↥q), (↑r : E) + (↑s : E) = x → r = u ∧ s = v

Tactic:
let ⟨u, hu₁, hu₂⟩ := existsUnique_add_of_isCompl_prod hc x
  ⟨u.1, u.2, hu₁, fun r s hrs => Prod.eq_iff_fst_eq_snd_eq.1 (hu₂ ⟨r, s⟩ hrs)⟩

Premises used: _private.0.Submodule.existsUnique_add_of_isCompl.match_1, Exists, Prod.mk, Prod.fst, And, HAdd.hAdd, And.intro, Exists.intro, Iff.mp, Prod.eq_iff_fst_eq_snd_eq, Subtype.val, Eq, Prod.snd, Submodule.existsUnique_add_of_isCompl_prod
-- 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
x : E
dsimp :
  HAdd.hAdd (α := E) (β := E)
      ((p.subtype ∘ₗ LinearMap.fst R ↥p ↥q ∘ₗ (↑(p.prodEquivOfIsCompl q hpq).symm : E →ₗ[R] ↥p × ↥q) : (a : E) → E) x :
        E)
      ((q.subtype ∘ₗ LinearMap.fst R ↥q ↥p ∘ₗ (↑(q.prodEquivOfIsCompl p ⋯).symm : E →ₗ[R] ↥q × ↥p) : (a : E) → E) x :
        E) =
    x
⊢ HAdd.hAdd (α := E) (β := E) ((p.projection q hpq : (a : E) → E) x : E) ((q.projection p ⋯ : (a : E) → E) x : E) = x

Tactic:
dsimp only [projection, projectionOnto]

Premises used: Submodule.projection, Submodule.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 q : Submodule R E
hpq : IsCompl p q
x : E
rw :
  HAdd.hAdd (α := E) (β := E)
      ((p.subtype ∘ₗ LinearMap.fst R ↥p ↥q ∘ₗ (↑(p.prodEquivOfIsCompl q hpq).symm : E →ₗ[R] ↥p × ↥q) : (a : E) → E) x :
        E)
      ((q.subtype ∘ₗ
              LinearMap.fst R ↥q ↥p ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q hpq)) : E →ₗ[R] ↥q × ↥p) :
            (a : E) → E)
          x :
        E) =
    x
⊢ HAdd.hAdd (α := E) (β := E)
      ((p.subtype ∘ₗ LinearMap.fst R ↥p ↥q ∘ₗ (↑(p.prodEquivOfIsCompl q hpq).symm : E →ₗ[R] ↥p × ↥q) : (a : E) → E) x :
        E)
      ((q.subtype ∘ₗ LinearMap.fst R ↥q ↥p ∘ₗ (↑(q.prodEquivOfIsCompl p ⋯).symm : E →ₗ[R] ↥q × ↥p) : (a : E) → E) x :
        E) =
    x

Tactic:
rw [← prodComm_trans_prodEquivOfIsCompl _ _ hpq]

Premises used: Submodule.prodComm_trans_prodEquivOfIsCompl
-- 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
x : E
⊢ HAdd.hAdd (α := E) (β := E)
      ((p.subtype ∘ₗ LinearMap.fst R ↥p ↥q ∘ₗ (↑(p.prodEquivOfIsCompl q hpq).symm : E →ₗ[R] ↥p × ↥q) : (a : E) → E) x :
        E)
      ((q.subtype ∘ₗ
              LinearMap.fst R ↥q ↥p ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q hpq)) : E →ₗ[R] ↥q × ↥p) :
            (a : E) → E)
          x :
        E) =
    x

Tactic:
(prodEquivOfIsCompl _ _ hpq).apply_symm_apply x

Premises used: Submodule.prodEquivOfIsCompl, LinearEquiv.apply_symm_apply
-- 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
x : E
⊢ HAdd.hAdd (α := E) (β := E)
      ((p.subtype ∘ₗ LinearMap.fst R ↥p ↥q ∘ₗ (↑(p.prodEquivOfIsCompl q hpq).symm : E →ₗ[R] ↥p × ↥q) : (a : E) → E) x :
        E)
      ((q.subtype ∘ₗ
              LinearMap.fst R ↥q ↥p ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q hpq)) : E →ₗ[R] ↥q × ↥p) :
            (a : E) → E)
          x :
        E) =
    x

Tactic:
exact (prodEquivOfIsCompl _ _ hpq).apply_symm_apply x

Premises used: Submodule.prodEquivOfIsCompl, LinearEquiv.apply_symm_apply
-- 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
⊢ p.projection q hpq + q.projection p ⋯ = LinearMap.id

Tactic:
LinearMap.ext (projection_add_projection_eq_self hpq)

Premises used: LinearMap.ext, Submodule.projection_add_projection_eq_self
-- 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
x : E
rw : HAdd.hAdd (α := E) (β := E) ((q.projection p ⋯ : (a : E) → E) x : E) ((p.projection q hpq : (a : E) → E) x : E) = x
rw₁ rw₂ : x = x
⊢ (q.projection p ⋯ : (a : E) → E) x = HSub.hSub (β := E) x ((p.projection q hpq : (a : E) → E) x : E)

Tactic:
rw [eq_sub_iff_add_eq, projection_add_projection_eq_self]

Premises used: eq_sub_iff_add_eq, Submodule.projection_add_projection_eq_self
-- 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
⊢ q.projection p ⋯ = LinearMap.id - p.projection q hpq

Tactic:
LinearMap.ext (projection_eq_self_sub_projection hpq)

Premises used: LinearMap.ext, Submodule.projection_eq_self_sub_projection
-- 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
x : E
rw : x = (p.projection q hpq : (a : E) → E) x ↔ x ∈ p
rw₁ : HSub.hSub (β := E) x ((p.projection q hpq : (a : E) → E) x : E) = 0 ↔ x ∈ p
rw₂ : Eq (α := E) ((q.projection p ⋯ : (a : E) → E) x : E) (0 : E) ↔ x ∈ p
rw₃ rw₄ : x ∈ p ↔ x ∈ p
⊢ (p.projection q hpq : (a : E) → E) x = x ↔ x ∈ p

Tactic:
rw [eq_comm, ← sub_eq_zero, ← projection_eq_self_sub_projection, projection_apply_eq_zero_iff]

Premises used: sub_eq_zero, eq_comm, Submodule.projection_eq_self_sub_projection, Submodule.projection_apply_eq_zero_iff
-- 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
x : E
⊢ Eq (α := ↥p × ↥q) (((p.prodEquivOfIsCompl q hpq).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q)
    (((p.projectionOnto q hpq : (a : E) → ↥p) x, (q.projectionOnto p ⋯ : (a : E) → ↥q) x) : ↥p × ↥q)

Tactic:
Prod.ext rfl congr(($(prodComm_trans_prodEquivOfIsCompl p q hpq).symm x).1)

Premises used: LinearEquiv.symm, congrArg, id, Submodule.prodComm_trans_prodEquivOfIsCompl, Prod.fst, Prod.ext, DFunLike.coe, 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 q : Submodule R E
hpq : IsCompl p q
⊢ ∀ (x : E),
    Eq (α := ↥p × ↥q) (((↑(p.prodEquivOfIsCompl q hpq).symm : E →ₗ[R] ↥p × ↥q) : (a : E) → ↥p × ↥q) x : ↥p × ↥q)
      (((p.projectionOnto q hpq).prod (q.projectionOnto p ⋯) : (a : E) → ↥p × ↥q) x : ↥p × ↥q)

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
h : IsCompl p q
x : E
rw : Membership.mem (α := E) q ((q.projection p ⋯ : (a : E) → E) x : E)
⊢ HSub.hSub (β := E) x ((p.projection q h : (a : E) → E) x : E) ∈ q

Tactic:
rw [← projection_eq_self_sub_projection h]

Premises used: Submodule.projection_eq_self_sub_projection
-- 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
h : IsCompl p q
x : E
⊢ Membership.mem (α := E) q ((q.projection p ⋯ : (a : E) → E) x : E)

Tactic:
projection_apply_mem h.symm x

Premises used: Submodule.projection_apply_mem, IsCompl.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 q : Submodule R E
h : IsCompl p q
x : E
⊢ Membership.mem (α := E) q ((q.projection p ⋯ : (a : E) → E) x : E)

Tactic:
exact projection_apply_mem h.symm x

Premises used: Submodule.projection_apply_mem, IsCompl.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
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
h : IsCompl p q
⊢ p ≤ (q.projectionOnto p ⋯).ker

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
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
h : IsCompl p q
h₁ :
  ∀ (x : ↥q),
    Eq.{u_2 + 1} (α := E) (↑((p.liftQ (q.projectionOnto p ⋯) ⋯ ∘ₗ p.mkQ ∘ₗ q.subtype : (a : ↥q) → ↥q) x) : E)
      (↑((LinearMap.id : (a : ↥q) → ↥q) x) : E)
⊢ p.liftQ (q.projectionOnto p ⋯) ⋯ ∘ₗ p.mkQ ∘ₗ q.subtype = LinearMap.id

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
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
h : IsCompl p q
x : ↥q
⊢ Eq.{u_2 + 1} (α := E) (↑((p.liftQ (q.projectionOnto p ⋯) ⋯ ∘ₗ p.mkQ ∘ₗ q.subtype : (a : ↥q) → ↥q) x) : E)
    (↑((LinearMap.id : (a : ↥q) → ↥q) 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
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
h : IsCompl p q
h₁ :
  ∀ (x : E),
    Eq (α := E ⧸ p) ((((p.mkQ ∘ₗ q.subtype) ∘ₗ p.liftQ (q.projectionOnto p ⋯) ⋯) ∘ₗ p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p)
      ((LinearMap.id ∘ₗ p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p)
⊢ (p.mkQ ∘ₗ q.subtype) ∘ₗ p.liftQ (q.projectionOnto p ⋯) ⋯ = LinearMap.id

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
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
h : IsCompl p q
x : E
⊢ Eq (α := E ⧸ p) ((((p.mkQ ∘ₗ q.subtype) ∘ₗ p.liftQ (q.projectionOnto p ⋯) ⋯) ∘ₗ p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p)
    ((LinearMap.id ∘ₗ p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p)

Tactic:
simp [Quotient.eq, sub_mem_comm_iff, sub_projection_mem]

Premises used: Submodule.Quotient.eq, Submodule.sub_projection_mem, sub_mem_comm_iff
-- 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
h : IsCompl p q
x : E
⊢ Eq (α := ↥q) ((p.quotientEquivOfIsCompl q h : (a : E ⧸ p) → ↥q) (Quotient.mk x) : ↥q)
    ((q.projectionOnto p ⋯ : (a : E) → ↥q) x : ↥q)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, 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 q : Submodule R E
h : IsCompl p q
x : ↥q
⊢ (p.quotientEquivOfIsCompl q h : (a : E ⧸ p) → ↥q) (Quotient.mk (↑x : E)) = x

Tactic:
(quotientEquivOfIsCompl p q h).apply_symm_apply x

Premises used: Submodule.Quotient.mk, Submodule.quotientEquivOfIsCompl, LinearEquiv.apply_symm_apply
-- 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
h : IsCompl p q
x : E ⧸ p
⊢ Quotient.mk (↑((p.quotientEquivOfIsCompl q h : (a : E ⧸ p) → ↥q) x) : E) = x

Tactic:
(quotientEquivOfIsCompl p q h).symm_apply_apply x

Premises used: Submodule.Quotient.mk, LinearEquiv.symm_apply_apply, Submodule.quotientEquivOfIsCompl
-- 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
h : IsCompl p q
⊢ (↑(p.quotientEquivOfIsCompl q h) : E ⧸ p →ₗ[R] ↥q) = p.liftQ (q.projectionOnto p ⋯) ⋯

Tactic:
rfl

Premises used: Submodule.liftQ, 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 q : Submodule R E
h : IsCompl p q
⊢ (↑(p.quotientEquivOfIsCompl q h).symm : ↥q →ₗ[R] E ⧸ p) = p.mkQ ∘ₗ q.subtype

Tactic:
rfl

Premises used: Submodule.Quotient.mk, 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
q : Submodule R E
F : Type u_7
inst_3 : AddCommGroup F
inst_4 : Module R F
i : F →ₗ[R] E
hi : Function.Injective.{u_7 + 1, u_2 + 1} (α := F) (β := E) (⇑i : (a : F) → E)
h : IsCompl i.range q
x : F
obtain :
  ∀ (ix : ↥i.range),
    Eq.{u_7 + 1} (α := F)
      ((linearProjOfIsCompl q i hi h : (a : E) → F)
          ((i : (a : F) → E) ((LinearEquiv.symm (LinearEquiv.ofInjective i hi) : (a : ↥i.range) → F) ix : F) : E) :
        F)
      ((LinearEquiv.symm (LinearEquiv.ofInjective i hi) : (a : ↥i.range) → F) ix : F)
⊢ (linearProjOfIsCompl q i hi h : (a : E) → F) ((i : (a : F) → E) x : E) = x

Tactic:
obtain ⟨ix, rfl⟩ := (LinearEquiv.ofInjective i hi).symm.surjective x

Premises used: LinearEquiv.symm, LinearEquiv.surjective, LinearEquiv.ofInjective, 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
q : Submodule R E
F : Type u_7
inst_3 : AddCommGroup F
inst_4 : Module R F
i : F →ₗ[R] E
hi : Function.Injective.{u_7 + 1, u_2 + 1} (α := F) (β := E) (⇑i : (a : F) → E)
h : IsCompl i.range q
ix : ↥i.range
⊢ Eq.{u_7 + 1} (α := F)
    ((linearProjOfIsCompl q i hi h : (a : E) → F)
        ((i : (a : F) → E) ((LinearEquiv.symm (LinearEquiv.ofInjective i hi) : (a : ↥i.range) → F) ix : F) : E) :
      F)
    ((LinearEquiv.symm (LinearEquiv.ofInjective i hi) : (a : ↥i.range) → F) ix : F)

Tactic:
simp [linearProjOfIsCompl]

Premises used: LinearMap.linearProjOfIsCompl
-- 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
q : Submodule R E
F : Type u_7
inst_3 : AddCommGroup F
inst_4 : Module R F
i : F →ₗ[R] E
hi : Function.Injective.{u_7 + 1, u_2 + 1} (α := F) (β := E) (⇑i : (a : F) → E)
h : IsCompl i.range q
x : E
hx : x ∈ q
⊢ Eq.{u_7 + 1} (α := F) ((linearProjOfIsCompl q i hi h : (a : E) → F) x : F) (0 : F)

Tactic:
simpa [LinearMap.linearProjOfIsCompl]

Premises used: LinearMap.linearProjOfIsCompl
-- 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
q : Submodule R E
F : Type u_7
inst_3 : AddCommGroup F
inst_4 : Module R F
i : F →ₗ[R] E
hi : Function.Injective.{u_7 + 1, u_2 + 1} (α := F) (β := E) (⇑i : (a : F) → E)
h : IsCompl i.range q
x : ↥q
⊢ Eq.{u_7 + 1} (α := F) ((linearProjOfIsCompl q i hi h : (a : E) → F) (↑x : E) : F) (0 : F)

Tactic:
simp [LinearMap.linearProjOfIsCompl]

Premises used: LinearMap.linearProjOfIsCompl
-- 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
q : Submodule R E
F : Type u_7
inst_3 : AddCommGroup F
inst_4 : Module R F
i : F →ₗ[R] E
hi : Function.Injective.{u_7 + 1, u_2 + 1} (α := F) (β := E) (⇑i : (a : F) → E)
h : IsCompl i.range q
⊢ (linearProjOfIsCompl q i hi h).ker = q

Tactic:
simp [LinearMap.linearProjOfIsCompl]

Premises used: LinearMap.linearProjOfIsCompl
-- 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) ((ofIsCompl h φ ψ : (a : E) → F) (↑u : E) : F) ((φ : (a : ↥p) → F) u : F)

Tactic:
simp [ofIsCompl]

Premises used: LinearMap.ofIsCompl
-- 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
v : ↥q
⊢ Eq.{u_3 + 1} (α := F) ((ofIsCompl h φ ψ : (a : E) → F) (↑v : E) : F) ((ψ : (a : ↥q) → F) v : F)

Tactic:
simp [ofIsCompl]

Premises used: LinearMap.ofIsCompl
-- 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
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), Eq.{u_3 + 1} (α := F) ((φ : (a : ↥p) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
hψ : ∀ (u : ↥q), Eq.{u_3 + 1} (α := F) ((ψ : (a : ↥q) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((ofIsCompl h φ ψ : (a : E) → F) x : F) ((χ : (a : E) → F) x : F)
⊢ ofIsCompl 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
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
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), Eq.{u_3 + 1} (α := F) ((φ : (a : ↥p) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
hψ : ∀ (u : ↥q), Eq.{u_3 + 1} (α := F) ((ψ : (a : ↥q) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
x : E
h₁ :
  ∀ (w : ↥p) (w_1 : ↥q),
    (∀ (r : ↥p) (s : ↥q), (↑r : E) + (↑s : E) = (↑w : E) + (↑w_1 : E) → r = w ∧ s = w_1) →
      Eq.{u_3 + 1} (α := F) ((ofIsCompl h φ ψ : (a : E) → F) ((↑w : E) + (↑w_1 : E)) : F)
        ((χ : (a : E) → F) ((↑w : E) + (↑w_1 : E)) : F)
⊢ Eq.{u_3 + 1} (α := F) ((ofIsCompl h φ ψ : (a : E) → F) x : F) ((χ : (a : E) → F) x : F)

Tactic:
obtain ⟨_, _, rfl, _⟩ := existsUnique_add_of_isCompl h x

Premises used: Submodule.existsUnique_add_of_isCompl, 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
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
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), Eq.{u_3 + 1} (α := F) ((φ : (a : ↥p) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
hψ : ∀ (u : ↥q), Eq.{u_3 + 1} (α := F) ((ψ : (a : ↥q) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
w : ↥p
w_1 : ↥q
right : ∀ (r : ↥p) (s : ↥q), (↑r : E) + (↑s : E) = (↑w : E) + (↑w_1 : E) → r = w ∧ s = w_1
⊢ Eq.{u_3 + 1} (α := F) ((ofIsCompl h φ ψ : (a : E) → F) ((↑w : E) + (↑w_1 : E)) : F)
    ((χ : (a : E) → F) ((↑w : E) + (↑w_1 : E)) : F)

Tactic:
simp [ofIsCompl, hφ, hψ]

Premises used: LinearMap.ofIsCompl
-- 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
χ : E →ₗ[R] F
hφ : φ = χ ∘ₗ p.subtype
hψ : ψ = χ ∘ₗ q.subtype
⊢ ofIsCompl h φ ψ = χ

Tactic:
ofIsCompl_eq h (fun _ => hφ.symm ▸ rfl) fun _ => hψ.symm ▸ rfl

Premises used: Eq.rec, LinearMap.ofIsCompl_eq, Eq.symm, 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
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
h :
  ∀ (x : E),
    Eq.{u_3 + 1} (α := F) ((ofIsCompl hpq φ ψ : (a : E) → F) x : F)
      ((φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯ : (a : E) → F) x : F)
⊢ ofIsCompl hpq φ ψ = φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯

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
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 : E
h :
  ∀ (a : ↥p) (b : ↥q),
    (∀ (r : ↥p) (s : ↥q), (↑r : E) + (↑s : E) = (↑a : E) + (↑b : E) → r = a ∧ s = b) →
      Eq.{u_3 + 1} (α := F) ((ofIsCompl hpq φ ψ : (a : E) → F) ((↑a : E) + (↑b : E)) : F)
        ((φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯ : (a : E) → F) ((↑a : E) + (↑b : E)) : F)
⊢ Eq.{u_3 + 1} (α := F) ((ofIsCompl hpq φ ψ : (a : E) → F) x : F)
    ((φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯ : (a : E) → F) x : F)

Tactic:
obtain ⟨a, b, rfl, _⟩ := existsUnique_add_of_isCompl hpq x

Premises used: Submodule.existsUnique_add_of_isCompl, 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
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
b : ↥q
right : ∀ (r : ↥p) (s : ↥q), (↑r : E) + (↑s : E) = (↑a : E) + (↑b : E) → r = a ∧ s = b
⊢ Eq.{u_3 + 1} (α := F) ((ofIsCompl hpq φ ψ : (a : E) → F) ((↑a : E) + (↑b : E)) : F)
    ((φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯ : (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
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
p q : Submodule R E
h : IsCompl p q
⊢ Eq (α := E →ₗ[R] F) (ofIsCompl h 0 0) 0

Tactic:
ofIsCompl_eq _ (fun _ => rfl) fun _ => rfl

Premises used: LinearMap.ofIsCompl_eq, rfl