mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
⊢ StrictMono ↑(f.extendFun hx)

Tactic:
intro y

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y : ↥(f.extendFun hx).domain
⊢ ∀ ⦃b : ↥(f.extendFun hx).domain⦄, y < b → ↑(f.extendFun hx) y < ↑(f.extendFun hx) b
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hy : 0 < mk y
⊢ stdPart (x + y) = stdPart x

Tactic:
rw [add_comm, stdPart_add_eq_right hy]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : P.natDegree = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
rw [eq_C_of_natDegree_eq_zero hdp] at h ⊢
    simp [coeffList_C (C_ne_zero.mp h)]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
⊢ evalEval x y 0 = 0

Tactic:
by
  simp only [evalEval, eval_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
p : R[X][Y]
⊢ eval₂ (evalRingHom x) y p = evalEval x y p

Tactic:
eval₂_evalRingHom

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x y : R
p : R[X][Y]
⊢ evalEval x y p = evalEval x y p
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p.eraseLead + C p.leadingCoeff * X ^ p.natDegree = X ^ n + p.eraseLead

Tactic:
rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n m : ℕ
hm✝ : n ≤ m
a✝ : Nontrivial R
hm : n < m
hp : p.natDegree < m
hq : q.natDegree < m
⊢ p.coeff m = q.coeff m

Tactic:
coeff_eq_zero_of_natDegree_lt hp,

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n m : ℕ
hm✝ : n ≤ m
a✝ : Nontrivial R
hm : n < m
hp : p.natDegree < m
hq : q.natDegree < m
⊢ 0 = q.coeff m
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : R[X][Y]
h : Polynomial.evalEval x y p = 0
g : R[X][Y]
⊢ eval₂ (evalRingHom x) y g = Polynomial.evalEval x y g

Tactic:
eval₂_evalRingHom

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
p : R[X][Y]
h : Polynomial.evalEval x y p = 0
g : R[X][Y]
⊢ Polynomial.evalEval x y g = Polynomial.evalEval x y g
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
by
  by_cases hp : p = 0
  · rw [hp, zero_mul, natDegree_zero, mul_zero]
  rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬n = 0
⊢ ∑ i ∈ Finset.range n, (monomial i) (((ofFn n) v).coeff i) = ∑ i, (monomial ↑i) (v i)

Tactic:
simp [Finset.sum_range]

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

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
h : f (p * p.mirror) = f (q * q.mirror)
⊢ q = p ∨ q = p.mirror

Tactic:
replace h := (irreducible_aux1 hkm hmn u v w hp).trans h

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
h : C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = f (q * q.mirror)
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
⊢ q = p ∨ q = p.mirror

Tactic:
have hmul := congr_arg leadingCoeff h

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : (p * p.mirror).leadingCoeff = (q * q.mirror).leadingCoeff
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inl
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑w * ↑u
⊢ q = p ∨ q = p.mirror

pp: case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n ↑w ↑v ↑u
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror

Tactic:
· exact irreducible_aux2 hkm hmn hkm' hmn' u v w hp hq h

Goal state after:
case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n ↑w ↑v ↑u
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
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
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
x✝ : j ∈ Finset.univ
⊢ (r i j).degree + ↑(↑j * (g i).natDegree) < (g i ^ n i).degree

Tactic:
degree_eq_natDegree ((hg i hi).pow (n i)).ne_zero,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
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
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
x✝ : j ∈ Finset.univ
⊢ (r i j).degree + ↑(↑j * (g i).natDegree) < ↑(g i ^ n i).natDegree
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
h₁ : P.nextCoeff ≠ 0
this✝ : P.signVariations = P.eraseLead.signVariations + 1
this : SignType.sign ((X - C η) * P).nextCoeff = -1
⊢ ((X - C η) * P).eraseLead.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
simp +decide [signVariations_eq_eraseLead_add_ite h_mul, h_lC,
          leadingCoeff_eraseLead_eq_nextCoeff, ← sign_eq_zero_iff, this]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
rw [left_cancel]

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case a
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]

pp: case a
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₃
⊢ R[B.i, B.j, B.k] ≤ B.liftHom.range

Tactic:
· rintro x ⟨y, rfl⟩
    refine add_mem (add_mem (add_mem ?_ ?_) ?_) ?_
    · exact algebraMap_mem _ _
    all_goals
      exact Subalgebra.smul_mem _ (Algebra.subset_adjoin <| by simp) _

Goal state after:
case a
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₃
⊢ R[B.i, B.j, B.k] ≤ B.liftHom.range
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)
⊢ (gi i * (algebraMap R[X] K) (g i)) ^ n i * (algebraMap R[X] K) (g i) ^ ↑j = (algebraMap R[X] K) (g i) ^ ↑j

Tactic:
hgi i hi,

Goal state after:
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)
⊢ 1 ^ n i * (algebraMap R[X] K) (g i) ^ ↑j = (algebraMap R[X] K) (g i) ^ ↑j
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
rcases eq_or_ne a 0 with (rfl | ne_a)

Goal state after:
case sq_add.inl
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : 0 * 0 + s ≠ 0
⊢ IsSumNonzeroSq (0 * 0 + s)

case sq_add.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
G' : Type u_4
G'' : Type u_5
f : G ≃ G'
g : G' ≃ G''
l : SkewMonoidAlgebra k G
⊢ equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)

Tactic:
ext x; rfl

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
l : SkewMonoidAlgebra k G
⊢ equivMapDomain (Equiv.refl G) l = l

Tactic:
ext x; rfl

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝¹ : DecidableEq G'
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
⊢ (f.sum g).support ⊆ f.support.biUnion fun a ↦ (g a (f.coeff a)).support

