mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: 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
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p : A[X]
⊢ d' ((aeval x) p) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p)) + (aeval x) (derivative p) • d' x

Tactic:
induction p using Polynomial.induction_on' with
  | add => simp_all only [map_add, add_smul]; abel
  | monomial =>
    simp only [aeval_monomial, leibniz, leibniz_pow, mapCoeffs_monomial,
      PolynomialModule.map_single, PolynomialModule.eval_single, derivative_monomial, map_mul,
      _root_.map_natCast, h]
    rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]

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

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < 0 ↔ p.degree < q.degree

Tactic:
simp only [hq, degree_zero, not_lt_bot, (pow_pos _).not_gt]

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_1
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
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
a✝ : M
⊢ ∀ ⦃b : M⦄, a✝ < b → (LinearMap.codRestrict ⊤ LinearMap.id ⋯) a✝ < (LinearMap.codRestrict ⊤ LinearMap.id ⋯) b

Tactic:
_

Goal state after:
case refine_1
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
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
a✝ b✝ : M
⊢ a✝ < b✝ → (LinearMap.codRestrict ⊤ LinearMap.id ⋯) a✝ < (LinearMap.codRestrict ⊤ LinearMap.id ⋯) b✝
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ p.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
rw [← one_mul (p.coeff i), ← one_pow p.natDegree]

Goal state after:
case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ 1 ^ deg(p) * p.coeff i ∈ Mq ^ deg(p) * Mp
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ ((monomial n) a).mirror = (monomial n) a

Tactic:
rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ (MvPolynomial.monomial ((fun₀ | 0 => m) + fun₀ | 1 => n - m)) 1 = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)

Tactic:
MvPolynomial.monomial_single_add,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ MvPolynomial.X 0 ^ m * (MvPolynomial.monomial fun₀ | 1 => n - m) 1 = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ ∃ q r,
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
Finset.coe_cons,

