Theorem: BilinForm.baseChange_eval (AntLorentz/BaseChange.lean)

State before:
R✝ : Type ?u.164095
M✝ : Type ?u.164098
A✝ : Type ?u.164322
inst✝¹⁶ : CommSemiring R✝
inst✝¹⁵ : AddCommMonoid M✝
inst✝¹⁴ : Module R✝ M✝
inst✝¹³ : CommSemiring A✝
inst✝¹² : Algebra R✝ A✝
inst✝¹¹ : Invertible 2
R A M N T : Type
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : AddCommGroup T
inst✝² : Module A T
inst✝¹ : Module R T
inst✝ : IsScalarTower R A T
F : BilinForm R M
a b : A
m n : M
⊢ bilin (baseChange A F) (a ⊗ₜ[R] m) (b ⊗ₜ[R] n) = a * b * ↑(algebraMap R A) (bilin F m n)
Tactic:
unfold baseChange
State after:
R✝ : Type ?u.164095
M✝ : Type ?u.164098
A✝ : Type ?u.164322
inst✝¹⁶ : CommSemiring R✝
inst✝¹⁵ : AddCommMonoid M✝
inst✝¹⁴ : Module R✝ M✝
inst✝¹³ : CommSemiring A✝
inst✝¹² : Algebra R✝ A✝
inst✝¹¹ : Invertible 2
R A M N T : Type
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : AddCommGroup T
inst✝² : Module A T
inst✝¹ : Module R T
inst✝ : IsScalarTower R A T
F : BilinForm R M
a b : A
m n : M
⊢ bilin
      (let L := ↑(toLinHom R) F;
      let L' := LinearMap.baseChange A L;
      ↑LinearMap.toBilin
        (LinearMap.comp
          (LinearMap.baseChangeLeft R A (M →ₗ[R] R) (A ⊗[R] M →ₗ[A] A)
            (LinearMap.comp (↑R (↑(LinearMap.llcomp A (A ⊗[R] M) (A ⊗[R] R) A) (AlgebraTensorModule.lift (boop A))))
              (LinearMap.baseChangeHom R A M R)))
          L'))
      (a ⊗ₜ[R] m) (b ⊗ₜ[R] n) =
    a * b * ↑(algebraMap R A) (bilin F m n)

State before:
R✝ : Type ?u.164095
M✝ : Type ?u.164098
A✝ : Type ?u.164322
inst✝¹⁶ : CommSemiring R✝
inst✝¹⁵ : AddCommMonoid M✝
inst✝¹⁴ : Module R✝ M✝
inst✝¹³ : CommSemiring A✝
inst✝¹² : Algebra R✝ A✝
inst✝¹¹ : Invertible 2
R A M N T : Type
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : AddCommGroup T
inst✝² : Module A T
inst✝¹ : Module R T
inst✝ : IsScalarTower R A T
F : BilinForm R M
a b : A
m n : M
⊢ bilin
      (let L := ↑(toLinHom R) F;
      let L' := LinearMap.baseChange A L;
      ↑LinearMap.toBilin
        (LinearMap.comp
          (LinearMap.baseChangeLeft R A (M →ₗ[R] R) (A ⊗[R] M →ₗ[A] A)
            (LinearMap.comp (↑R (↑(LinearMap.llcomp A (A ⊗[R] M) (A ⊗[R] R) A) (AlgebraTensorModule.lift (boop A))))
              (LinearMap.baseChangeHom R A M R)))
          L'))
      (a ⊗ₜ[R] m) (b ⊗ₜ[R] n) =
    a * b * ↑(algebraMap R A) (bilin F m n)
Tactic:
dsimp
State after:
R✝ : Type ?u.164095
M✝ : Type ?u.164098
A✝ : Type ?u.164322
inst✝¹⁶ : CommSemiring R✝
inst✝¹⁵ : AddCommMonoid M✝
inst✝¹⁴ : Module R✝ M✝
inst✝¹³ : CommSemiring A✝
inst✝¹² : Algebra R✝ A✝
inst✝¹¹ : Invertible 2
R A M N T : Type
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : AddCommGroup T
inst✝² : Module A T
inst✝¹ : Module R T
inst✝ : IsScalarTower R A T
F : BilinForm R M
a b : A
m n : M
⊢ bilin
      (↑LinearMap.toBilin
        (LinearMap.comp
          (LinearMap.baseChangeLeft R A (M →ₗ[R] R) (A ⊗[R] M →ₗ[A] A)
            (LinearMap.comp (↑R (↑(LinearMap.llcomp A (A ⊗[R] M) (A ⊗[R] R) A) (AlgebraTensorModule.lift (boop A))))
              (LinearMap.baseChangeHom R A M R)))
          (LinearMap.baseChange A (↑(toLinHom R) F))))
      (a ⊗ₜ[R] m) (b ⊗ₜ[R] n) =
    a * b * ↑(algebraMap R A) (bilin F m n)

State before:
R✝ : Type ?u.164095
M✝ : Type ?u.164098
A✝ : Type ?u.164322
inst✝¹⁶ : CommSemiring R✝
inst✝¹⁵ : AddCommMonoid M✝
inst✝¹⁴ : Module R✝ M✝
inst✝¹³ : CommSemiring A✝
inst✝¹² : Algebra R✝ A✝
inst✝¹¹ : Invertible 2
R A M N T : Type
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : AddCommGroup T
inst✝² : Module A T
inst✝¹ : Module R T
inst✝ : IsScalarTower R A T
F : BilinForm R M
a b : A
m n : M
⊢ bilin
      (↑LinearMap.toBilin
        (LinearMap.comp
          (LinearMap.baseChangeLeft R A (M →ₗ[R] R) (A ⊗[R] M →ₗ[A] A)
            (LinearMap.comp (↑R (↑(LinearMap.llcomp A (A ⊗[R] M) (A ⊗[R] R) A) (AlgebraTensorModule.lift (boop A))))
              (LinearMap.baseChangeHom R A M R)))
          (LinearMap.baseChange A (↑(toLinHom R) F))))
      (a ⊗ₜ[R] m) (b ⊗ₜ[R] n) =
    a * b * ↑(algebraMap R A) (bilin F m n)
Tactic:
unfold bilin
State after:
R✝ : Type ?u.164095
M✝ : Type ?u.164098
A✝ : Type ?u.164322
inst✝¹⁶ : CommSemiring R✝
inst✝¹⁵ : AddCommMonoid M✝
inst✝¹⁴ : Module R✝ M✝
inst✝¹³ : CommSemiring A✝
inst✝¹² : Algebra R✝ A✝
inst✝¹¹ : Invertible 2
R A M N T : Type
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : AddCommGroup T
inst✝² : Module A T
inst✝¹ : Module R T
inst✝ : IsScalarTower R A T
F : BilinForm R M
a b : A
m n : M
⊢ (↑LinearMap.toBilin
          (LinearMap.comp
            (LinearMap.baseChangeLeft R A (M →ₗ[R] R) (A ⊗[R] M →ₗ[A] A)
              (LinearMap.comp (↑R (↑(LinearMap.llcomp A (A ⊗[R] M) (A ⊗[R] R) A) (AlgebraTensorModule.lift (boop A))))
                (LinearMap.baseChangeHom R A M R)))
            (LinearMap.baseChange A (↑(toLinHom R) F)))).1
      (a ⊗ₜ[R] m) (b ⊗ₜ[R] n) =
    a * b * ↑(algebraMap R A) (F.1 m n)

State before:
R✝ : Type ?u.164095
M✝ : Type ?u.164098
A✝ : Type ?u.164322
inst✝¹⁶ : CommSemiring R✝
inst✝¹⁵ : AddCommMonoid M✝
inst✝¹⁴ : Module R✝ M✝
inst✝¹³ : CommSemiring A✝
inst✝¹² : Algebra R✝ A✝
inst✝¹¹ : Invertible 2
R A M N T : Type
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : AddCommGroup T
inst✝² : Module A T
inst✝¹ : Module R T
inst✝ : IsScalarTower R A T
F : BilinForm R M
a b : A
m n : M
⊢ (↑LinearMap.toBilin
          (LinearMap.comp
            (LinearMap.baseChangeLeft R A (M →ₗ[R] R) (A ⊗[R] M →ₗ[A] A)
              (LinearMap.comp (↑R (↑(LinearMap.llcomp A (A ⊗[R] M) (A ⊗[R] R) A) (AlgebraTensorModule.lift (boop A))))
                (LinearMap.baseChangeHom R A M R)))
            (LinearMap.baseChange A (↑(toLinHom R) F)))).1
      (a ⊗ₜ[R] m) (b ⊗ₜ[R] n) =
    a * b * ↑(algebraMap R A) (F.1 m n)
Tactic:
sorry
State after:
no goals