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 R : { P : M // IsLprojection X P }
e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw : (↑(P ⊔ Q) : M) * (↑(P ⊔ R) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * (↑(P ⊔ R) : M) * (↑(P ⊔ Q ⊓ R) : M) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₂ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) * (↑(P ⊔ Q ⊓ R) : M) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₃ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₄ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₅ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₆ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₇ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₈ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₉ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₀ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑(Q ⊓ R) : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw₁₁ : ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)) =
  (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
Tactic: rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ←
        compl_mul, ← compl_mul, (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc,
        distrib_lattice_lemma, (Q.prop.commute R.prop).eq, distrib_lattice_lemma]
-- 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 }
e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw : (↑(P ⊔ Q) : M) * (↑(P ⊔ R) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * (↑(P ⊔ R) : M) * (↑(P ⊔ Q ⊓ R) : M) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₂ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) * (↑(P ⊔ Q ⊓ R) : M) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₃ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₄ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₅ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₆ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₇ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₈ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₉ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₀ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑(Q ⊓ R) : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₁ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw₁₂ : ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * (((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M))) =
  (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
Tactic: rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ←
        compl_mul, ← compl_mul, (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc,
        distrib_lattice_lemma, (Q.prop.commute R.prop).eq, distrib_lattice_lemma]
-- 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 }
e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw : (↑(P ⊔ Q) : M) * (↑(P ⊔ R) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * (↑(P ⊔ R) : M) * (↑(P ⊔ Q ⊓ R) : M) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₂ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) * (↑(P ⊔ Q ⊓ R) : M) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₃ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₄ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₅ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₆ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₇ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₈ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₉ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₀ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑(Q ⊓ R) : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₁ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₂ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) *
      (((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw₁₃ : ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)) =
  (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
Tactic: rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ←
        compl_mul, ← compl_mul, (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc,
        distrib_lattice_lemma, (Q.prop.commute R.prop).eq, distrib_lattice_lemma]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (hypothesis)
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 }
e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
have e₂ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
Tactic: have e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = (P : M) + ↑Q * ↑R * ↑Pᶜ := by
      rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ←
        compl_mul, ← compl_mul, (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc,
        distrib_lattice_lemma, (Q.prop.commute R.prop).eq, distrib_lattice_lemma]
-- 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 }
e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
e₂ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
have rw : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑((P ⊔ Q) ⊓ (P ⊔ R) ⊓ (P ⊔ Q ⊓ R)) : M)
Tactic: rw [le_def, e₁, coe_inf, e₂]
-- 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 }
e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
e₂ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑((P ⊔ Q) ⊓ (P ⊔ R) ⊓ (P ⊔ Q ⊓ R)) : M)
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
have rw₁ : (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M) = (↑((P ⊔ Q) ⊓ (P ⊔ R) ⊓ (P ⊔ Q ⊓ R)) : M)
Tactic: rw [le_def, e₁, coe_inf, e₂]
-- 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 }
e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
e₂ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑((P ⊔ Q) ⊓ (P ⊔ R) ⊓ (P ⊔ Q ⊓ R)) : M)
rw₁ : (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M) = (↑((P ⊔ Q) ⊓ (P ⊔ R) ⊓ (P ⊔ Q ⊓ R)) : M)
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
have rw₂ : (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M) = (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M)
Tactic: rw [le_def, e₁, coe_inf, e₂]
-- 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 }
e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
e₂ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑((P ⊔ Q) ⊓ (P ⊔ R) ⊓ (P ⊔ Q ⊓ R)) : M)
rw₁ : (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M) = (↑((P ⊔ Q) ⊓ (P ⊔ R) ⊓ (P ⊔ Q ⊓ R)) : M)
rw₂ : (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M) = (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M)
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
have rw₃ : (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
Tactic: rw [le_def, e₁, coe_inf, e₂]
-- 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 : { P : M // IsLprojection X P }
⊢ (↑(P ⊓ Pᶜ) : M) = (↑⊥ : M)
have rw : (↑P : M) * (↑Pᶜ : M) = (↑⊥ : M)
Tactic: rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self]
-- 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 : { P : M // IsLprojection X P }
rw : (↑P : M) * (↑Pᶜ : M) = (↑⊥ : M)
⊢ (↑(P ⊓ Pᶜ) : M) = (↑⊥ : M)
have rw₁ : (↑P : M) * (1 - (↑P : M)) = (↑⊥ : M)
Tactic: rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self]
-- 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 : { P : M // IsLprojection X P }
rw : (↑P : M) * (↑Pᶜ : M) = (↑⊥ : M)
rw₁ : (↑P : M) * (1 - (↑P : M)) = (↑⊥ : M)
⊢ (↑(P ⊓ Pᶜ) : M) = (↑⊥ : M)
have rw₂ : (↑P : M) * (1 - (↑P : M)) = 0
Tactic: rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self]
-- 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 : { P : M // IsLprojection X P }
rw : (↑P : M) * (↑Pᶜ : M) = (↑⊥ : M)
rw₁ : (↑P : M) * (1 - (↑P : M)) = (↑⊥ : M)
rw₂ : (↑P : M) * (1 - (↑P : M)) = 0
⊢ (↑(P ⊓ Pᶜ) : M) = (↑⊥ : M)
have rw₃ : (↑P : M) * (↑Pᶜ : M) = 0
Tactic: rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self]
-- 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 : { P : M // IsLprojection X P }
rw : (↑P : M) * (↑Pᶜ : M) = (↑⊥ : M)
rw₁ : (↑P : M) * (1 - (↑P : M)) = (↑⊥ : M)
rw₂ : (↑P : M) * (1 - (↑P : M)) = 0
rw₃ : (↑P : M) * (↑Pᶜ : M) = 0
⊢ (↑(P ⊓ Pᶜ) : M) = (↑⊥ : M)
have rw₄ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self]
-- 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 : { P : M // IsLprojection X P }
⊢ (↑⊤ : M) = (↑(P ⊔ Pᶜ) : M)
have rw : 1 = (↑(P ⊔ Pᶜ) : M)
Tactic: rw [coe_top, coe_sup, coe_compl, add_sub_cancel, ← coe_compl, mul_compl_self,
            sub_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 : { P : M // IsLprojection X P }
rw : 1 = (↑(P ⊔ Pᶜ) : M)
⊢ (↑⊤ : M) = (↑(P ⊔ Pᶜ) : M)
have rw₁ : 1 = (↑P : M) + (↑Pᶜ : M) - (↑P : M) * (↑Pᶜ : M)
Tactic: rw [coe_top, coe_sup, coe_compl, add_sub_cancel, ← coe_compl, mul_compl_self,
            sub_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 : { P : M // IsLprojection X P }
rw : 1 = (↑(P ⊔ Pᶜ) : M)
rw₁ : 1 = (↑P : M) + (↑Pᶜ : M) - (↑P : M) * (↑Pᶜ : M)
⊢ (↑⊤ : M) = (↑(P ⊔ Pᶜ) : M)
have rw₂ : 1 = (↑P : M) + (1 - (↑P : M)) - (↑P : M) * (1 - (↑P : M))
Tactic: rw [coe_top, coe_sup, coe_compl, add_sub_cancel, ← coe_compl, mul_compl_self,
            sub_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 : { P : M // IsLprojection X P }
rw : 1 = (↑(P ⊔ Pᶜ) : M)
rw₁ : 1 = (↑P : M) + (↑Pᶜ : M) - (↑P : M) * (↑Pᶜ : M)
rw₂ : 1 = (↑P : M) + (1 - (↑P : M)) - (↑P : M) * (1 - (↑P : M))
⊢ (↑⊤ : M) = (↑(P ⊔ Pᶜ) : M)
have rw₃ : 1 = 1 - (↑P : M) * (1 - (↑P : M))
Tactic: rw [coe_top, coe_sup, coe_compl, add_sub_cancel, ← coe_compl, mul_compl_self,
            sub_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 : { P : M // IsLprojection X P }
rw : 1 = (↑(P ⊔ Pᶜ) : M)
rw₁ : 1 = (↑P : M) + (↑Pᶜ : M) - (↑P : M) * (↑Pᶜ : M)
rw₂ : 1 = (↑P : M) + (1 - (↑P : M)) - (↑P : M) * (1 - (↑P : M))
rw₃ : 1 = 1 - (↑P : M) * (1 - (↑P : M))
⊢ (↑⊤ : M) = (↑(P ⊔ Pᶜ) : M)
have rw₄ : 1 = 1 - (↑P : M) * (↑Pᶜ : M)
Tactic: rw [coe_top, coe_sup, coe_compl, add_sub_cancel, ← coe_compl, mul_compl_self,
            sub_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 : { P : M // IsLprojection X P }
rw : 1 = (↑(P ⊔ Pᶜ) : M)
rw₁ : 1 = (↑P : M) + (↑Pᶜ : M) - (↑P : M) * (↑Pᶜ : M)
rw₂ : 1 = (↑P : M) + (1 - (↑P : M)) - (↑P : M) * (1 - (↑P : M))
rw₃ : 1 = 1 - (↑P : M) * (1 - (↑P : M))
rw₄ : 1 = 1 - (↑P : M) * (↑Pᶜ : M)
⊢ (↑⊤ : M) = (↑(P ⊔ Pᶜ) : M)
have rw₅ : 1 = HSub.hSub (α := M) 1 0
Tactic: rw [coe_top, coe_sup, coe_compl, add_sub_cancel, ← coe_compl, mul_compl_self,
            sub_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 : { P : M // IsLprojection X P }
rw : 1 = (↑(P ⊔ Pᶜ) : M)
rw₁ : 1 = (↑P : M) + (↑Pᶜ : M) - (↑P : M) * (↑Pᶜ : M)
rw₂ : 1 = (↑P : M) + (1 - (↑P : M)) - (↑P : M) * (1 - (↑P : M))
rw₃ : 1 = 1 - (↑P : M) * (1 - (↑P : M))
rw₄ : 1 = 1 - (↑P : M) * (↑Pᶜ : M)
rw₅ : 1 = HSub.hSub (α := M) 1 0
⊢ (↑⊤ : M) = (↑(P ⊔ Pᶜ) : M)
have rw₆ : Eq.{u_2 + 1} (α := M) 1 1
Tactic: rw [coe_top, coe_sup, coe_compl, add_sub_cancel, ← coe_compl, mul_compl_self,
            sub_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 }
⊢ (↑(P \ Q) : M) = (↑(P ⊓ Qᶜ) : M)
have rw : (↑P : M) * (1 - (↑Q : M)) = (↑(P ⊓ Qᶜ) : M)
Tactic: rw [coe_sdiff, ← coe_compl, coe_inf]
-- 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) * (1 - (↑Q : M)) = (↑(P ⊓ Qᶜ) : M)
⊢ (↑(P \ Q) : M) = (↑(P ⊓ Qᶜ) : M)
have rw₁ : (↑P : M) * (↑Qᶜ : M) = (↑(P ⊓ Qᶜ) : M)
Tactic: rw [coe_sdiff, ← coe_compl, coe_inf]
-- 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) * (1 - (↑Q : M)) = (↑(P ⊓ Qᶜ) : M)
rw₁ : (↑P : M) * (↑Qᶜ : M) = (↑(P ⊓ Qᶜ) : M)
⊢ (↑(P \ Q) : M) = (↑(P ⊓ Qᶜ) : M)
have rw₂ : (↑P : M) * (↑Qᶜ : M) = (↑P : M) * (↑Qᶜ : M)
Tactic: rw [coe_sdiff, ← coe_compl, coe_inf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : Finite ι
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : IsTopologicalAddGroup F
inst_7 : Module 𝕜 F
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
    (fx.1 : (a : (i : ι) → E i) → F) fx.2
have intro : ∀ (val : Fintype ι),
  Continuous[instTopologicalSpaceProd, inst_4] fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
    (fx.1 : (a : (i : ι) → E i) → F) fx.2
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : Finite ι
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : IsTopologicalAddGroup F
inst_7 : Module 𝕜 F
val : Fintype ι
x : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
    (fx.1 : (a : (i : ι) → E i) → F) fx.2
have this : IsUniformAddGroup F
Tactic: have := isUniformAddGroup_of_addCommGroup (G := F)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : Finite ι
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : IsTopologicalAddGroup F
inst_7 : Module 𝕜 F
val : Fintype ι
x : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
    (fx.1 : (a : (i : ι) → E i) → F) fx.2
have intro : ∀ (m : (i : ι) → E i),
  ∃ (V : Set ((i : ι) → E i)),
    Membership.mem (γ := Set (Set ((i : ι) → E i))) {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s} V ∧ V ∈ 𝓝 m
Tactic: refine (UniformOnFun.continuousOn_eval₂ fun m ↦ ?_).comp_continuous
      (isEmbedding_toUniformOnFun.continuous.prodMap continuous_id) fun (f, x) ↦ f.cont.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0
have rw : ∀ (hi : Inseparable (m i) 0), Inseparable.{wG} (X := G) ((f : (a : (i : ι) → E i) → G) m : G) (0 : G)
Tactic: rw [← inseparable_zero_iff_norm] at hi ⊢
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
m : (i : ι) → E i
i : ι
hi : Inseparable (m i) 0
⊢ Inseparable.{wG} (X := G) ((f : (a : (i : ι) → E i) → G) m : G) (0 : G)
have this : Inseparable (update (β := E) m i 0) m
Tactic: have : Inseparable (update m i 0) m := inseparable_pi.2 <|
    (forall_update_iff m fun i a ↦ Inseparable a (m i)).2 ⟨hi.symm, fun _ _ ↦ rfl⟩