mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup G
inst✝² : Module R G
inst✝¹ : DecidableEq G
s : Finset R
t : Finset G
inst✝ : DecidableEq R
⊢ -s • t = -(s • t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.i = -c₁ • q.j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.j = c₃ • q.i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
ih_y :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦y⟧ =
    F ⟦y⟧
hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
this : ∀ (x y : EnvelGroup R), F (Mul.mul x y) = F x * F y
⊢ mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) = F ⟦x.mul y⟧

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.j * q.k = (c₂ * c₃) • 1 - c₃ • q.i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    ((algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)) *
        ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
      (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.k = -((c₁ * c₃) • 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.lift 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.lift 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (x + y) = q.lift x + q.lift y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Distrib R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonUnitalNonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toDistrib R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ inst₁.toAddMonoid = inst₂.toAddMonoid

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (x * y) = q.lift x * q.lift y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (r • x) = r • q.lift x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
⊢ NatCast.natCast = NatCast.natCast

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ inst₁ = inst₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ B.i ∈ {B.i, B.j, B.k}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toAddMonoidWithOne R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ B.j ∈ {B.i, B.j, B.k}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
⊢ inst₁ = inst₂

Tactic:
have h_zero : (inst₁.toMulZeroClass).toZero.zero = (inst₂.toMulZeroClass).toZero.zero :=
    congrArg (fun inst => (inst.toMulZeroClass).toZero.zero) h

Goal state after:
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ B.k ∈ {B.i, B.j, B.k}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ inst₁.toMulZeroOneClass.toOne = inst₂.toMulZeroOneClass.toOne

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : inst₁.toMulZeroOneClass.toOne = inst₂.toMulZeroOneClass.toOne
h_one : One.one = One.one
⊢ inst₁.toAddCommMonoidWithOne = inst₂.toAddCommMonoidWithOne

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ B.liftHom.range = R[B.i, B.j, B.k]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F q.i * F q.i = c₁ • 1 + c₂ • F q.i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F q.j * F q.j = c₃ • 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F q.i * F q.j = F q.k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F q.j * F q.i = c₂ • F q.j - F q.k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ (Basis.self R).compHom q.liftHom = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonUnitalNonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
⊢ ((Basis.self R).compHom F).liftHom = F

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ ↑j + 1 ≤ n i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonUnitalRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonUnitalRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ y₁ y₂ : R
⊢ (x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ y₁ y₂ n : R
⊢ (x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
⊢ a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
⊢ a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocRing R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
⊢ inst₁.toAddGroup = inst₂.toAddGroup

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) ^ 2 +
        (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) ^ 2 +
      (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
⊢ IntCast.intCast = IntCast.intCast

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ inst₁ = inst₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ inst₁ = inst₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
i : ι
hi : i ∈ s
⊢ (algebraMap R[X] K) (g i) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing
⊢ inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
i : ι
hi : i ∈ s
⊢ (algebraMap R[X] K) (g i) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
⊢ (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
⊢ ∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocSemiring R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁.toAddCommMonoid = inst₂.toAddCommMonoid

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid
⊢ inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid
h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring
⊢ inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid
h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring
h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring
⊢ inst₁.toMonoidWithZero.toMonoid = inst₂.toMonoidWithZero.toMonoid

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
r₁ : Bool → R[X] := fun t ↦ Bool.rec r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun t ↦ Bool.rec r₂₂ r₁₂ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
⊢ (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Identities

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2 + x₅ ^ 2 + x₆ ^ 2 + x₇ ^ 2 + x₈ ^ 2) *
      (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2 + y₅ ^ 2 + y₆ ^ 2 + y₇ ^ 2 + y₈ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄ - x₅ * y₅ - x₆ * y₆ - x₇ * y₇ - x₈ * y₈) ^ 2 +
                  (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃ + x₅ * y₆ - x₆ * y₅ - x₇ * y₈ + x₈ * y₇) ^ 2 +
                (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂ + x₅ * y₇ + x₆ * y₈ - x₇ * y₅ - x₈ * y₆) ^ 2 +
              (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁ + x₅ * y₈ - x₆ * y₇ + x₇ * y₆ - x₈ * y₅) ^ 2 +
            (x₁ * y₅ - x₂ * y₆ - x₃ * y₇ - x₄ * y₈ + x₅ * y₁ + x₆ * y₂ + x₇ * y₃ + x₈ * y₄) ^ 2 +
          (x₁ * y₆ + x₂ * y₅ - x₃ * y₈ + x₄ * y₇ - x₅ * y₂ + x₆ * y₁ - x₇ * y₄ + x₈ * y₃) ^ 2 +
        (x₁ * y₇ + x₂ * y₈ + x₃ * y₅ - x₄ * y₆ - x₅ * y₃ + x₆ * y₄ + x₇ * y₁ - x₈ * y₂) ^ 2 +
      (x₁ * y₈ - x₂ * y₇ + x₃ * y₆ + x₄ * y₅ - x₅ * y₄ - x₆ * y₃ + x₇ * y₂ + x₈ * y₁) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₁ : IsSumNonzeroSq s₁
h₂ : IsSumNonzeroSq s₂
⊢ IsSumNonzeroSq (s₁ + s₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s : R
h : IsSumNonzeroSq s
⊢ IsSumSq s

Tactic:
by

Goal state after: