awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 : M) = (↑(P ⊓ P) : M)

Tactic:
simpa only [coe_inf, ← sq] using P.prop.proj.eq.symm

Premises used: sq, Subtype.prop, IsLprojection.proj, IsIdempotentElem.eq, Eq.symm, IsLprojection.coe_inf
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 ⊓ Q) : M)
h₂ : (↑Q : M) = (↑(Q ⊓ R) : M)
simp : (↑P : M) = (↑P : M) * (↑R : M)
⊢ (↑P : M) = (↑(P ⊓ R) : M)

Tactic:
simp only [coe_inf] at h₁ h₂ ⊢

Premises used: IsLprojection.coe_inf
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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₂ : (↑Q : M) = (↑Q : M) * (↑R : M)
rw : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑R : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑Q : M) * (↑R : M))
rw₂ rw₃ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M)
⊢ (↑P : M) = (↑P : M) * (↑R : M)

Tactic:
rw [h₁, mul_assoc, ← h₂]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 }
h₁ : (↑P : M) = (↑(P ⊓ Q) : M)
h₂ : (↑Q : M) = (↑(Q ⊓ P) : M)
⊢ (↑P : M) * (↑Q : M) = (↑Q : M) * (↑P : M)

Tactic:
(P.prop.commute Q.prop).eq

Premises used: IsLprojection.commute, Subtype.prop, Commute.eq
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 }
h₁ : (↑P : M) = (↑(P ⊓ Q) : M)
h₂ : (↑Q : M) = (↑(Q ⊓ P) : M)
⊢ (↑P : M) = (↑Q : M)

Tactic:
convert! (P.prop.commute Q.prop).eq

Premises used: IsLprojection.commute, Subtype.prop, Commute.eq
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 : M) = (↑(P ⊓ Q) : M)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Normed.Module.MStructure
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
rw : HMul.hMul (α := M) 0 0 = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) 0 0
⊢ IsIdempotentElem.{u_2} (M := M) 0

Tactic:
rw [IsIdempotentElem, zero_mul]

Premises used: MulZeroClass.zero_mul, IsIdempotentElem
-- Module: Mathlib.Analysis.Normed.Module.MStructure
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
x : X
⊢ ‖x‖ = ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 0 x‖ + ‖HSub.hSub (α := M) 1 0 • x‖

Tactic:
simp only [zero_smul, norm_zero, sub_zero, one_smul, zero_add]

Premises used: sub_zero, norm_zero, zero_add, one_smul, zero_smul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
⊢ Eq.{u_2 + 1} (α := M) (↑0 : M) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.MStructure
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
⊢ Eq.{u_2 + 1} (α := M) (↑1 : M) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
⊢ Eq.{u_2 + 1} (α := M) (↑⊥ : M) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
⊢ Eq.{u_2 + 1} (α := M) (↑⊤ : M) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.MStructure
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
P : { P : M // IsLprojection X P }
Q : M
rw : (1 - (↑P : M)) * Q = Q - (↑P : M) * Q
rw₁ : 1 * Q - (↑P : M) * Q = Q - (↑P : M) * Q
rw₂ rw₃ : Q - (↑P : M) * Q = Q - (↑P : M) * Q
⊢ (↑Pᶜ : M) * Q = Q - (↑P : M) * Q

Tactic:
rw [coe_compl, sub_mul, one_mul]

Premises used: IsLprojection.coe_compl, sub_mul, one_mul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
P : { P : M // IsLprojection X P }
rw : (↑P : M) * (1 - (↑P : M)) = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) 0 0
⊢ (↑P : M) * (↑Pᶜ : M) = 0

Tactic:
rw [coe_compl, P.prop.proj.mul_one_sub_self]

Premises used: IsLprojection.coe_compl, IsIdempotentElem.mul_one_sub_self, Subtype.prop, IsLprojection.proj
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
rw₉ rw₁₀ : (↑P : M) = (↑P : M)
⊢ P ≤ P ⊔ Q

Tactic:
rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]

Premises used: mul_sub, sub_self, add_sub, mul_assoc, Subtype.prop, IsLprojection.proj, mul_add, IsIdempotentElem.eq, add_zero, IsLprojection.coe_sup, IsLprojection.coe_inf, IsLprojection.le_def
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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))
rw₉ rw₁₀ : (↑Q : M) = (↑Q : M)
⊢ Q ≤ P ⊔ Q

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]

Premises used: mul_sub, add_sub, mul_assoc, IsLprojection.commute, add_sub_cancel, Subtype.prop, IsLprojection.proj, mul_add, IsIdempotentElem.eq, IsLprojection.coe_sup, IsLprojection.coe_inf, Commute.eq, IsLprojection.le_def
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 }
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)))
⊢ P ≤ R → Q ≤ R → P ⊔ Q ≤ R

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]

Premises used: add_mul, add_sub, mul_assoc, sub_mul, IsLprojection.coe_sup, IsLprojection.coe_inf, IsLprojection.le_def
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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))
rw₁ rw₂ : (↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)) = (↑P : 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)))

Tactic:
rw [← h₂, ← h₁]
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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)
rw₇ rw₈ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M)
⊢ P ⊓ Q ≤ P

Tactic:
rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]

Premises used: mul_assoc, IsLprojection.commute, Subtype.prop, IsLprojection.proj, IsIdempotentElem.eq, IsLprojection.coe_inf, Commute.eq, IsLprojection.le_def
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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))
rw₅ rw₆ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M)
⊢ P ⊓ Q ≤ Q

Tactic:
rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]

Premises used: mul_assoc, Subtype.prop, IsLprojection.proj, IsIdempotentElem.eq, IsLprojection.coe_inf, IsLprojection.le_def
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 }
rw : (↑P : M) = (↑P : M) * (↑Q : M) → (↑P : M) = (↑P : M) * (↑R : M) → (↑P : M) = (↑P : M) * (↑Q : M) * (↑R : M)
⊢ P ≤ Q → P ≤ R → P ≤ Q ⊓ R

Tactic:
rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_inf, coe_inf, ← mul_assoc]

Premises used: mul_assoc, IsLprojection.coe_inf, IsLprojection.le_def
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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)
rw₁ rw₂ : (↑P : M) = (↑P : M)
⊢ (↑P : M) = (↑P : M) * (↑Q : M) * (↑R : M)

Tactic:
rw [← h₁, ← h₂]
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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)

Tactic:
have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑Pᶜ := by
      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]
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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)) : 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]
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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)
rw₃ rw₄ : (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R

Tactic:
rw [le_def, e₁, coe_inf, e₂]

Premises used: IsLprojection.coe_inf, IsLprojection.le_def
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
rw₄ rw₅ : Eq.{u_2 + 1} (α := M) 0 0
⊢ (↑(P ⊓ Pᶜ) : M) = (↑⊥ : M)

Tactic:
rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self]

Premises used: IsLprojection.coe_compl, IsLprojection.coe_bot, IsLprojection.mul_compl_self, IsLprojection.coe_inf
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
rw₆ rw₇ : Eq.{u_2 + 1} (α := M) 1 1
⊢ (↑⊤ : M) = (↑(P ⊔ Pᶜ) : M)

Tactic:
rw [coe_top, coe_sup, coe_compl, add_sub_cancel, ← coe_compl, mul_compl_self,
            sub_zero]

Premises used: sub_zero, IsLprojection.coe_compl, IsLprojection.coe_top, add_sub_cancel, IsLprojection.mul_compl_self, IsLprojection.coe_sup
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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)
rw₂ rw₃ : (↑P : M) * (↑Qᶜ : M) = (↑P : M) * (↑Qᶜ : M)
⊢ (↑(P \ Q) : M) = (↑(P ⊓ Qᶜ) : M)

Tactic:
rw [coe_sdiff, ← coe_compl, coe_inf]

Premises used: IsLprojection.coe_compl, IsLprojection.coe_sdiff, IsLprojection.coe_inf
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
intro :
  ∀ (val : Fintype ι),
    Continuous[instTopologicalSpaceProd, inst_4] fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (fx.1 : (a : (i : ι) → E i) → F) fx.2
⊢ 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 ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
⊢ IsUniformAddGroup F

Tactic:
have := isUniformAddGroup_of_addCommGroup (G := F)
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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

Tactic:
(UniformOnFun.continuousOn_eval₂ fun m ↦ ?_).comp_continuous
      (isEmbedding_toUniformOnFun.continuous.prodMap continuous_id) fun (f, x) ↦ f.cont.continuousAt

Premises used: Bornology.IsVonNBounded, Continuous.prodMap, ContinuousAt, ContinuousOn.comp_continuous, setOf, ContinuousMultilinearMap.toUniformOnFun, Membership.mem, id, Prod.map, UniformOnFun.toFun, Prod.fst, UniformOnFun.continuousOn_eval₂, Continuous.continuousAt, ContinuousMultilinearMap.isEmbedding_toUniformOnFun, continuous_id, ContinuousMultilinearMap.cont, UniformOnFun, _private.0.ContinuousMultilinearMap.instContinuousEval.match_1, Prod.snd, DFunLike.coe, Topology.IsEmbedding.continuous
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
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
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
    (fx.1 : (a : (i : ι) → E i) → F) fx.2

Tactic:
refine (UniformOnFun.continuousOn_eval₂ fun m ↦ ?_).comp_continuous
      (isEmbedding_toUniformOnFun.continuous.prodMap continuous_id) fun (f, x) ↦ f.cont.continuousAt

Premises used: Continuous.prodMap, ContinuousOn.comp_continuous, UniformOnFun.continuousOn_eval₂, ContinuousMultilinearMap.isEmbedding_toUniformOnFun, continuous_id, Topology.IsEmbedding.continuous
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
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:
⟨ball m 1, NormedSpace.isVonNBounded_of_isBounded _ isBounded_ball,
      ball_mem_nhds _ one_pos⟩

Premises used: Metric.isBounded_ball, Metric.ball, NormedSpace.isVonNBounded_of_isBounded, Metric.ball_mem_nhds, And.intro, Exists.intro, OfNat.ofNat, one_pos
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
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:
exact ⟨ball m 1, NormedSpace.isVonNBounded_of_isBounded _ isBounded_ball,
      ball_mem_nhds _ one_pos⟩
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : TopologicalSpace G
inst_10 : Module 𝕜 G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (p : G × ((i : ι) → E i)) ↦
    (((f : (a : G) → ContinuousMultilinearMap 𝕜 E F) p.1 : ContinuousMultilinearMap 𝕜 E F) : (a : (i : ι) → E i) → F)
      p.2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : TopologicalSpace G
inst_10 : Module 𝕜 G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
s : Set (G × ((i : ι) → E i))
⊢ ContinuousOn (Y := F)
    (fun (p : G × ((i : ι) → E i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 E F) p.1 : ContinuousMultilinearMap 𝕜 E F) : (a : (i : ι) → E i) → F)
        p.2)
    s

Tactic:
f.continuous_uncurry_of_multilinear.continuousOn

Premises used: Continuous.continuousOn, ContinuousLinearMap.continuous_uncurry_of_multilinear
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : TopologicalSpace G
inst_10 : Module 𝕜 G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
x : G × ((i : ι) → E i)
⊢ ContinuousAt (Y := F)
    (fun (p : G × ((i : ι) → E i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 E F) p.1 : ContinuousMultilinearMap 𝕜 E F) : (a : (i : ι) → E i) → F)
        p.2)
    x

Tactic:
f.continuous_uncurry_of_multilinear.continuousAt

Premises used: Continuous.continuousAt, ContinuousLinearMap.continuous_uncurry_of_multilinear