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
c : FiniteArchimedeanClass M
y' : M
hy' : y' ∈ (f.extendFun hx).domain
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(f.extendFun hx) ⟨y', hy'⟩))) ∈ (f.extendFun hx).toFun.range

Tactic:
extendFun,

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
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ ((↑f).supSpanSingleton x (f.eval x) hx).domain
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(f.extendFun hx) ⟨y', hy'✝⟩))) ∈ (f.extendFun hx).toFun.range
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
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(f.extendFun hx) ⟨y', hy'✝⟩))) ∈ (f.extendFun hx).toFun.range

Tactic:
extendFun,

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
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑((↑f).supSpanSingleton x (f.eval x) hx) ⟨y', hy'✝⟩))) ∈
    ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
q : A[X]
n : ℕ
a : A
⊢ (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a * q)) =
    (monomial n) a • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q) +
      q • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a))

Tactic:
induction q using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
x y : R
⊢ evalEval (f x) (f y) (map (mapRingHom f) p) = f (evalEval x y p)

Tactic:
by
  rw [evalEval, ← map_mapRingHom_eval_map_eval, map_C]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
x✝ : p.natDegree ≤ n ∧ p.coeff n = 1
H₁ : p.natDegree ≤ n
H₂ : p.coeff n = 1
⊢ p.Monic

Tactic:
exact monic_of_natDegree_le_of_coeff_eq_one n H₁ H₂

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b ^ N * eval (i a * bf) (Polynomial.map i f) + i Dg =
    i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)

Tactic:
Hg

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bg) (Polynomial.map i g) =
    i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
⊢ (p + q).homogenize n = p.homogenize n + q.homogenize n

Tactic:
simp [homogenize, Finset.sum_add_distrib]

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
hxy : x ≠ y
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup

Tactic:
simp only [mem_cons, forall_eq_or_imp, pairwise_cons] at h

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
⊢ ∀ (n : ℕ), q.smeval ↑n = ↑(q.smeval n)

Tactic:
induction q using Polynomial.induction_on' with

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

Goal state before:
pp: p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3

Tactic:
natDegree_mul_mirror,

Goal state after:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p * p.mirror).coeff ((2 * p.natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3
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
hmul :
  (trinomial k m n ↑u ↑v ↑w).leadingCoeff * (trinomial k m n ↑u ↑v ↑w).trailingCoeff =
    (trinomial k m' n ↑x ↑v ↑z).leadingCoeff * (trinomial k m' n ↑x ↑v ↑z).trailingCoeff
⊢ q = p ∨ q = p.mirror

Tactic:
trinomial_leadingCoeff hkm hmn w.ne_zero,

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 :
  ↑w * (trinomial k m n ↑u ↑v ↑w).trailingCoeff =
    (trinomial k m' n ↑x ↑v ↑z).leadingCoeff * (trinomial k m' n ↑x ↑v ↑z).trailingCoeff
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ (q * q.mirror).natDegree = 2 * n'

Tactic:
natDegree_mul_mirror,

Goal state after:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ 2 * q.natDegree = 2 * n'
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

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

Tactic:
rcases irreducible_aux3 hkm hmn hkm' hmn' u v w x z hp hq hpq with (h2 | h2)

Goal state after:
case inl.inl
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑v ↑z
h1 : ↑y = ↑v
h2 : q = p
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

case inl.inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑v ↑z
h1 : ↑y = ↑v
h2 : q = p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
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 * (q₁ - q₂) * ∏ x ∈ s, g x = 0
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
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
← mul_rotate,

Goal state after:
case cons
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 : (∏ x ∈ s, g x) * g i * (q₁ - q₂) = 0
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
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case mp
R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b)) r ∣ z → r ∣ z.re ∧ r ∣ z.im

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case mp
R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ r ∣ ((algebraMap R (QuadraticAlgebra R a b)) r * x).re ∧ r ∣ ((algebraMap R (QuadraticAlgebra R a b)) r * x).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : ¬norm z = 0
⊢ (norm z)⁻¹ • (z * star z) = 1

Tactic:
rw [← C_mul_eq_smul, C_eq_algebraMap, ← algebraMap_norm_eq_mul_star, ← map_mul,
      inv_mul_cancel₀ hz, map_one]

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
  -- Split into `AddMonoid` instance, `mul` function and properties.
  rcases inst₁ with @⟨_, ⟨⟩⟩
  rcases inst₂ with @⟨_, ⟨⟩⟩
  -- Prove equality of parts using already-proved extensionality lemmas.
  congr; ext : 1; assumption

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₁ = inst₂

Tactic:
by
  -- Show that enough substructures are equal.
  have h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid := by
    ext : 1 <;> assumption
  have h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring := by
    ext : 1 <;> assumption
  have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by
    ext : 1 <;> assumption
  have h₃ : (inst₁.toMonoidWithZero).toMonoid = (inst₂.toMonoidWithZero).toMonoid := by
    ext : 1; exact h_mul
  -- Split into fields and prove they are equal using the above.
  cases inst₁; cases inst₂
  congr <;> solve | injection h₁ | injection h₂

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

Goal state before:
pp: case refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS → T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

pp: case refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)
⊢ T ∈ (toEndRingHom α).rangeS

Tactic:
· rintro ⟨f, rfl⟩ S (⟨a, rfl⟩ | ⟨b, rfl⟩)
    · exact AddMonoidHom.ext fun b ↦ (map_mul_left f a b).symm
    · exact AddMonoidHom.ext fun a ↦ (map_mul_right f a b).symm

Goal state after:
case refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)
⊢ T ∈ (toEndRingHom α).rangeS
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
⊢ Quot.lift ⇑f ⋯ (toQuot 1) = 1

Tactic:
by simp only [← one_quot, map_one]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.coeff.sum fun x1 x2 ↦ (g x1 x2).coeff).sum h = f.sum fun a b ↦ (g a b).sum h

Tactic:
Finsupp.sum_sum_index h_zero h_add

Goal state after:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.coeff.sum fun a b ↦ (g a b).coeff.sum h) = f.sum fun a b ↦ (g a b).sum h
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ min (untrop x) (untrop y) = untrop x ↔ x ≤ y

Tactic:
← untrop_le_iff,

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ min (untrop x) (untrop y) = untrop x ↔ untrop x ≤ untrop y
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ min (untrop x) (untrop y) = untrop y ↔ y ≤ x

Tactic:
← untrop_le_iff,

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ min (untrop x) (untrop y) = untrop y ↔ untrop y ≤ untrop x
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
⊢ ∀ (m : R) (x : U),
    (of R) (A.compHahnSeries B (m • x)).ofIterate = (RingHom.id R) m • (of R) (A.compHahnSeries B x).ofIterate

Tactic:
intro r x

Goal state after:
Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
x : U
⊢ (of R) (A.compHahnSeries B (r • x)).ofIterate = (RingHom.id R) r • (of R) (A.compHahnSeries B x).ofIterate
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ (presheafToSheaf (Opens.grothendieckTopology ↑X) A).map
        (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝) ≫
          ((Functor.whiskeringLeft (Opens ↑X)ᵒᵖ (Opens ↑Y)ᵒᵖ A).obj ⋯.functor.op).map ((Sheaf.forget A Y).map u)) ≫
      ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝)) ≫
        ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv) ≫
      (sheafPullback A hf).map u

Tactic:
Sheaf.hom_ext_iff

Goal state after:
case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map
          (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝) ≫
            ((Functor.whiskeringLeft (Opens ↑X)ᵒᵖ (Opens ↑Y)ᵒᵖ A).obj ⋯.functor.op).map ((Sheaf.forget A Y).map u)) ≫
        ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv).hom =
    (((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝)) ≫
          ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv) ≫
        (sheafPullback A hf).map u).hom
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.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
⊢ fc = gc

Tactic:
ext U s

Goal state after:
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.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (fc.app (op U))) s = (ConcreteCategory.hom (gc.app (op U))) s
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ X.presheaf.stalk x = X.presheaf.stalk ((ConcreteCategory.hom (α ≫ β).base) x)

Tactic:
rw [h_eq]

Goal state after: