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
p q : Submodule R E
h : IsCompl p q
x : E
⊢ Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔ x ∈ p
have conv_rhs : Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
  Membership.mem (α := E) p
    ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
        (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
      E)
Tactic: conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply 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 q : Submodule R E
h : IsCompl p q
x : E
⊢ Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    Membership.mem (α := E) p
      ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
          (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
        E)
have rw : Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
  HAdd.hAdd (α := E) (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 : E)
      (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 : E) ∈
    p
Tactic: rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
    mem_left_iff_eq_zero_of_disjoint h.disjoint]
-- 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 q : Submodule R E
h : IsCompl p q
x : E
rw :
  Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    HAdd.hAdd (α := E) (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 : E)
        (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 : E) ∈
      p
⊢ Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    Membership.mem (α := E) p
      ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
          (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
        E)
have rw₁ : Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
  (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 : E) ∈ p
Tactic: rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
    mem_left_iff_eq_zero_of_disjoint h.disjoint]
-- 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 q : Submodule R E
h : IsCompl p q
x : E
rw :
  Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    HAdd.hAdd (α := E) (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 : E)
        (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 : E) ∈
      p
rw₁ :
  Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 : E) ∈ p
⊢ Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    Membership.mem (α := E) p
      ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
          (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
        E)
have rw₂ : Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
  Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0
Tactic: rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
    mem_left_iff_eq_zero_of_disjoint h.disjoint]
-- 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 q : Submodule R E
hpq : IsCompl p q
x : E
⊢ HAdd.hAdd (α := E) (β := E) ((p.projection q hpq : (a : E) → E) x : E) ((q.projection p ⋯ : (a : E) → E) x : E) = x
have 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 sorry).symm : E →ₗ[R] ↥q × ↥p) : (a : E) → E) x : E) =
  x
Tactic: dsimp only [projection, projectionOnto]
-- 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 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 ∘ₗ (↑(q.prodEquivOfIsCompl p ⋯).symm : E →ₗ[R] ↥q × ↥p) : (a : E) → E) x :
        E) =
    x