Goal state after:
case cons
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (insert i ↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ ∃ q r,
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case hq
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
hp : p = 0
⊢ False

Tactic:
exact p0 hp

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h : Multiset.countP (fun x ↦ 0 < x) ((X - C η) * Q).roots = n✝ + 1
hp : (X - C η) * Q ≠ 0
η_root : η ∈ ((X - C η) * Q).roots
⊢ Multiset.countP (fun x ↦ 0 < x) Q.roots = n✝

Tactic:
simp [← h, roots_mul (ne_zero_of_mem_roots η_root), η_pos, ← Nat.succ.injEq]

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

Goal state before:
pp: R : Type u
a₁✝ : NonUnitalNonAssocSemiring R
⊢ ∀ ⦃a₂ : NonUnitalNonAssocSemiring R⦄, a₁✝.toDistrib = a₂.toDistrib → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
⊢ a₁✝.toDistrib = a₂✝.toDistrib → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ : NonAssocSemiring R
⊢ ∀ ⦃a₂ : NonAssocSemiring R⦄, a₁✝.toNonUnitalNonAssocSemiring = a₂.toNonUnitalNonAssocSemiring → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
⊢ a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
⊢ a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring → a₁✝ = a₂✝

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
a✝ : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

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

Tactic:
by
  intro _ _ _
  ext <;> congr

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

Goal state before:
pp: R : Type u
a₁✝ : NonUnitalNonAssocRing R
⊢ ∀ ⦃a₂ : NonUnitalNonAssocRing R⦄, a₁✝.toNonUnitalNonAssocSemiring = a₂.toNonUnitalNonAssocSemiring → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
⊢ a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ : NonUnitalRing R
⊢ ∀ ⦃a₂ : NonUnitalRing R⦄, a₁✝.toNonUnitalSemiring = a₂.toNonUnitalSemiring → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
⊢ a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ : NonUnitalRing R
⊢ ∀ ⦃a₂ : NonUnitalRing R⦄, a₁✝.toNonUnitalNonAssocRing = a₂.toNonUnitalNonAssocRing → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
⊢ a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonUnitalRing R
⊢ a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing → a₁✝ = a₂✝

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

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

Tactic:
by
  intro _ _ _
  ext <;> congr

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

Goal state before:
pp: R : Type u
a₁✝ : NonAssocRing R
⊢ ∀ ⦃a₂ : NonAssocRing R⦄, a₁✝.toNonAssocSemiring = a₂.toNonAssocSemiring → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonAssocRing R
⊢ a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ : NonAssocRing R
⊢ ∀ ⦃a₂ : NonAssocRing R⦄, a₁✝.toNonUnitalNonAssocRing = a₂.toNonUnitalNonAssocRing → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonAssocRing R
⊢ a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonAssocRing R
⊢ a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing → a₁✝ = a₂✝

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : NonAssocRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ : Semiring R
⊢ ∀ ⦃a₂ : Semiring R⦄, a₁✝.toNonUnitalSemiring = a₂.toNonUnitalSemiring → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : Semiring R
⊢ a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ : Semiring R
⊢ ∀ ⦃a₂ : Semiring R⦄, a₁✝.toNonAssocSemiring = a₂.toNonAssocSemiring → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : Semiring R
⊢ a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ : Ring R
⊢ ∀ ⦃a₂ : Ring R⦄, toNonUnitalRing = toNonUnitalRing → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : Ring R
⊢ toNonUnitalRing = toNonUnitalRing → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ : Ring R
⊢ ∀ ⦃a₂ : Ring R⦄, toNonAssocRing = toNonAssocRing → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : Ring R
⊢ toNonAssocRing = toNonAssocRing → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ : Ring R
⊢ ∀ ⦃a₂ : Ring R⦄, a₁✝.toSemiring = a₂.toSemiring → a₁✝ = a₂

Tactic:
_

Goal state after:
R : Type u
a₁✝ a₂✝ : Ring R
⊢ a₁✝.toSemiring = a₂✝.toSemiring → a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ eval₂ (algebraMap (↥R) L) x (int R P hP) = (aeval x) P

Tactic:
rw [aeval_eq_sum_range, eval₂_eq_sum_range]

Goal state after:
K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ ∑ i ∈ Finset.range ((int R P hP).natDegree + 1), (algebraMap (↥R) L) ((int R P hP).coeff i) * x ^ i =
    ∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i • x ^ i
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel.trans
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
a b x✝¹ y✝¹ : R
hab : Rel r x✝¹ y✝¹
c d x✝ y✝ z✝ : R
a✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a✝ : Relation.EqvGen (Rel r) y✝ z✝
h : Relation.EqvGen (Rel r) (y✝¹ * x✝) (y✝¹ * y✝)
h' : Relation.EqvGen (Rel r) (y✝¹ * y✝) (y✝¹ * z✝)
⊢ Relation.EqvGen (Rel r) (y✝¹ * x✝) (y✝¹ * z✝)

Tactic:
exact h.trans _ _ _ h'

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl.trans
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
a b x✝¹ c d x✝ y✝ z✝ : R
a✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a✝ : Relation.EqvGen (Rel r) y✝ z✝
h : Relation.EqvGen (Rel r) (x✝¹ * x✝) (x✝¹ * y✝)
h' : Relation.EqvGen (Rel r) (x✝¹ * y✝) (x✝¹ * z✝)
⊢ Relation.EqvGen (Rel r) (x✝¹ * x✝) (x✝¹ * z✝)

Tactic:
exact h.trans _ _ _ h'

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel.trans
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
a b x✝¹ y✝¹ : R
hab : Rel r x✝¹ y✝¹
c d x✝ y✝ z✝ : R
a✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a✝ : Relation.EqvGen (Rel r) y✝ z✝
h : Relation.EqvGen (Rel r) (y✝¹ + x✝) (y✝¹ + y✝)
h' : Relation.EqvGen (Rel r) (y✝¹ + y✝) (y✝¹ + z✝)
⊢ Relation.EqvGen (Rel r) (y✝¹ + x✝) (y✝¹ + z✝)

Tactic:
exact h.trans _ _ _ h'

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl.trans
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
a b x✝¹ c d x✝ y✝ z✝ : R
a✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a✝ : Relation.EqvGen (Rel r) y✝ z✝
h : Relation.EqvGen (Rel r) (x✝¹ + x✝) (x✝¹ + y✝)
h' : Relation.EqvGen (Rel r) (x✝¹ + y✝) (x✝¹ + z✝)
⊢ Relation.EqvGen (Rel r) (x✝¹ + x✝) (x✝¹ + z✝)

Tactic:
exact h.trans _ _ _ h'

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mul_left
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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
x : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
r' : f a✝¹ = f b✝
⊢ f (a✝¹ * c✝) = f (b✝ * c✝)

Tactic:
rw [map_mul, map_mul, r']

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mul_right
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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
x : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
r' : f b✝ = f c✝
⊢ f (a✝¹ * b✝) = f (a✝¹ * c✝)

Tactic:
rw [map_mul, map_mul, r']

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_3
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 uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a b : B
⊢ a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
    b ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
      (mkRingHom r) a = 0 → (mkRingHom r) b = 0 → (mkRingHom r) (a + b) = 0

Tactic:
_

Goal state after:
case refine_3
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 uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a b : B
hx✝ : a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
⊢ b ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
    (mkRingHom r) a = 0 → (mkRingHom r) b = 0 → (mkRingHom r) (a + b) = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_3
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 uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a b : B
hx✝ : a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
⊢ b ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
    (mkRingHom r) a = 0 → (mkRingHom r) b = 0 → (mkRingHom r) (a + b) = 0

Tactic:
_

Goal state after:
case refine_3
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 uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a b : B
hx✝ : a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
hy✝ : b ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
⊢ (mkRingHom r) a = 0 → (mkRingHom r) b = 0 → (mkRingHom r) (a + b) = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_4
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 uR
inst✝ : CommRing B
r : B → B → Prop
x✝ : B
h : x✝ ∈ Ideal.ofRel r
a x : B
⊢ x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} → (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0

Tactic:
_

Goal state after:
case refine_4
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 uR
inst✝ : CommRing B
r : B → B → Prop
x✝ : B
h : x✝ ∈ Ideal.ofRel r
a x : B
hx✝ : x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
⊢ (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ C a * X = (monomial 1) a

Tactic:
by
  rw [← C_mul_X_pow_eq_monomial, pow_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
x✝ : ℕ
⊢ x✝ ∈ s → x✝ ∉ p.support → f x✝ (p.coeff x✝) = 0

Tactic:
_

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
x✝ : ℕ
a✝ : x✝ ∈ s
⊢ x✝ ∉ p.support → f x✝ (p.coeff x✝) = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ ↑f (a.coeff y * y • b.coeff x) * g (y * x) = ↑f (a.coeff y) * g y * (↑f (b.coeff x) * g x)

Tactic:
simp only [AddMonoidHom.coe_coe, map_mul]

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ f (a.coeff y) * f (y • b.coeff x) * (g y * g x) = f (a.coeff y) * g y * (f (b.coeff x) * g x)
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
⊢ ↑u = y • ↑v

Tactic:
simpa [← mul_assoc] using congr(v * $h).symm

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ untrop (trop (max (untrop a) (untrop b))) = untrop (if a ≤ b then b else a)

Tactic:
simp only [max_def, untrop_le_iff, untrop_trop]

Goal state after:
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoid R
l : List R
⊢ trop l.sum = (map trop l).prod

Tactic:
by
  induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoid R
l : List (Tropical R)
⊢ untrop l.prod = (map untrop l).sum

Tactic:
by
  induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ∀ (x : G), ¬g' = x * g
⊢ (x * single g r).coeff g' = 0

Tactic:
by
  classical
  simp only [coeff_mul, smul_zero, mul_zero, ite_self, sum_single_index]
  apply Finset.sum_eq_zero
  simp_rw [ite_eq_right_iff]
  rintro _ _ rfl
  exact False.elim (h _ rfl)

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 *
      (⅟2 * (unsym a * (unsym b * unsym (a * a) + unsym (a * a) * unsym b)) +
        ⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)

Tactic:
mul_assoc (⅟2) _ (unsym a),

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 *
      (⅟2 * (unsym a * (unsym b * unsym (a * a) + unsym (a * a) * unsym b)) +
        ⅟2 * ((unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a))
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
this : (liftNC ↑f ⇑g).comp ((smulAddHom k (SkewMonoidAlgebra k G)) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
simpa using congr($this φ)

Goal state after: