mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
hsc : (⇑SignType.sign ∘ fun x ↦ -x) = (fun x ↦ -x) ∘ ⇑SignType.sign
h_neg_destutter :
  ∀ (l : List SignType),
    List.map (fun x ↦ -x) (List.destutter (fun x1 x2 ↦ ¬x1 = x2) l) =
      List.destutter (fun x1 x2 ↦ ¬x1 = x2) (List.map (fun x ↦ -x) l)
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign ∘ fun x ↦ -x)
            (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign ∘ fun x ↦ -x) P.coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign) (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) P.coeffList))).length -
      1

Tactic:
rw [hsc, List.comp_map, ← h_neg_destutter, List.length_map]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
hsc : (⇑SignType.sign ∘ fun x ↦ -x) = (fun x ↦ -x) ∘ ⇑SignType.sign
h_neg_destutter :
  ∀ (l : List SignType),
    List.map (fun x ↦ -x) (List.destutter (fun x1 x2 ↦ ¬x1 = x2) l) =
      List.destutter (fun x1 x2 ↦ ¬x1 = x2) (List.map (fun x ↦ -x) l)
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (List.map (⇑SignType.sign)
            (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ (fun x ↦ -x) ∘ ⇑SignType.sign) P.coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign) (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
⊢ range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)

Tactic:
rw [range_eq_Ico, range_eq_Ico, Ico_union_Ico_eq_Ico hq.le]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
⊢ q ≤ p.natDegree + 1
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
j : ι
hj : j ∈ s
⊢ ((r₁ j - r₂ j) * ∏ k ∈ s.erase j, g k).degree < (∏ i ∈ s, g i).degree

Tactic:
← Finset.mul_prod_erase s g hj,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
j : ι
hj : j ∈ s
⊢ ((r₁ j - r₂ j) * ∏ k ∈ s.erase j, g k).degree < (g j * ∏ x ∈ s.erase j, g x).degree
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

Tactic:
intros

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x

Tactic:
intros

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

Tactic:
intros

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x

Tactic:
intros

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

Tactic:
intros

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x : QuadraticAlgebra R a b), (equivProd a b) (-x) = -(equivProd a b) x

Tactic:
intros

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (-x✝) = -(equivProd a b) x✝
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x - y) = (equivProd a b) x - (equivProd a b) y

Tactic:
intros

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ - y✝) = (equivProd a b) x✝ - (equivProd a b) y✝
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x

Tactic:
intros

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℤ), (equivProd a b) (n • x) = n • (equivProd a b) x

Tactic:
intros

Goal state after:
case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
n✝ : ℤ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case zero
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
ih : ∀ m < 0, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = 0
hcQ : 0 < P.coeff 0
hxcQ : ((X - C η) * P).coeff 1 = P.coeff 0
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
            (List.filter (fun x ↦ decide ¬x = 0)
              (List.map (⇑SignType.sign) (List.map P.coeff (List.range P.degree.succ).reverse)))).length -
        1 +
      1 ≤
    (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (List.filter (fun x ↦ decide ¬x = 0)
            (List.map (⇑SignType.sign)
              (List.map ((X - C η) * P).coeff (List.range ((X - C η) * P).degree.succ).reverse)))).length -
      1

Tactic:
withBotSucc_degree_eq_natDegree_add_one hP,