have 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
Tactic: rw [← prodComm_trans_prodEquivOfIsCompl _ _ hpq]
-- 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 q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (q.projection p ⋯ : (a : E) → E) x = HSub.hSub (β := E) x ((p.projection q hpq : (a : E) → E) x : E)
have rw : HAdd.hAdd (α := E) (β := E) ((q.projection p sorry : (a : E) → E) x : E) ((p.projection q hpq : (a : E) → E) x : E) = x
Tactic: rw [eq_sub_iff_add_eq, projection_add_projection_eq_self]
-- 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 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
⊢ (q.projection p ⋯ : (a : E) → E) x = HSub.hSub (β := E) x ((p.projection q hpq : (a : E) → E) x : E)
have rw₁ : x = x
Tactic: rw [eq_sub_iff_add_eq, projection_add_projection_eq_self]
-- 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 q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (p.projection q hpq : (a : E) → E) x = x ↔ x ∈ p
have rw : x = (p.projection q hpq : (a : E) → E) x ↔ x ∈ p
Tactic: rw [eq_comm, ← sub_eq_zero, ← projection_eq_self_sub_projection, projection_apply_eq_zero_iff]
-- 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 q : Submodule R E
hpq : IsCompl p q
x : E
rw : x = (p.projection q hpq : (a : E) → E) x ↔ x ∈ p
⊢ (p.projection q hpq : (a : E) → E) x = x ↔ x ∈ p
have rw₁ : HSub.hSub (β := E) x ((p.projection q hpq : (a : E) → E) x : E) = 0 ↔ x ∈ p
Tactic: rw [eq_comm, ← sub_eq_zero, ← projection_eq_self_sub_projection, projection_apply_eq_zero_iff]
-- 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 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
⊢ (p.projection q hpq : (a : E) → E) x = x ↔ x ∈ p
have rw₂ : Eq (α := E) ((q.projection p sorry : (a : E) → E) x : E) (0 : E) ↔ x ∈ p
Tactic: rw [eq_comm, ← sub_eq_zero, ← projection_eq_self_sub_projection, projection_apply_eq_zero_iff]
-- 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 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
⊢ (p.projection q hpq : (a : E) → E) x = x ↔ x ∈ p
have rw₃ : x ∈ p ↔ x ∈ p
Tactic: rw [eq_comm, ← sub_eq_zero, ← projection_eq_self_sub_projection, projection_apply_eq_zero_iff]
-- 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 q : Submodule R E
h : IsCompl p q
x : E
⊢ HSub.hSub (β := E) x ((p.projection q h : (a : E) → E) x : E) ∈ q
have rw : Membership.mem (α := E) q ((q.projection p sorry : (a : E) → E) x : E)
Tactic: rw [← projection_eq_self_sub_projection 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
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.liftQ (q.projectionOnto p ⋯) ⋯ ∘ₗ p.mkQ ∘ₗ q.subtype = LinearMap.id
have h₁ : ∀ (x : ↥q),
  Eq.{u_2 + 1} (α := E) (↑((p.liftQ (q.projectionOnto p sorry) sorry ∘ₗ p.mkQ ∘ₗ q.subtype : (a : ↥q) → ↥q) x) : E)
    (↑((LinearMap.id : (a : ↥q) → ↥q) x) : E)
Tactic: ext
-- 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
h : IsCompl p q
⊢ (p.mkQ ∘ₗ q.subtype) ∘ₗ p.liftQ (q.projectionOnto p ⋯) ⋯ = LinearMap.id
have h₁ : ∀ (x : E),
  Eq (α := E ⧸ p) ((((p.mkQ ∘ₗ q.subtype) ∘ₗ p.liftQ (q.projectionOnto p sorry) sorry) ∘ₗ p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p)
    ((LinearMap.id ∘ₗ p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p)
Tactic: ext
-- 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
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
⊢ (linearProjOfIsCompl q i hi h : (a : E) → F) ((i : (a : F) → E) x : E) = x
have 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)
Tactic: obtain ⟨ix, rfl⟩ := (LinearEquiv.ofInjective i hi).symm.surjective x
Cleared hypotheses: 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
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)
⊢ ofIsCompl h φ ψ = χ
have h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((ofIsCompl h φ ψ : (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
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
⊢ Eq.{u_3 + 1} (α := F) ((ofIsCompl h φ ψ : (a : E) → F) x : F) ((χ : (a : E) → F) x : F)
have 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)
Tactic: obtain ⟨_, _, rfl, _⟩ := existsUnique_add_of_isCompl h x
Cleared hypotheses: 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
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 hpq φ ψ = φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯
have h : ∀ (x : E),
  Eq.{u_3 + 1} (α := F) ((ofIsCompl hpq φ ψ : (a : E) → F) x : F)
    ((φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p sorry : (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
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
⊢ Eq.{u_3 + 1} (α := F) ((ofIsCompl hpq φ ψ : (a : E) → F) x : F)
    ((φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯ : (a : E) → F) x : F)
have 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 sorry : (a : E) → F) ((↑a : E) + (↑b : E)) : F)
Tactic: obtain ⟨a, b, rfl, _⟩ := existsUnique_add_of_isCompl hpq x
Cleared hypotheses: 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 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
⊢ p.projectionOnto q h ∘ₗ p.subtype ∘ₗ f = f
have 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)
Tactic: ext
-- 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
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
⊢ (fun (f : E →ₗ[R] M) ↦ f ∘ₗ p.subtype) (f ∘ₗ p.projectionOnto q h) = f
have 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)
Tactic: ext
-- 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
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 hpq φ ψ).range = φ.range ⊔ ψ.range
have rw : (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p sorry).range = φ.range ⊔ ψ.range
Tactic: rw [ofIsCompl_eq_add]
-- 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
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 + ψ ∘ₗ q.projectionOnto p ⋯).range = φ.range ⊔ ψ.range
have a : (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p sorry).range ≤ φ.range ⊔ ψ.range
Tactic: apply le_antisymm
-- 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
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
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range = φ.range ⊔ ψ.range
have a₁ : φ.range ⊔ ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p sorry).range
Tactic: apply le_antisymm
-- 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
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 + ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range
have a : (φ ∘ₗ p.projectionOnto q hpq).range ⊔ (ψ ∘ₗ q.projectionOnto p sorry).range ≤ φ.range ⊔ ψ.range
Tactic: apply range_add_le _ _ |>.trans
-- 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
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 ⊔ (ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range
have a : (φ ∘ₗ p.projectionOnto q hpq).range ≤ φ.range
Tactic: gcongr
-- 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
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
⊢ (φ ∘ₗ p.projectionOnto q hpq).range ⊔ (ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range
have a₁ : (ψ ∘ₗ q.projectionOnto p sorry).range ≤ ψ.range
Tactic: gcongr
-- 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
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
⊢ φ.range ⊔ ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range
have a : φ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p sorry).range
Tactic: apply sup_le
-- 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
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
⊢ φ.range ⊔ ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range
have a₁ : ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p sorry).range
Tactic: apply sup_le
-- 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
⊢ ofIsCompl h (φ + ψ).1 (φ + ψ).2 = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
have rw : ofIsCompl h (φ + ψ).1 (φ.2 + ψ.2) = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
Tactic: rw [Prod.snd_add, Prod.fst_add, ofIsCompl_add]
-- 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
rw : ofIsCompl h (φ + ψ).1 (φ.2 + ψ.2) = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
⊢ ofIsCompl h (φ + ψ).1 (φ + ψ).2 = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
have rw₁ : ofIsCompl h (φ.1 + ψ.1) (φ.2 + ψ.2) = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
Tactic: rw [Prod.snd_add, Prod.fst_add, ofIsCompl_add]
-- 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
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
⊢ ofIsCompl h (φ + ψ).1 (φ + ψ).2 = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
have rw₂ : 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]
-- 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
⊢ (fun (φ : E →ₗ[R₁] F) ↦ (φ.domRestrict p, φ.domRestrict q)) (AddHom.toFun (toAddHom (ofIsComplProd h)) φ) = φ
have 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)
Tactic: ext x