awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
hx : IsStarNormal x
⊢ HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) =
    HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
        (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)

Tactic:
simp [Commute.realPart_imaginaryPart x |>.eq]

Premises used: Commute.realPart_imaginaryPart, Commute.eq
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : StarModule ℂ A
a : Eq.{u_1 + 1} (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) 1) : A) (↑1 : A)
⊢ Eq.{u_1 + 1} (α := ↥(selfAdjoint A)) (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) 1) 1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : StarModule ℂ A
⊢ Eq.{u_1 + 1} (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) 1) : A) (↑1 : A)

Tactic:
simp [realPart_apply_coe, ← two_smul ℝ]

Premises used: Real, two_smul, realPart_apply_coe
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : SMulCommClass ℂ A A
inst_4 : IsScalarTower ℂ A A
inst_5 : StarModule ℂ A
x : A
⊢ star x * x = 1 ∧ x * star x = 1 ↔
    IsStarNormal x ∧
      HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
        1

Tactic:
⟨fun ⟨h, h'⟩ ↦ ?_, fun ⟨hx, h⟩ ↦ ?_⟩

Premises used: HMul.hMul, IsStarNormal, imaginaryPart, And, HPow.hPow, HAdd.hAdd, _private.0.mem_unitary_iff_isStarNormal_and_realPart_sq_add_imaginaryPart_sq_eq_one.match_1, Iff.intro, realPart, OfNat.ofNat, Subtype.val, Eq, DFunLike.coe, _private.0.mem_unitary_iff_isStarNormal_and_realPart_sq_add_imaginaryPart_sq_eq_one.match_2, Star.star
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : SMulCommClass ℂ A A
inst_4 : IsScalarTower ℂ A A
inst_5 : StarModule ℂ A
x : A
refine_1 :
  star x * x = 1 ∧ x * star x = 1 →
    ∀ (h : star x * x = 1) (h' : x * star x = 1),
      IsStarNormal x ∧
        HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
            HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
          1
refine_2 :
  IsStarNormal x ∧
      HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
        1 →
    ∀ (hx : IsStarNormal x)
      (h :
        HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
            HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
          1),
      star x * x = 1 ∧ x * star x = 1
⊢ star x * x = 1 ∧ x * star x = 1 ↔
    IsStarNormal x ∧
      HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
        1

Tactic:
refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun ⟨hx, h⟩ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : SMulCommClass ℂ A A
inst_4 : IsScalarTower ℂ A A
inst_5 : StarModule ℂ A
x : A
h_1 : star x * x = 1 ∧ x * star x = 1
h : star x * x = 1
h' : x * star x = 1
⊢ IsStarNormal x

Tactic:
have : IsStarNormal x := ⟨h.trans h'.symm⟩
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : SMulCommClass ℂ A A
inst_4 : IsScalarTower ℂ A A
inst_5 : StarModule ℂ A
x : A
h_1 : star x * x = 1 ∧ x * star x = 1
h : star x * x = 1
h' : x * star x = 1
this : IsStarNormal x
⊢ HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
      HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
    1

Tactic:
simp [sq, ← star_mul_self_eq_realPart_sq_add_imaginaryPart_sq x, h]

Premises used: star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, sq
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : SMulCommClass ℂ A A
inst_4 : IsScalarTower ℂ A A
inst_5 : StarModule ℂ A
x : A
h_1 : star x * x = 1 ∧ x * star x = 1
h : star x * x = 1
h' : x * star x = 1
this : IsStarNormal x
⊢ IsStarNormal x ∧
    HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
      1

Tactic:
exact ⟨this, by simp [sq, ← star_mul_self_eq_realPart_sq_add_imaginaryPart_sq x, h]⟩
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : SMulCommClass ℂ A A
inst_4 : IsScalarTower ℂ A A
inst_5 : StarModule ℂ A
x : A
h_1 :
  IsStarNormal x ∧
    HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
      1
hx : IsStarNormal x
h :
  HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
      HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
    1
⊢ star x * x = 1 ∧ x * star x = 1

Tactic:
simp [← hx.star_comm_self.eq, star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, ← sq, h]

Premises used: IsStarNormal.star_comm_self, star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, sq, Commute.eq
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Dual R M
m : M
⊢ Eq.{u_2 + 1} (α := R) ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (f ⊗ₜ[R] m) : R) ((f : (a : M) → R) m : R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Dual R M
m : M
⊢ Eq.{u_2 + 1} (α := R) ((contractRight R M : (a : M ⊗[R] Dual R M) → R) (m ⊗ₜ[R] f) : R) ((f : (a : M) → R) m : R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : Dual R M
m : M
n : N
⊢ (((dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N) (f ⊗ₜ[R] n) : M →ₗ[R] N) : (a : M) → N) m =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : M) → R) m : R) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Dual R M
m : M
h :
  ∀ (f' : Dual R M) (m' : M),
    Eq.{u_2 + 1} (α := R)
      ((((((Dual.transpose : (a : M →ₗ[R] M) → Dual R M →ₗ[R] Dual R M)
                      ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (f ⊗ₜ[R] m)) :
                    Dual R M →ₗ[R] Dual R M) :
                  (a : Dual R M) → Dual R M)
                f' :
              Dual R M) :
            (a : M) → R)
          m' :
        R)
      ((((((dualTensorHom R (Dual R M) (Dual R M) : (a : Dual R (Dual R M) ⊗[R] Dual R M) → Dual R M →ₗ[R] Dual R M)
                      ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m ⊗ₜ[R] f) :
                    Dual R M →ₗ[R] Dual R M) :
                  (a : Dual R M) → Dual R M)
                f' :
              Dual R M) :
            (a : M) → R)
          m' :
        R)
⊢ Eq (α := Dual R M →ₗ[R] Dual R M)
    ((Dual.transpose : (a : M →ₗ[R] M) → Dual R M →ₗ[R] Dual R M)
        ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (f ⊗ₜ[R] m)) :
      Dual R M →ₗ[R] Dual R M)
    ((dualTensorHom R (Dual R M) (Dual R M) : (a : Dual R (Dual R M) ⊗[R] Dual R M) → Dual R M →ₗ[R] Dual R M)
        ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m ⊗ₜ[R] f) :
      Dual R M →ₗ[R] Dual R M)

Tactic:
ext f' m'
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Dual R M
m : M
f' : Dual R M
m' : M
h :
  HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m' : R) ((f' : (a : M) → R) m : R) =
    HMul.hMul (α := R) (β := R) ((f' : (a : M) → R) m : R) ((f : (a : M) → R) m' : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((((Dual.transpose : (a : M →ₗ[R] M) → Dual R M →ₗ[R] Dual R M)
                    ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (f ⊗ₜ[R] m)) :
                  Dual R M →ₗ[R] Dual R M) :
                (a : Dual R M) → Dual R M)
              f' :
            Dual R M) :
          (a : M) → R)
        m' :
      R)
    ((((((dualTensorHom R (Dual R M) (Dual R M) : (a : Dual R (Dual R M) ⊗[R] Dual R M) → Dual R M →ₗ[R] Dual R M)
                    ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m ⊗ₜ[R] f) :
                  Dual R M →ₗ[R] Dual R M) :
                (a : Dual R M) → Dual R M)
              f' :
            Dual R M) :
          (a : M) → R)
        m' :
      R)

Tactic:
simp only [Dual.transpose_apply, coe_comp, Function.comp_apply, dualTensorHom_apply,
    map_smulₛₗ, RingHom.id_apply, smul_eq_mul, Dual.eval_apply,
    LinearMap.smul_apply]

Premises used: RingHom.id_apply, LinearMap.smul_apply, dualTensorHom_apply, Module.Dual.eval_apply, Module.Dual.transpose_apply, MulActionSemiHomClass.map_smulₛₗ, LinearMap.coe_comp, Function.comp_apply, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Dual R M
m : M
f' : Dual R M
m' : M
⊢ HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m' : R) ((f' : (a : M) → R) m : R) =
    HMul.hMul (α := R) (β := R) ((f' : (a : M) → R) m : R) ((f : (a : M) → R) m' : R)

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Dual R M
m : M
f' : Dual R M
m' : M
⊢ HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m' : R) ((f' : (a : M) → R) m : R) =
    HMul.hMul (α := R) (β := R) ((f' : (a : M) → R) m : R) ((f : (a : M) → R) m' : R)

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
hl :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := P)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).1
hl₁ :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := Q)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).2
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).2
hr :
  ∀ (x : N),
    Eq.{u_5 + 1} (α := P)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inr R M N :
            (a : N) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inr R M N :
            (a : N) → P × Q)
          x).1
hr₁ :
  ∀ (x : N),
    Eq.{u_6 + 1} (α := Q)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inr R M N :
            (a : N) → P × Q)
          x).2
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inr R M N :
            (a : N) → P × Q)
          x).2
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0)
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
x : M
⊢ Eq.{u_5 + 1} (α := P)
    ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N : (a : M) → P × Q)
        x).1
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
            inl R M N :
          (a : M) → P × Q)
        x).1

Tactic:
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Premises used: LinearMap.zero_apply, LinearMap.prodMap_apply, dualTensorHom_apply, smul_zero, LinearMap.fst_apply, LinearMap.coe_inl, LinearMap.coe_comp, Function.comp_apply, Prod.smul_mk
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
x : M
⊢ Eq.{u_6 + 1} (α := Q)
    ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N : (a : M) → P × Q)
        x).2
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
            inl R M N :
          (a : M) → P × Q)
        x).2

Tactic:
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Premises used: LinearMap.zero_apply, LinearMap.prodMap_apply, dualTensorHom_apply, smul_zero, LinearMap.fst_apply, LinearMap.coe_inl, LinearMap.coe_comp, Function.comp_apply, Prod.smul_mk
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
x : N
⊢ Eq.{u_5 + 1} (α := P)
    ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inr R M N : (a : N) → P × Q)
        x).1
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
            inr R M N :
          (a : N) → P × Q)
        x).1

Tactic:
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Premises used: LinearMap.zero_apply, LinearMap.prodMap_apply, dualTensorHom_apply, smul_zero, LinearMap.fst_apply, LinearMap.coe_inl, LinearMap.coe_comp, Function.comp_apply, Prod.smul_mk
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
x : N
⊢ Eq.{u_6 + 1} (α := Q)
    ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inr R M N : (a : N) → P × Q)
        x).2
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
            inr R M N :
          (a : N) → P × Q)
        x).2

Tactic:
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Premises used: LinearMap.zero_apply, LinearMap.prodMap_apply, dualTensorHom_apply, smul_zero, LinearMap.fst_apply, LinearMap.coe_inl, LinearMap.coe_comp, Function.comp_apply, Prod.smul_mk
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
g : Dual R N
q : Q
hl :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := P)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).1
hl₁ :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := Q)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).2
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).2
hr :
  ∀ (x : N),
    Eq.{u_5 + 1} (α := P)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N :
            (a : N) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inr R M N :
            (a : N) → P × Q)
          x).1
hr₁ :
  ∀ (x : N),
    Eq.{u_6 + 1} (α := Q)
      ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N :
            (a : N) → P × Q)
          x).2
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
              inr R M N :
            (a : N) → P × Q)
          x).2
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)))
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
g : Dual R N
q : Q
x : M
⊢ Eq.{u_5 + 1} (α := P)
    ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N : (a : M) → P × Q)
        x).1
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
            inl R M N :
          (a : M) → P × Q)
        x).1

Tactic:
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Premises used: LinearMap.zero_apply, LinearMap.prodMap_apply, LinearMap.coe_inr, dualTensorHom_apply, smul_zero, LinearMap.coe_comp, Function.comp_apply, Prod.smul_mk, LinearMap.snd_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
g : Dual R N
q : Q
x : M
⊢ Eq.{u_6 + 1} (α := Q)
    ((prodMap 0 ((dualTensorHom R N Q : (a : Dual R N ⊗[R] Q) → N →ₗ[R] Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N : (a : M) → P × Q)
        x).2
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q : (a : Q) → P × Q) q) ∘ₗ
            inl R M N :
          (a : M) → P × Q)
        x).2

Tactic:
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Premises used: LinearMap.zero_apply, LinearMap.prodMap_apply, LinearMap.coe_inr, dualTensorHom_apply, smul_zero, LinearMap.coe_comp, Function.comp_apply, Prod.smul_mk, LinearMap.snd_apply