Goal state after:
case zero
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
ih : ∀ m < 0, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = 0
hcQ : 0 < P.coeff 0
hxcQ : ((X - C η) * P).coeff 1 = P.coeff 0
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
            (List.filter (fun x ↦ decide ¬x = 0)
              (List.map (⇑SignType.sign) (List.map P.coeff (List.range (P.natDegree + 1)).reverse)))).length -
        1 +
      1 ≤
    (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (List.filter (fun x ↦ decide ¬x = 0)
            (List.map (⇑SignType.sign)
              (List.map ((X - C η) * P).coeff (List.range ((X - C η) * P).degree.succ).reverse)))).length -
      1
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ { re := x, im := y } * star { re := x, im := y } =
    (algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x +
        (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x *
          (algebraMap R (QuadraticAlgebra R a b)) y -
      (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y *
        (algebraMap R (QuadraticAlgebra R a b)) y

Tactic:
by
  ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z - star z = z.im • (ω - star ω)

Tactic:
by
  ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃⁻¹ y = x ◃⁻¹ y

Tactic:
rw [← left_cancel (x ◃ x)]
  rw [right_inv]
  rw [self_act_act_eq]
  rw [right_inv]

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
⊢ 0 ∈ r • ↑t ↔ 0 ∈ t

Tactic:
Set.zero_mem_smul_set_iff hr,

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
⊢ 0 ∈ ↑t ↔ 0 ∈ t
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
⊢ s₁ = 0

Tactic:
by_contra! h₁
  have h₂ : s₂ ≠ 0 := fun hc ↦ by simp_all
  rw [← isSumNonzeroSq_iff_isSumSq h₁] at hs₁
  rw [← isSumNonzeroSq_iff_isSumSq h₂] at hs₂
  exact not_isSumNonzeroSq_zero (h ▸ IsSumNonzeroSq.add hs₁ hs₂)

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₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
⊢ star P = P

Tactic:
dsimp [P]

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 := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
⊢ star (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) = 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
⊢ x ∈ S ↔ x ∈ T

Tactic:
by rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
⊢ ∀ (r : R),
    MulOpposite.unop (y (MulOpposite.unop (y ((algebraMap R (FreeAlgebra R X)) r)))) =
      (algebraMap R (FreeAlgebra R X)) r

Tactic:
intros

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
r✝ : R
⊢ MulOpposite.unop (y (MulOpposite.unop (y ((algebraMap R (FreeAlgebra R X)) r✝)))) =
    (algebraMap R (FreeAlgebra R X)) r✝
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
z : ↥(StarSubsemiring.center α)
⊢ ↑((fun T ↦ ⟨T 1, ⋯⟩) (starCenterToCentroid.toFun z)) = ↑z

Tactic:
simp only [MulHom.toFun_eq_coe,
    NonUnitalRingHom.coe_toMulHom, NonUnitalStarRingHom.coe_toNonUnitalRingHom,
    starCenterToCentroid_apply, mul_one]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
⊢ ∀ (x : X), MulOpposite.unop (y (MulOpposite.unop (y (ι R x)))) = ι R x

Tactic:
intros

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
x✝ : X
⊢ MulOpposite.unop (y (MulOpposite.unop (y (ι R x✝)))) = ι R x✝
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
⊢ ∀ (a b : FreeAlgebra R X),
    MulOpposite.unop (y (MulOpposite.unop (y a))) = a →
      MulOpposite.unop (y (MulOpposite.unop (y b))) = b → MulOpposite.unop (y (MulOpposite.unop (y (a * b)))) = a * b

Tactic:
intros

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
a✝² b✝ : FreeAlgebra R X
a✝¹ : MulOpposite.unop (y (MulOpposite.unop (y a✝²))) = a✝²
a✝ : MulOpposite.unop (y (MulOpposite.unop (y b✝))) = b✝
⊢ MulOpposite.unop (y (MulOpposite.unop (y (a✝² * b✝)))) = a✝² * b✝
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
⊢ ∀ (a b : FreeAlgebra R X),
    MulOpposite.unop (y (MulOpposite.unop (y a))) = a →
      MulOpposite.unop (y (MulOpposite.unop (y b))) = b → MulOpposite.unop (y (MulOpposite.unop (y (a + b)))) = a + b

Tactic:
intros

Goal state after:
case refine_4
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
a✝² b✝ : FreeAlgebra R X
a✝¹ : MulOpposite.unop (y (MulOpposite.unop (y a✝²))) = a✝²
a✝ : MulOpposite.unop (y (MulOpposite.unop (y b✝))) = b✝
⊢ MulOpposite.unop (y (MulOpposite.unop (y (a✝² + b✝)))) = a✝² + b✝
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := ⋯
this : Mul R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

Tactic:
intros

Goal state after:
case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := e.star
this : Mul R := e.mul
x✝ : R
⊢ e (star x✝) = star (e x✝)
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := ⋯
this : Mul R := ⋯
⊢ ∀ (x y : R), e (x * y) = e x * e y

Tactic:
intros

Goal state after:
case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := e.star
this : Mul R := e.mul
x✝ y✝ : R
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := ⋯
this : AddMonoid R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

Tactic:
intros

Goal state after:
case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := e.star
this : AddMonoid R := e.addMonoid
x✝ : R
⊢ e (star x✝) = star (e x✝)
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := ⋯
this : AddMonoid R := ⋯
⊢ ∀ (x y : R), e (x + y) = e x + e y

Tactic:
intros

Goal state after:
case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := e.star
this : AddMonoid R := e.addMonoid
x✝ y✝ : R
⊢ e (x✝ + y✝) = e x✝ + e y✝
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := ⋯
this : NonUnitalNonAssocSemiring R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

Tactic:
intros

Goal state after:
case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := e.star
this : NonUnitalNonAssocSemiring R := e.nonUnitalNonAssocSemiring
x✝ : R
⊢ e (star x✝) = star (e x✝)
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := ⋯
this : NonUnitalNonAssocSemiring R := ⋯
⊢ ∀ (x y : R), e (x + y) = e x + e y

Tactic:
intros

Goal state after:
case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := e.star
this : NonUnitalNonAssocSemiring R := e.nonUnitalNonAssocSemiring
x✝ y✝ : R
⊢ e (x✝ + y✝) = e x✝ + e y✝
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := ⋯
this : NonUnitalNonAssocSemiring R := ⋯
⊢ ∀ (x y : R), e (x * y) = e x * e y

Tactic:
intros

Goal state after:
case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := e.star
this : NonUnitalNonAssocSemiring R := e.nonUnitalNonAssocSemiring
x✝ y✝ : R
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := ⋯
this : SMul 𝕜 R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

Tactic:
intros

Goal state after:
case star
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := e.star
this : SMul 𝕜 R := Equiv.smul 𝕜 e
x✝ : R
⊢ e (star x✝) = star (e x✝)
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case smul
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := ⋯
this : SMul 𝕜 R := ⋯
⊢ ∀ (r : 𝕜) (x : R), e (r • x) = r • e x

Tactic:
intros

Goal state after:
case smul
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := e.star
this : SMul 𝕜 R := Equiv.smul 𝕜 e
r✝ : 𝕜
x✝ : R
⊢ e (r✝ • x✝) = r✝ • e x✝
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ trop (s.inf f) = ∑ i ∈ s, trop (f i)

Tactic:
convert! Multiset.trop_inf (s.val.map f)
  simp only [Multiset.map_map, Function.comp_apply]
  rfl

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := h, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom g) y = (ConcreteCategory.hom h) y

Tactic:
rw [← (h₁ y).choose_spec]
    simpa using congr(($e).base.hom (h₁ y).choose)

Goal state after: