awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
rw₁ : (↑P : M) = (↑P : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑P : M) = (↑P : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑P : M) = (↑P : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑P : M) = (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
⊢ P ≤ P ⊔ Q
have rw₅ : (↑P : M) = (↑P : M) * (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * ((↑P : M) * (↑Q : M)))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
rw₁ : (↑P : M) = (↑P : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑P : M) = (↑P : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑P : M) = (↑P : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑P : M) = (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
rw₅ : (↑P : M) = (↑P : M) * (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * ((↑P : M) * (↑Q : M)))
⊢ P ≤ P ⊔ Q
have rw₆ : (↑P : M) = (↑P : M) * (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * (↑P : M) * (↑Q : M))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
rw₁ : (↑P : M) = (↑P : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑P : M) = (↑P : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑P : M) = (↑P : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑P : M) = (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
rw₅ : (↑P : M) = (↑P : M) * (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * ((↑P : M) * (↑Q : M)))
rw₆ : (↑P : M) = (↑P : M) * (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * (↑P : M) * (↑Q : M))
⊢ P ≤ P ⊔ Q
have rw₇ : (↑P : M) = (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * (↑Q : M))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
rw₁ : (↑P : M) = (↑P : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑P : M) = (↑P : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑P : M) = (↑P : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑P : M) = (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
rw₅ : (↑P : M) = (↑P : M) * (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * ((↑P : M) * (↑Q : M)))
rw₆ : (↑P : M) = (↑P : M) * (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * (↑P : M) * (↑Q : M))
rw₇ : (↑P : M) = (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * (↑Q : M))
⊢ P ≤ P ⊔ Q
have rw₈ : (↑P : M) = (↑P : M) + 0
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
rw₁ : (↑P : M) = (↑P : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑P : M) = (↑P : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑P : M) = (↑P : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑P : M) = (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
rw₅ : (↑P : M) = (↑P : M) * (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * ((↑P : M) * (↑Q : M)))
rw₆ : (↑P : M) = (↑P : M) * (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * (↑P : M) * (↑Q : M))
rw₇ : (↑P : M) = (↑P : M) + ((↑P : M) * (↑Q : M) - (↑P : M) * (↑Q : M))
rw₈ : (↑P : M) = (↑P : M) + 0
⊢ P ≤ P ⊔ Q
have rw₉ : (↑P : M) = (↑P : M)
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
⊢ Q ≤ P ⊔ Q
have rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
⊢ Q ≤ P ⊔ Q
have rw₁ : (↑Q : M) = (↑Q : M) * (↑(P ⊔ Q) : M)
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
rw₁ : (↑Q : M) = (↑Q : M) * (↑(P ⊔ Q) : M)
⊢ Q ≤ P ⊔ Q
have rw₂ : (↑Q : M) = (↑Q : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
rw₁ : (↑Q : M) = (↑Q : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑Q : M) = (↑Q : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
⊢ Q ≤ P ⊔ Q
have rw₃ : (↑Q : M) = (↑Q : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
rw₁ : (↑Q : M) = (↑Q : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑Q : M) = (↑Q : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑Q : M) = (↑Q : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
⊢ Q ≤ P ⊔ Q
have rw₄ : (↑Q : M) = (↑Q : M) * (↑P : M) + (↑Q : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
rw₁ : (↑Q : M) = (↑Q : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑Q : M) = (↑Q : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑Q : M) = (↑Q : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑Q : M) = (↑Q : M) * (↑P : M) + (↑Q : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
⊢ Q ≤ P ⊔ Q
have rw₅ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * ((↑P : M) * (↑Q : M)))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
rw₁ : (↑Q : M) = (↑Q : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑Q : M) = (↑Q : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑Q : M) = (↑Q : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑Q : M) = (↑Q : M) * (↑P : M) + (↑Q : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
rw₅ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * ((↑P : M) * (↑Q : M)))
⊢ Q ≤ P ⊔ Q
have rw₆ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * ((↑Q : M) * (↑P : M)))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
rw₁ : (↑Q : M) = (↑Q : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑Q : M) = (↑Q : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑Q : M) = (↑Q : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑Q : M) = (↑Q : M) * (↑P : M) + (↑Q : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
rw₅ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * ((↑P : M) * (↑Q : M)))
rw₆ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * ((↑Q : M) * (↑P : M)))
⊢ Q ≤ P ⊔ Q
have rw₇ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * (↑Q : M) * (↑P : M))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
rw₁ : (↑Q : M) = (↑Q : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑Q : M) = (↑Q : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑Q : M) = (↑Q : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑Q : M) = (↑Q : M) * (↑P : M) + (↑Q : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
rw₅ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * ((↑P : M) * (↑Q : M)))
rw₆ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * ((↑Q : M) * (↑P : M)))
rw₇ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * (↑Q : M) * (↑P : M))
⊢ Q ≤ P ⊔ Q
have rw₈ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) - (↑Q : M) * (↑P : M))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑Q : M) = (↑(Q ⊓ (P ⊔ Q)) : M)
rw₁ : (↑Q : M) = (↑Q : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑Q : M) = (↑Q : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑Q : M) = (↑Q : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
rw₄ : (↑Q : M) = (↑Q : M) * (↑P : M) + (↑Q : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
rw₅ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * ((↑P : M) * (↑Q : M)))
rw₆ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * ((↑Q : M) * (↑P : M)))
rw₇ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) * (↑Q : M) - (↑Q : M) * (↑Q : M) * (↑P : M))
rw₈ : (↑Q : M) = (↑Q : M) * (↑P : M) + ((↑Q : M) - (↑Q : M) * (↑P : M))
⊢ Q ≤ P ⊔ Q
have rw₉ : (↑Q : M) = (↑Q : M)
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
      ← mul_assoc, Q.prop.proj.eq, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q R : { P : M // IsLprojection X P }
⊢ P ≤ R → Q ≤ R → P ⊔ Q ≤ R
have rw : (↑P : M) = (↑P : M) * (↑R : M) →
  (↑Q : M) = (↑Q : M) * (↑R : M) →
    (↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)) =
      (↑P : M) * (↑R : M) + ((↑Q : M) * (↑R : M) - (↑P : M) * ((↑Q : M) * (↑R : M)))
Tactic: rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_sup, coe_inf, coe_sup, ← add_sub, add_mul,
      sub_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q R : { P : M // IsLprojection X P }
h₁ : (↑P : M) = (↑P : M) * (↑R : M)
h₂ : (↑Q : M) = (↑Q : M) * (↑R : M)
⊢ (↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)) =
    (↑P : M) * (↑R : M) + ((↑Q : M) * (↑R : M) - (↑P : M) * ((↑Q : M) * (↑R : M)))
have rw : (↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)) = (↑P : M) * (↑R : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))
Tactic: rw [← h₂, ← h₁]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q R : { P : M // IsLprojection X P }
h₁ : (↑P : M) = (↑P : M) * (↑R : M)
h₂ : (↑Q : M) = (↑Q : M) * (↑R : M)
rw : (↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)) = (↑P : M) * (↑R : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))
⊢ (↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)) =
    (↑P : M) * (↑R : M) + ((↑Q : M) * (↑R : M) - (↑P : M) * ((↑Q : M) * (↑R : M)))
have rw₁ : (↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)) = (↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))
Tactic: rw [← h₂, ← h₁]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
⊢ P ⊓ Q ≤ P
have rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ P) : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ P) : M)
⊢ P ⊓ Q ≤ P
have rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ P) : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ P) : M)
⊢ P ⊓ Q ≤ P
have rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑P : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑P : M)
⊢ P ⊓ Q ≤ P
have rw₃ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑P : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑P : M)
rw₃ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑P : M)
⊢ P ⊓ Q ≤ P
have rw₄ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑Q : M) * (↑P : M))
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑P : M)
rw₃ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑P : M)
rw₄ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑Q : M) * (↑P : M))
⊢ P ⊓ Q ≤ P
have rw₅ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑P : M) * (↑Q : M))
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑P : M)
rw₃ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑P : M)
rw₄ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑Q : M) * (↑P : M))
rw₅ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑P : M) * (↑Q : M))
⊢ P ⊓ Q ≤ P
have rw₆ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑P : M) * (↑Q : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ P) : M)
rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑P : M)
rw₃ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑P : M)
rw₄ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑Q : M) * (↑P : M))
rw₅ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑P : M) * (↑Q : M))
rw₆ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑P : M) * (↑Q : M)
⊢ P ⊓ Q ≤ P
have rw₇ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
⊢ P ⊓ Q ≤ Q
have rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ Q) : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ Q) : M)
⊢ P ⊓ Q ≤ Q
have rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ Q) : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ Q) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ Q) : M)
⊢ P ⊓ Q ≤ Q
have rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑Q : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ Q) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ Q) : M)
rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑Q : M)
⊢ P ⊓ Q ≤ Q
have rw₃ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑Q : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ Q) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ Q) : M)
rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑Q : M)
rw₃ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑Q : M)
⊢ P ⊓ Q ≤ Q
have rw₄ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑Q : M) * (↑Q : M))
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : { P : M // IsLprojection X P }
rw : (↑(P ⊓ Q) : M) = (↑(P ⊓ Q ⊓ Q) : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q ⊓ Q) : M)
rw₂ : (↑P : M) * (↑Q : M) = (↑(P ⊓ Q) : M) * (↑Q : M)
rw₃ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑Q : M)
rw₄ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑Q : M) * (↑Q : M))
⊢ P ⊓ Q ≤ Q
have rw₅ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M)
Tactic: rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q R : { P : M // IsLprojection X P }
⊢ P ≤ Q → P ≤ R → P ≤ Q ⊓ R
have rw : (↑P : M) = (↑P : M) * (↑Q : M) → (↑P : M) = (↑P : M) * (↑R : M) → (↑P : M) = (↑P : M) * (↑Q : M) * (↑R : M)
Tactic: rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_inf, coe_inf, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q R : { P : M // IsLprojection X P }
h₁ : (↑P : M) = (↑P : M) * (↑Q : M)
h₂ : (↑P : M) = (↑P : M) * (↑R : M)
rw : (↑P : M) = (↑P : M) * (↑R : M)
⊢ (↑P : M) = (↑P : M) * (↑Q : M) * (↑R : M)
have rw₁ : (↑P : M) = (↑P : M)
Tactic: rw [← h₁, ← h₂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q R : { P : M // IsLprojection X P }
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw : (↑(P ⊔ Q) : M) * (↑(P ⊔ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
Tactic: rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul,
        mul_add, (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M),
        (Pᶜ.prop.commute P.prop).eq, mul_compl_self, zero_mul, mul_zero,
        zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq,
        mul_assoc, (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]