internlm/Lean-Github huggingface dataset:
Theorem: MulLECancellable.of_hMul_left
Proof state before:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * (b * x) ≤ a * (b * y)
Tactic:
exact mul_le_mul_left' h a
Proof state after:
no goals
Theorem: Function.update_head
Proof state before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ update (vecCons x t) 0 y = vecCons y t
Tactic:
rw [funext_iff, Fin.forall_fin_succ]
Proof state after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ update (vecCons x t) 0 y 0 = vecCons y t 0 ∧
    ∀ (i_1 : Fin i), update (vecCons x t) 0 y (succ i_1) = vecCons y t (succ i_1)
Theorem: Function.update_head
Proof state before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ update (vecCons x t) 0 y 0 = vecCons y t 0 ∧
    ∀ (i_1 : Fin i), update (vecCons x t) 0 y (succ i_1) = vecCons y t (succ i_1)
Tactic:
refine' ⟨rfl, fun j => _⟩
Proof state after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ update (vecCons x t) 0 y (succ j) = vecCons y t (succ j)
Theorem: Function.update_head
Proof state before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ update (vecCons x t) 0 y (succ j) = vecCons y t (succ j)
Tactic:
rw [update_noteq]
Proof state after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ vecCons x t (succ j) = vecCons y t (succ j)

case h
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ j ≠ 0
Theorem: Function.update_head
Proof state before:
case h
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ j ≠ 0
Tactic:
exact succ_ne_zero j
Proof state after:
no goals
Theorem: Function.update_head
Proof state before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ vecCons x t (succ j) = vecCons y t (succ j)
Tactic:
simp only [vecCons, Fin.cons_succ]
Proof state after:
no goals
Theorem: Function.update_cons_one
Proof state before:
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
⊢ update (vecCons x (vecCons y t)) 1 z = vecCons x (vecCons z t)
Tactic:
simp only [funext_iff, forall_fin_succ]
Proof state after:
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
⊢ update (vecCons x (vecCons y t)) 1 z 0 = vecCons x (vecCons z t) 0 ∧
    update (vecCons x (vecCons y t)) 1 z (succ 0) = vecCons x (vecCons z t) (succ 0) ∧
      ∀ (i_1 : Fin i),
        update (vecCons x (vecCons y t)) 1 z (succ (succ i_1)) = vecCons x (vecCons z t) (succ (succ i_1))
Theorem: Function.update_cons_one
Proof state before:
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
⊢ update (vecCons x (vecCons y t)) 1 z 0 = vecCons x (vecCons z t) 0 ∧
    update (vecCons x (vecCons y t)) 1 z (succ 0) = vecCons x (vecCons z t) (succ 0) ∧
      ∀ (i_1 : Fin i),
        update (vecCons x (vecCons y t)) 1 z (succ (succ i_1)) = vecCons x (vecCons z t) (succ (succ i_1))
Tactic:
refine' ⟨rfl, rfl, fun j => _⟩
Proof state after:
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
j : Fin i
⊢ update (vecCons x (vecCons y t)) 1 z (succ (succ j)) = vecCons x (vecCons z t) (succ (succ j))
Theorem: Function.update_cons_one
Proof state before:
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
j : Fin i
⊢ update (vecCons x (vecCons y t)) 1 z (succ (succ j)) = vecCons x (vecCons z t) (succ (succ j))
Tactic:
rw [update_noteq]
Proof state after:
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
j : Fin i
⊢ vecCons x (vecCons y t) (succ (succ j)) = vecCons x (vecCons z t) (succ (succ j))

case h
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 1
Theorem: Function.update_cons_one
Proof state before:
case h
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 1
Tactic:
exact (succ_injective _).ne (Fin.succ_ne_zero _)
Proof state after:
no goals
Theorem: Function.update_cons_one
Proof state before:
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
j : Fin i
⊢ vecCons x (vecCons y t) (succ (succ j)) = vecCons x (vecCons z t) (succ (succ j))
Tactic:
simp only [vecCons, cons_succ]
Proof state after:
no goals
Theorem: Function.update_cons_two
Proof state before:
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
⊢ update (vecCons w (vecCons x (vecCons y t))) 2 z = vecCons w (vecCons x (vecCons z t))
Tactic:
simp only [funext_iff, forall_fin_succ]
Proof state after:
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
⊢ update (vecCons w (vecCons x (vecCons y t))) 2 z 0 = vecCons w (vecCons x (vecCons z t)) 0 ∧
    update (vecCons w (vecCons x (vecCons y t))) 2 z (succ 0) = vecCons w (vecCons x (vecCons z t)) (succ 0) ∧
      update (vecCons w (vecCons x (vecCons y t))) 2 z (succ (succ 0)) =
          vecCons w (vecCons x (vecCons z t)) (succ (succ 0)) ∧
        ∀ (i_1 : Fin i),
          update (vecCons w (vecCons x (vecCons y t))) 2 z (succ (succ (succ i_1))) =
            vecCons w (vecCons x (vecCons z t)) (succ (succ (succ i_1)))
Theorem: Function.update_cons_two
Proof state before:
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
⊢ update (vecCons w (vecCons x (vecCons y t))) 2 z 0 = vecCons w (vecCons x (vecCons z t)) 0 ∧
    update (vecCons w (vecCons x (vecCons y t))) 2 z (succ 0) = vecCons w (vecCons x (vecCons z t)) (succ 0) ∧
      update (vecCons w (vecCons x (vecCons y t))) 2 z (succ (succ 0)) =
          vecCons w (vecCons x (vecCons z t)) (succ (succ 0)) ∧
        ∀ (i_1 : Fin i),
          update (vecCons w (vecCons x (vecCons y t))) 2 z (succ (succ (succ i_1))) =
            vecCons w (vecCons x (vecCons z t)) (succ (succ (succ i_1)))
Tactic:
refine' ⟨rfl, rfl, rfl, fun j => _⟩
Proof state after:
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
j : Fin i
⊢ update (vecCons w (vecCons x (vecCons y t))) 2 z (succ (succ (succ j))) =
    vecCons w (vecCons x (vecCons z t)) (succ (succ (succ j)))
Theorem: Function.update_cons_two
Proof state before:
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
j : Fin i
⊢ update (vecCons w (vecCons x (vecCons y t))) 2 z (succ (succ (succ j))) =
    vecCons w (vecCons x (vecCons z t)) (succ (succ (succ j)))
Tactic:
rw [update_noteq]
Proof state after:
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
j : Fin i
⊢ vecCons w (vecCons x (vecCons y t)) (succ (succ (succ j))) =
    vecCons w (vecCons x (vecCons z t)) (succ (succ (succ j)))

case h
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
j : Fin i
⊢ succ (succ (succ j)) ≠ 2
Theorem: Function.update_cons_two
Proof state before:
case h
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
j : Fin i
⊢ succ (succ (succ j)) ≠ 2
Tactic:
exact (succ_injective _).ne ((succ_injective _).ne (succ_ne_zero _))
Proof state after:
no goals
Theorem: Function.update_cons_two
Proof state before:
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
j : Fin i
⊢ vecCons w (vecCons x (vecCons y t)) (succ (succ (succ j))) =
    vecCons w (vecCons x (vecCons z t)) (succ (succ (succ j)))
Tactic:
simp only [vecCons, cons_succ]
Proof state after:
no goals
Theorem: Function.swap_cons
Proof state before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1) = vecCons y (vecCons x t)
Tactic:
rw [funext_iff]
Proof state after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ ∀ (a : Fin (Nat.succ (Nat.succ i))), (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) a = vecCons y (vecCons x t) a
Theorem: Function.swap_cons
Proof state before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ ∀ (a : Fin (Nat.succ (Nat.succ i))), (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) a = vecCons y (vecCons x t) a
Tactic:
simp only [forall_fin_succ]
Proof state after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) 0 = vecCons y (vecCons x t) 0 ∧
    (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ 0) = vecCons y (vecCons x t) (succ 0) ∧
      ∀ (i_1 : Fin i),
        (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ (succ i_1)) = vecCons y (vecCons x t) (succ (succ i_1))
Theorem: Function.swap_cons
Proof state before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) 0 = vecCons y (vecCons x t) 0 ∧
    (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ 0) = vecCons y (vecCons x t) (succ 0) ∧
      ∀ (i_1 : Fin i),
        (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ (succ i_1)) = vecCons y (vecCons x t) (succ (succ i_1))
Tactic:
refine' ⟨rfl, rfl, fun j => _⟩
Proof state after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ (succ j)) = vecCons y (vecCons x t) (succ (succ j))
Theorem: Function.swap_cons
Proof state before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ (succ j)) = vecCons y (vecCons x t) (succ (succ j))
Tactic:
simp only [vecCons, cons_succ, comp_apply]
Proof state after:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ cons x (cons y t) (↑(Equiv.swap 0 1) (succ (succ j))) = t j
Theorem: Function.swap_cons
Proof state before:
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ cons x (cons y t) (↑(Equiv.swap 0 1) (succ (succ j))) = t j
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne, cons_succ, cons_succ]
Proof state after:
case a
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 0

case a
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 1
Theorem: Function.swap_cons
Proof state before:
case a
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 1
Tactic:
exact (succ_injective _).ne (succ_ne_zero _)
Proof state after:
no goals
Theorem: Function.swap_cons
Proof state before:
case a
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 0
Tactic:
exact succ_ne_zero _
Proof state after:
no goals
Theorem: BilinForm.baseChange_eval
Proof 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
Proof 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)
Theorem: BilinForm.baseChange_eval
Proof 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
Proof 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)
Theorem: BilinForm.baseChange_eval
Proof 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
Proof 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)
Theorem: BilinForm.baseChange_eval
Proof 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
Proof state after:
no goals
Theorem: QuadraticForm.baseChange_eval
Proof state before:
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
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
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ ↑(baseChange A F) (a ⊗ₜ[R] m) = a * a * ↑(algebraMap R A) (↑F m)
Tactic:
rw [baseChange, BilinForm.toQuadraticForm_apply, BilinForm.baseChange_eval, associated_apply,
    ← two_smul R m, QuadraticForm.map_smul]
Proof state after:
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
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
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ a * a * ↑(algebraMap R A) (⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m)) = a * a * ↑(algebraMap R A) (↑F m)
Theorem: QuadraticForm.baseChange_eval
Proof state before:
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
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
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ a * a * ↑(algebraMap R A) (⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m)) = a * a * ↑(algebraMap R A) (↑F m)
Tactic:
congr
Proof state after:
case e_a.h.e_6.h
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
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
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ ⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m) = ↑F m
Theorem: QuadraticForm.baseChange_eval
Proof state before:
case e_a.h.e_6.h
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
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
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ ⅟2 * (2 * 2 * ↑F m - ↑F m - ↑F m) = ↑F m
Tactic:
rw [mul_assoc, invOf_mul_eq_iff_eq_mul_left]
Proof state after:
case e_a.h.e_6.h
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
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
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ 2 * (2 * ↑F m) - ↑F m - ↑F m = 2 * ↑F m
Theorem: QuadraticForm.baseChange_eval
Proof state before:
case e_a.h.e_6.h
R✝ : Type ?u.206610
M✝ : Type ?u.206613
A✝ : Type ?u.206837
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
a : A
F : QuadraticForm R M
m : M
inst✝ : Invertible 2
⊢ 2 * (2 * ↑F m) - ↑F m - ↑F m = 2 * ↑F m
Tactic:
ring
Proof state after:
no goals
Theorem: BilinForm.baseChangeSymm
Proof state before:
R✝ : Type ?u.255543
M✝ : Type ?u.255546
A✝ : Type ?u.255770
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
hF : IsSymm F
⊢ IsSymm (baseChange A F)
Tactic:
simp [IsSymm] at *
Proof state after:
R✝ : Type ?u.255543
M✝ : Type ?u.255546
A✝ : Type ?u.255770
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
hF : ∀ (x y : M), bilin F x y = bilin F y x
⊢ ∀ (x y : A ⊗[R] M), bilin (baseChange A F) x y = bilin (baseChange A F) y x
Theorem: BilinForm.baseChangeSymm
Proof state before:
R✝ : Type ?u.255543
M✝ : Type ?u.255546
A✝ : Type ?u.255770
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
hF : ∀ (x y : M), bilin F x y = bilin F y x
⊢ ∀ (x y : A ⊗[R] M), bilin (baseChange A F) x y = bilin (baseChange A F) y x
Tactic:
intros x y
Proof state after:
R✝ : Type ?u.255543
M✝ : Type ?u.255546
A✝ : Type ?u.255770
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
hF : ∀ (x y : M), bilin F x y = bilin F y x
x y : A ⊗[R] M
⊢ bilin (baseChange A F) x y = bilin (baseChange A F) y x