awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v w : V
| ((((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) w) : V →ₗ[K] K) : (a : V) → K) v : K)
have rw : ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
Tactic: rw [comp_symmCompOfNondegenerate_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v w : V
⊢ Eq.{u_6 + 1} (α := K)
    ((((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) w) : V →ₗ[K] K) : (a : V) → K) v :
      K)
    ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
have conv_lhs : Eq.{u_6 + 1} (α := K)
  ((((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) w) : V →ₗ[K] K) : (a : V) → K) v : K)
  ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
Tactic: conv_lhs => rw [comp_symmCompOfNondegenerate_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v w : V
conv_lhs :
  Eq.{u_6 + 1} (α := K)
    ((((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) w) : V →ₗ[K] K) : (a : V) → K) v :
      K)
    ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) w) : V →ₗ[K] K) : (a : V) → K) v :
      K)
    ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
have conv_lhs₁ : Eq.{u_6 + 1} (α := K) ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
  ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
Tactic: conv_lhs => rw [comp_symmCompOfNondegenerate_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Algebra R A
inst_7 : Module R M₁
inst_8 : Module A M₁
inst_9 : Module R N₁
inst_10 : Module A N₁
inst_11 : SMulCommClass R A M₁
inst_12 : IsScalarTower R A M₁
inst_13 : SMulCommClass R A N₁
inst_14 : IsScalarTower R A N₁
inst_15 : Module R M₂
inst_16 : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ :
  ∀ (x y : M₁),
    Eq.{uN₁ + 1} (α := N₁) ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) x : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) y : N₁)
      ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) y : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) x : N₁)
hB₂ :
  ∀ (x y : M₂),
    Eq.{uN₂ + 1} (α := N₂) ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) x : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) y : N₂)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) y : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) x : N₂)
x y : M₁ ⊗[R] M₂
⊢ Eq (α := N₁ ⊗[R] N₂)
    ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) x : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
          (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        y :
      N₁ ⊗[R] N₂)
    ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) y : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
          (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        x :
      N₁ ⊗[R] N₂)
have revert : ∀ (x y : M₁ ⊗[R] M₂),
  Eq (α := N₁ ⊗[R] N₂)
    ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) x : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
          (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        y :
      N₁ ⊗[R] N₂)
    ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) y : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
          (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        x :
      N₁ ⊗[R] N₂)
Tactic: revert x y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Algebra R A
inst_7 : Module R M₁
inst_8 : Module A M₁
inst_9 : Module R N₁
inst_10 : Module A N₁
inst_11 : SMulCommClass R A M₁
inst_12 : IsScalarTower R A M₁
inst_13 : SMulCommClass R A N₁
inst_14 : IsScalarTower R A N₁
inst_15 : Module R M₂
inst_16 : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ :
  ∀ (x y : M₁),
    Eq.{uN₁ + 1} (α := N₁) ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) x : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) y : N₁)
      ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) y : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) x : N₁)
hB₂ :
  ∀ (x y : M₂),
    Eq.{uN₂ + 1} (α := N₂) ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) x : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) y : N₂)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) y : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) x : N₂)
⊢ ∀ (x y : M₁ ⊗[R] M₂),
    Eq (α := N₁ ⊗[R] N₂)
      ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) x : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
            (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          y :
        N₁ ⊗[R] N₂)
      ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) y : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
            (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          x :
        N₁ ⊗[R] N₂)
have rw : Eq (α := BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) (B₁.tmul B₂) (flip (B₁.tmul B₂))
Tactic: rw [isSymm_iff_eq_flip]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : Algebra R A
inst_5 : Module R M₁
inst_6 : Module A M₁
inst_7 : SMulCommClass R A M₁
inst_8 : IsScalarTower R A M₁
inst_9 : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ IsSymm (M := M₁ ⊗[R] M₂) (B₁.tmul B₂)
have rw : Eq (α := BilinForm A (M₁ ⊗[R] M₂)) (B₁.tmul B₂) (LinearMap.flip (B₁.tmul B₂))
Tactic: rw [LinearMap.isSymm_iff_eq_flip]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : Algebra R A
inst_5 : Module R M₁
inst_6 : Module A M₁
inst_7 : SMulCommClass R A M₁
inst_8 : IsScalarTower R A M₁
inst_9 : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ Eq (α := BilinForm A (M₁ ⊗[R] M₂)) (B₁.tmul B₂) (LinearMap.flip (B₁.tmul B₂))
have a : ∀ (x₁ : M₁) (x₂ : M₂) (y₁ : M₁) (y₂ : M₂),
  Eq.{uA + 1} (α := A)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry (B₁.tmul B₂) : M₁ →ₗ[A] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A)
                            x₁ :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[A] A)
                      x₂) :
                  M₁ →ₗ[A] M₂ →ₗ[R] A) :
                (a : M₁) → M₂ →ₗ[R] A)
              y₁ :
            M₂ →ₗ[R] A) :
          (a : M₂) → A)
        y₂ :
      A)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry (LinearMap.flip (B₁.tmul B₂)) :
                                M₁ →ₗ[A] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                              (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A)
                            x₁ :
                          M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                        (a : M₂) → M₁ ⊗[R] M₂ →ₗ[A] A)
                      x₂) :
                  M₁ →ₗ[A] M₂ →ₗ[R] A) :
                (a : M₁) → M₂ →ₗ[R] A)
              y₁ :
            M₂ →ₗ[R] A) :
          (a : M₂) → A)
        y₂ :
      A)
Tactic: ext x₁ x₂ y₁ y₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
⊢ Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A 0) 0
have a : ∀ (x x_1 : M₂),
  Eq.{uA + 1} (α := A)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry (BilinForm.baseChange A 0) : A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] A)
                    x) :
                A →ₗ[A] M₂ →ₗ[R] A) :
              (a : A) → M₂ →ₗ[R] A)
            1 :
          (a : M₂) → A)
        x_1 :
      A)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry 0 : A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] A)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] A)
                    x) :
                A →ₗ[A] M₂ →ₗ[R] A) :
              (a : A) → M₂ →ₗ[R] A)
            1 :
          (a : M₂) → A)
        x_1 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : FaithfulSMul R A
B : BilinForm R M₂
⊢ Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A B) 0 ↔ B = 0
have refine : ∀ (h : Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A B) 0), B = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : FaithfulSMul R A
B : BilinForm R M₂
h : Eq (α := BilinForm A (A ⊗[R] M₂)) (BilinForm.baseChange A B) 0
⊢ B = 0
have H : ∀ (m m' : M₂),
  Eq.{uR + 1} (α := R) ((((B : (a : M₂) → M₂ →ₗ[R] R) m : M₂ →ₗ[R] R) : (a : M₂) → R) m' : R)
    ((((0 : (a : M₂) → M₂ →ₗ[R] R) m : M₂ →ₗ[R] R) : (a : M₂) → R) m' : R)
Tactic: ext m m'
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.TensorProduct (goal)
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Module.Free R M₁
inst_6 : Module.Finite R M₁
inst_7 : Module.Free R M₂
inst_8 : Module.Finite R M₂
⊢ Eq (α := BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
    (↑(tensorDistribEquiv R) : BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) (tensorDistrib R R)
have a : ∀ (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂),
  Eq (α := BilinForm R (M₁ ⊗[R] M₂))
    (((((AlgebraTensorModule.curry
                    (↑(tensorDistribEquiv R) : BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                  BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
              B₁ :
            BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
          (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
        B₂ :
      BilinForm R (M₁ ⊗[R] M₂))
    (((((AlgebraTensorModule.curry (tensorDistrib R R) :
                  BilinForm R M₁ →ₗ[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
                (a : BilinForm R M₁) → BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂))
              B₁ :
            BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂)) :
          (a : BilinForm R M₂) → BilinForm R (M₁ ⊗[R] M₂))
        B₂ :
      BilinForm R (M₁ ⊗[R] M₂))
Tactic: ext B₁ B₂ : 3
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₅
σ₂₃ : R₂ →+* R₃
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module R₂ N
inst_9 : Module R₃ P
inst_10 : Module R₅ P
inst_11 : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
⊢ h.compl₂ id = h
have h₁ : ∀ (x : M) (x_1 : N),
  Eq.{u_21 + 1} (α := P) ((((h.compl₂ id : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₅
σ₂₃ : R₂ →+* R₃
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module R₂ N
inst_9 : Module R₃ P
inst_10 : Module R₅ P
inst_11 : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
x : M
x_1 : N
⊢ Eq.{u_21 + 1} (α := P) ((((h.compl₂ id : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
have h₁ : Eq.{u_21 + 1} (α := P)
  ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) ((id : (a : N) → N) x_1 : N) : P)
  ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
Tactic: rw [compl₂_apply, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₅
σ₂₃ : R₂ →+* R₃
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module R₂ N
inst_9 : Module R₃ P
inst_10 : Module R₅ P
inst_11 : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
x : M
x_1 : N
h₁ :
  Eq.{u_21 + 1} (α := P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) ((id : (a : N) → N) x_1 : N) : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
⊢ Eq.{u_21 + 1} (α := P) ((((h.compl₂ id : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
have h₂ : Eq.{u_21 + 1} (α := P) ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) (_root_.id x_1) : P)
  ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
Tactic: rw [compl₂_apply, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₅
σ₂₃ : R₂ →+* R₃
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module R₂ N
inst_9 : Module R₃ P
inst_10 : Module R₅ P
inst_11 : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
x : M
x_1 : N
h₁ :
  Eq.{u_21 + 1} (α := P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) ((id : (a : N) → N) x_1 : N) : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
h₂ :
  Eq.{u_21 + 1} (α := P) ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) (_root_.id x_1) : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
⊢ Eq.{u_21 + 1} (α := P) ((((h.compl₂ id : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
    ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
have h₃ : Eq.{u_21 + 1} (α := P) ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
  ((((h : (a : M) → N →ₛₗ[σ₂₃] P) x : N →ₛₗ[σ₂₃] P) : (a : N) → P) x_1 : P)
Tactic: rw [compl₂_apply, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
N : Type u_7
P : Type u_9
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
H : f.flip = g.flip
m : M
n : N
⊢ Eq.{u_9 + 1} (α := P) ((((f.flip : (a : N) → M →ₛₗ[ρ₁₂] P) n : M →ₛₗ[ρ₁₂] P) : (a : M) → P) m : P)
    ((((g.flip : (a : N) → M →ₛₗ[ρ₁₂] P) n : M →ₛₗ[ρ₁₂] P) : (a : M) → P) m : P)
have rw : Eq.{u_9 + 1} (α := P) ((((g.flip : (a : N) → M →ₛₗ[ρ₁₂] P) n : M →ₛₗ[ρ₁₂] P) : (a : M) → P) m : P)
  ((((g.flip : (a : N) → M →ₛₗ[ρ₁₂] P) n : M →ₛₗ[ρ₁₂] P) : (a : M) → P) m : P)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid P
inst_9 : AddCommMonoid P₂
inst_10 : AddCommMonoid Pₗ
inst_11 : Module R M
inst_12 : Module R M₂
inst_13 : Module S N
inst_14 : Module S N₂
inst_15 : Module R₂ P
inst_16 : Module S₂ P
inst_17 : Module R P₂
inst_18 : Module S₂ P₂
inst_19 : Module R Pₗ
inst_20 : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst_21 : AddCommGroup M'
inst_22 : AddCommGroup P'
inst_23 : Module R M'
inst_24 : Module R₂ P'
inst_25 : Module S₂ P'
inst_26 : SMulCommClass S₂ R₂ P
inst_27 : SMulCommClass S R Pₗ
inst_28 : SMulCommClass S₂ R₂ P'
inst_29 : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst_30 : Semiring R'
inst_31 : Semiring S'
inst_32 : Module R' M
inst_33 : Module S' N
inst_34 : Module R' Pₗ
inst_35 : Module S' Pₗ
inst_36 : SMulCommClass S' R' Pₗ
inst_37 : SMul S' S
inst_38 : IsScalarTower S' S N
inst_39 : IsScalarTower S' S Pₗ
inst_40 : SMul R' R
inst_41 : IsScalarTower R' R M
inst_42 : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x : N
⊢ (((B : (a : M) → N →ₗ[S] Pₗ) (r' • m) : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
have rw : (((B : (a : M) → N →ₗ[S] Pₗ) (HSMul.hSMul (β := R) r' 1 • m) : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x =
  HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
Tactic: rw [← smul_one_smul R r' m, map_smul₂, smul_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid P
inst_9 : AddCommMonoid P₂
inst_10 : AddCommMonoid Pₗ
inst_11 : Module R M
inst_12 : Module R M₂
inst_13 : Module S N
inst_14 : Module S N₂
inst_15 : Module R₂ P
inst_16 : Module S₂ P
inst_17 : Module R P₂
inst_18 : Module S₂ P₂
inst_19 : Module R Pₗ
inst_20 : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst_21 : AddCommGroup M'
inst_22 : AddCommGroup P'
inst_23 : Module R M'
inst_24 : Module R₂ P'
inst_25 : Module S₂ P'
inst_26 : SMulCommClass S₂ R₂ P
inst_27 : SMulCommClass S R Pₗ
inst_28 : SMulCommClass S₂ R₂ P'
inst_29 : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst_30 : Semiring R'
inst_31 : Semiring S'
inst_32 : Module R' M
inst_33 : Module S' N
inst_34 : Module R' Pₗ
inst_35 : Module S' Pₗ
inst_36 : SMulCommClass S' R' Pₗ
inst_37 : SMul S' S
inst_38 : IsScalarTower S' S N
inst_39 : IsScalarTower S' S Pₗ
inst_40 : SMul R' R
inst_41 : IsScalarTower R' R M
inst_42 : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x : N
rw :
  (((B : (a : M) → N →ₗ[S] Pₗ) (HSMul.hSMul (β := R) r' 1 • m) : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
⊢ (((B : (a : M) → N →ₗ[S] Pₗ) (r' • m) : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
have rw₁ : HSMul.hSMul (β := Pₗ) (HSMul.hSMul (β := R) r' 1)
    ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ) =
  HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
Tactic: rw [← smul_one_smul R r' m, map_smul₂, smul_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid P
inst_9 : AddCommMonoid P₂
inst_10 : AddCommMonoid Pₗ
inst_11 : Module R M
inst_12 : Module R M₂
inst_13 : Module S N
inst_14 : Module S N₂
inst_15 : Module R₂ P
inst_16 : Module S₂ P
inst_17 : Module R P₂
inst_18 : Module S₂ P₂
inst_19 : Module R Pₗ
inst_20 : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst_21 : AddCommGroup M'
inst_22 : AddCommGroup P'
inst_23 : Module R M'
inst_24 : Module R₂ P'
inst_25 : Module S₂ P'
inst_26 : SMulCommClass S₂ R₂ P
inst_27 : SMulCommClass S R Pₗ
inst_28 : SMulCommClass S₂ R₂ P'
inst_29 : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst_30 : Semiring R'
inst_31 : Semiring S'
inst_32 : Module R' M
inst_33 : Module S' N
inst_34 : Module R' Pₗ
inst_35 : Module S' Pₗ
inst_36 : SMulCommClass S' R' Pₗ
inst_37 : SMul S' S
inst_38 : IsScalarTower S' S N
inst_39 : IsScalarTower S' S Pₗ
inst_40 : SMul R' R
inst_41 : IsScalarTower R' R M
inst_42 : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x : N
rw :
  (((B : (a : M) → N →ₗ[S] Pₗ) (HSMul.hSMul (β := R) r' 1 • m) : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
rw₁ :
  HSMul.hSMul (β := Pₗ) (HSMul.hSMul (β := R) r' 1)
      ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ) =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
⊢ (((B : (a : M) → N →ₗ[S] Pₗ) (r' • m) : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x =
    HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
have rw₂ : HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ) =
  HSMul.hSMul (β := Pₗ) r' ((((B : (a : M) → N →ₗ[S] Pₗ) m : N →ₗ[S] Pₗ) : (a : N) → Pₗ) x : Pₗ)
Tactic: rw [← smul_one_smul R r' m, map_smul₂, smul_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : Module R₁ Mₗ
inst_6 : Module R₂ N
inst_7 : Module R₂ Pₗ
inst_8 : Module R₁ Pₗ
inst_9 : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
⊢ f.compl₁₂ id id = f
have h : ∀ (x : Mₗ) (x_1 : N),
  Eq.{u_9 + 1} (α := Pₗ) ((((f.compl₁₂ id id : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
Tactic: ext