Tactic:
simp_rw [support, coeff_sum']
  apply Finsupp.support_sum

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
i₁ : 0 ≤ P
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2

Tactic:
apply le_of_sub_nonneg

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := ⋯
i₁ : 0 ≤ P
⊢ 0 ≤ 2 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Tactic:
apply le_of_sub_nonneg

Goal state after:
R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := ⋯
Q : R := ⋯
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ 0 ≤ √2 ^ 3 • 1 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X * p = (p.sum fun a b ↦ (monomial a) (φ b)) * X

Tactic:
simp only [X, mul_def]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (((monomial 1) 1).sum fun a₁ b₁ ↦ p.sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)) =
    (p.sum fun a b ↦ (monomial a) (φ b)).sum fun a₁ b₁ ↦
      ((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ f * (g + h) = f * g + f * h

Tactic:
classical
    simp only [mul_def]
    refine Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_add_index ?_ ?_)) ?_ <;>
      simp only [smul_zero, smul_add, mul_add, mul_zero, single_zero, single_add,
        forall_true_iff, sum_add]

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ ∅, f i) = sInf (untrop ∘ f '' ↑∅)

Tactic:
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
⊢ coeff A n = ncoeff A (-n - 1)

Tactic:
ncoeff_apply,

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
⊢ coeff A n = coeff A (-(-n - 1) - 1)
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
n : ℤ
v : V
⊢ (ncoeff (of_coeff f hf) n) v = (f (-n - 1)) v

Tactic:
ncoeff_apply,

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
n : ℤ
v : V
⊢ (coeff (of_coeff f hf) (-n - 1)) v = (f (-n - 1)) v
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: case refine_1
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ (star (toConv ↑f.ofConv)).ofConv ∘ₗ (star (toConv ↑f.ofConv⁻¹)).ofConv = 1

Tactic:
← toConv_injective.eq_iff,

Goal state after:
case refine_1
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ toConv ((star (toConv ↑f.ofConv)).ofConv ∘ₗ (star (toConv ↑f.ofConv⁻¹)).ofConv) = toConv 1
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ (star (toConv ↑f.ofConv⁻¹)).ofConv ∘ₗ (star (toConv ↑f.ofConv)).ofConv = 1

Tactic:
← toConv_injective.eq_iff,

Goal state after:
case refine_2
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ toConv ((star (toConv ↑f.ofConv⁻¹)).ofConv ∘ₗ (star (toConv ↑f.ofConv)).ofConv) = toConv 1
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
β : X.Hom Y
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ (Presheaf.pushforward C base✝).obj X.presheaf
w : { base := base✝, c := c✝ }.base = β.base
h : { base := base✝, c := c✝ }.c ≍ β.c
⊢ { base := base✝, c := c✝ } = β

Tactic:
cases β

Goal state after:
case mk.mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base✝¹ : ↑X ⟶ ↑Y
c✝¹ : Y.presheaf ⟶ (Presheaf.pushforward C base✝¹).obj X.presheaf
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ (Presheaf.pushforward C base✝).obj X.presheaf
w : { base := base✝¹, c := c✝¹ }.base = { base := base✝, c := c✝ }.base
h : { base := base✝¹, c := c✝¹ }.c ≍ { base := base✝, c := c✝ }.c
⊢ { base := base✝¹, c := c✝¹ } = { base := base✝, c := c✝ }
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
U✝ : TopCat
X : PresheafedSpace C
f✝ : U✝ ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f✝)
U V : (Opens ↑↑X)ᵒᵖ
f : U ⟶ V
⊢ X.presheaf.map f ≫ X.presheaf.map (⋯.adjunction.counit.app (unop V)).op =
    X.presheaf.map (⋯.adjunction.counit.app (unop U)).op ≫ X.presheaf.map (h.functor.op.map ((Opens.map f✝).op.map f))

Tactic:
rw [← map_comp, ← map_comp]
          rfl

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
⊢ V.carrier ⊆ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}

Tactic:
intro y

Goal state after:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
y : ↑↑X.toPresheafedSpace
⊢ y ∈ V.carrier → y ∈ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case h
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
t : m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)
U : (Opens ↑↑s.pt)ᵒᵖ
j : Jᵒᵖ
⊢ (m.c ≫ whiskerRight (eqToHom ⋯) (colimitCocone F).pt.presheaf).app U ≫
      (limit.π (pushforwardDiagramToColimit F).leftOp j).app ((Opens.map (desc F s).base).op.obj U) =
    (desc F s).c.app U ≫ (limit.π (pushforwardDiagramToColimit F).leftOp j).app ((Opens.map (desc F s).base).op.obj U)

Tactic:
simp [desc, descCApp,
        PresheafedSpace.congr_app (w (unop j)).symm U,
        NatTrans.congr (limit.π (pushforwardDiagramToColimit F).leftOp j)
        (congr_arg op (Functor.congr_obj (congr_arg Opens.map t) (unop U)))]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCatᵒᵖ
⊢ locallyRingedSpaceMap (𝟙 (unop R)) = 𝟙 (locallyRingedSpaceObj (unop R))

Tactic:
Spec.locallyRingedSpaceMap_id

Goal state after:
R : CommRingCatᵒᵖ
⊢ 𝟙 (locallyRingedSpaceObj (unop R)) = 𝟙 (locallyRingedSpaceObj (unop R))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ app (inv f) U ≫ app f (inv f ⁻¹ᵁ U) = X.presheaf.map (eqToHom ⋯).op

Tactic:
← comp_app,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ app (f ≫ inv f) U = X.presheaf.map (eqToHom ⋯).op
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
inst✝ : SheafedSpace.IsOpenImmersion f
⊢ toSheafedSpace Y f.hom = X

Tactic:
by cases X; rfl

Goal state after: