mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₁ x) ≤ f₂.sum h

Tactic:
sum_of_support_subset _ Finset.subset_union_right _ hh₀

Goal state after:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₁ x) ≤ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₂ x)
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
A : Type z
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
f : R[X]
G : Type u_3
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G R A
g : G
x : A
⊢ (aeval ((MulSemiringAction.toAlgHom R A g) x)) f = g • (aeval x) f

Tactic:
aeval_algHom_apply,

Goal state after:
R : Type u
A : Type z
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
f : R[X]
G : Type u_3
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G R A
g : G
x : A
⊢ (MulSemiringAction.toAlgHom R A g) ((aeval x) f) = g • (aeval x) f
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: S : Type v
A' : Type u_1
inst✝² : CommSemiring A'
inst✝¹ : CommSemiring S
inst✝ : Algebra S A'
⊢ aevalTower (Algebra.ofId S A') = aeval

Tactic:
ext
  simp only [aeval_X, aevalTower_X]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f i < f j
⊢ toColex (f ∘ ⇑(Equiv.swap i j)) < toColex f

Tactic:
rw [Equiv.swap_comm]
  exact lex_desc (ι := ιᵒᵈ) h₁ h₂

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ ((aeval f) p) v = p.sum fun n b ↦ b • (f ^ n) v

Tactic:
rw [aeval_def, eval₂_eq_sum]
  exact map_sum (LinearMap.applyₗ v) _ _

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

Goal state before:
pp: case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support → b ≠ 0 → motive ((monomial f) a) → motive ((monomial (Finsupp.single a_1 b + f)) a)

Tactic:
· intro n e p _hpn _he ih
    have : ∀ e : ℕ, motive (monomial p a * X n ^ e) := by
      intro e
      induction e with
      | zero => simp [ih]
      | succ e e_ih => simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]
    simp [add_comm, monomial_add_single, this]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : MvPolynomial σ R →ₐ[R] A
hf : ∀ (i : σ), f (X i) = g (X i)
⊢ f.comp singleZeroAlgHom = g.comp singleZeroAlgHom

Tactic:
by ext

Goal state after:
Module: Mathlib.Data.Finsupp.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (fun a ↦ toLex (single a 1)) b < (fun a ↦ toLex (single a 1)) a

Tactic:
simp only [LT.lt, Finsupp.lex_def]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ j,
    (∀ d < j, (ofLex (toLex (single b 1))) d = (ofLex (toLex (single a 1))) d) ∧
      ((ofLex (toLex (single b 1))) j).lt ((ofLex (toLex (single a 1))) j)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h : (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) q
d : σ →₀ ℕ
h' : a * coeff d p = a * coeff d q
⊢ a * coeff d p = a * coeff d q

Tactic:
h'

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h : (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) q
d : σ →₀ ℕ
h' : a * coeff d p = a * coeff d q
⊢ a * coeff d q = a * coeff d q
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
⊢ (monomial i) x ∈ coeffsIn σ M ↔ x ∈ M

Tactic:
classical
  simp only [mem_coeffsIn, coeff_monomial]
  exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case monomial_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
ih : ((map f) ((monomial a) s)).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs
⊢ Disjoint ((map f) ((monomial a) s)).support ((map f) p).support

Tactic:
· exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: σ : Type u_1
S : Type u_2
A : Type u_3
inst✝² : CommSemiring S
inst✝¹ : CommSemiring A
inst✝ : Algebra S A
⊢ aevalTower (Algebra.ofId S A) = aeval

Tactic:
ext
  simp only [aeval_X, aevalTower_X]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = p.support.sup fun m ↦ (toMultiset m).card

Tactic:
by
  rw [totalDegree]
  congr; funext m
  exact (Finsupp.card_toMultiset _).symm

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case pos.a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p.support, i ∈ d.support

Tactic:
exact ⟨d, hd, hi⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg.h₀.a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p.support, i ∈ d.support

Tactic:
exact ⟨d, hd, hi⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p₁.support, i ∈ d.support

Tactic:
exact ⟨d, hd, hi⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ (aeval fun i ↦ if i ∈ s then X i else 0) ((monomial u) (coeff u q)) = (monomial u) (coeff u q)

Tactic:
rw [MvPolynomial.aeval_monomial, MvPolynomial.monomial_eq]

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ ((algebraMap R (MvPolynomial σ R)) (coeff u q) * u.prod fun i k ↦ (if i ∈ s then X i else 0) ^ k) =
    C (coeff u q) * u.prod fun n e ↦ X n ^ e
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (↑n).natTrailingDegree = 0

Tactic:
simp only [← C_eq_natCast, natTrailingDegree_C]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ∈ f.eraseLead.support
⊢ a < f.natDegree

Tactic:
rw [eraseLead_support, mem_erase] at h

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ≠ f.natDegree ∧ a ∈ f.support
⊢ a < f.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0

Tactic:
case =>

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1

Tactic:
case =>

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : f = 0
⊢ #f.support ≤ 1

Tactic:
case =>

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Tactic:
case =>

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : r = 0
⊢ ((monomial i) r).eraseLead = 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).eraseLead = 0

Tactic:
· subst r
    simp only [monomial_zero_right, eraseLead_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).eraseLead = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N n✝ : ℕ
⊢ (reflect N (C r * f)).coeff n✝ = (C r * reflect N f).coeff n✝

Tactic:
simp only [coeff_reflect, coeff_C_mul]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
⊢ (p.comp q).degree = p.degree * q.degree

Tactic:
rcases eq_or_ne p 0 with rfl | hp
  · rw [zero_comp, degree_zero, WithBot.bot_mul']
    simp [hq.ne']
  rw [degree_eq_natDegree hp, degree_eq_natDegree (ne_zero_of_degree_gt hq), ← Nat.cast_mul,
    ← natDegree_comp]
  apply degree_eq_natDegree
  simp_rw [Ne, comp_eq_zero_iff, hp, false_or, not_and_or, ← degree_le_zero_iff]
  simp [hq]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
⊢ (p * q).degree = (q * p).degree

Tactic:
by
  by_cases h : q = 0
  · simp [h]
  rw [degree_mul', hp.degree_mul]
  · exact add_comm _ _
  · rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ ∑ i ∈ range (n + 2), 0 ^ i = if n + 2 = 0 then 0 else 1

Tactic:
geom_sum_succ'

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ 0 ^ (n + 1) + ∑ i ∈ range (n + 1), 0 ^ i = if n + 2 = 0 then 0 else 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ (f * g).natDegree)

Tactic:
rw [hf.natDegree_mul hg, add_le_add_iff_right]

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0
⊢ ¬(0 < g.natDegree ∧ g.natDegree ≤ f.natDegree)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → ¬(0 < g_1.natDegree ∧ g_1.natDegree + g_1.natDegree ≤ (f * g).natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
· simp_rw [hf.natDegree_mul hg, pos_iff_ne_zero] at h
    contrapose! h
    obtain hl | hl := le_total f.natDegree g.natDegree
    · exact ⟨g, f, hg, hf, mul_comm g f, h.1, by gcongr⟩
    · exact ⟨f, g, hf, hg, rfl, h.2, by gcongr⟩

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

Goal state before:
pp: case inr.mpr.refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₁) * (X + C c₂) = C c₁ * C c₂ * X ^ 0 + C (c₁ + c₂) * X ^ 1 + C 1 * X ^ 2

Tactic:
C_add,

Goal state after:
case inr.mpr.refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₁) * (X + C c₂) = C c₁ * C c₂ * X ^ 0 + (C c₁ + C c₂) * X ^ 1 + C 1 * X ^ 2
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ (∑ i ∈ range n.succ, P ^ i).Monic

Tactic:
geom_sum_succ'

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ (P ^ n + ∑ i ∈ range n, P ^ i).Monic
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
S : Subalgebra R A
⊢ P S

Tactic:
by
  classical
  obtain ⟨t, rfl⟩ := S.fg_of_noetherian
  refine Finset.induction_on t ?_ ?_
  · simpa using base
  intro x t _ h
  rw [Finset.coe_insert]
  simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A → ∃ s f, Surjective ⇑f

Tactic:
rintro ⟨s, hs⟩
    refine ⟨s, FreeAlgebra.lift _ (↑), ?_⟩
    rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift,
      Subtype.range_coe_subtype, Finset.setOfPred_mem, hs, coe_top]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : ¬r = 0
⊢ Unitization.inl r = -↑a

Tactic:
· exact (h r hr <| hx ▸ (neg_mem a.property)).elim

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ Star.star x ∈ s ∪ Star.star s

Tactic:
by simpa using Or.inl hx

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

pp: case refine_2
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
· exact (isPeriodicPt_minimalPeriod _ _).const_mul _

Goal state after:
case refine_2
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ (y :: l ++ [x]).next x h = y

Tactic:
rw [next, nextOr_concat]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ (y :: l ++ [x]).get ⟨0, ⋯⟩ = y

case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ x ∉ y :: l
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
h : x ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝
⊢ x ∈ orbit (↥(H.subgroupOf K)) b✝

Tactic:
rcases h with ⟨⟨gv, gp⟩, rfl⟩
    simp only
    simp only [Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf] at gp
    refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)
    · exact gp.2
    · simp only [Subgroup.mem_subgroupOf]
      exact gp.1

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mp
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
p : ℕ
hle : p ≤ n
heq : n = p ^ k
hprime : Nat.Prime p
⊢ n = n.minFac ^ k

Tactic:
heq,

Goal state after:
case inr.mp
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
p : ℕ
hle : p ≤ n
heq : n = p ^ k
hprime : Nat.Prime p
⊢ p ^ k = (p ^ k).minFac ^ k
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)

Tactic:
rw [chain_coe_cons] at p ⊢

Goal state after:
case cons
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : IsChain r₁ (a✝¹ :: (l✝ ++ [a✝¹]))
⊢ IsChain r₂ (a✝¹ :: (l✝ ++ [a✝¹]))
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ x✝²⁻¹ * (x✝¹ * unop x✝³ * (unop x✝³)⁻¹) ∈ H

Tactic:
mul_inv_cancel_right

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ x✝²⁻¹ * x✝¹ ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x✝ : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
x : ↑(orbitRel.Quotient.orbit ω)
hx : ↑x ∈ orbitRel.Quotient.orbit ω
⊢ ⟦↑x⟧ = ω

Tactic:
orbitRel.Quotient.mem_orbit

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x✝ : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
x : ↑(orbitRel.Quotient.orbit ω)
hx : Quotient.mk'' ↑x = ω
⊢ ⟦↑x⟧ = ω
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ∣ n

Tactic:
by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · exact dvd_zero p
  · rwa [← mem_primeFactorsList_iff_dvd hn.ne' (prime_of_mem_primeFactorsList h)]

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ≤ 0

pp: case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n

Tactic:
· rw [primeFactorsList_zero] at h
    cases h

Goal state after:
case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ a, ∀ (b : G), (a * b ∈ H ∨ b ∈ H) ∧ ¬(a * b ∈ H ∧ b ∈ H)) ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H

Tactic:
exact exists_congr fun a ↦ ⟨fun h ↦ ⟨fun ha ↦ ((h a)).2 ⟨mul_mem ha ha, ha⟩, fun b ↦ (h b).1⟩,
    fun h b ↦ ⟨h.2 b, fun h' ↦ h.1 (by simpa using mul_mem h'.1 (inv_mem h'.2))⟩⟩

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ ↑⟨x, hx⟩ = ↑⟨y, hy⟩

Tactic:
exact f

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k a : ℕ
⊢ (∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range (k + 1))

Tactic:
simp [eq_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ ∑ i ∈ range n, x ^ i = 0 ↔ x = -1 ∧ Even n

Tactic:
refine ⟨fun h => ?_, @fun ⟨h, hn⟩ => by simp only [h, hn, neg_one_geom_sum, if_true]⟩
  contrapose! h
  have hx := eq_or_ne x (-1)
  rcases hx with hx | hx
  · rw [hx, neg_one_geom_sum]
    simp only [h hx, ite_false, ne_eq, one_ne_zero, not_false_eq_true]
  · exact geom_sum_ne_zero hx hn

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], -[a✝+1]) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (-[a✝¹+1], -[a✝+1]).1 * (-[a✝¹+1], -[a✝+1]).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

Tactic:
case =>

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a * ↑(unitOfCoprime 2 hn) = 0 ↔ a = 0

Tactic:
Units.mul_left_eq_zero

Goal state after:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a = 0 ↔ a = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ 0 < a.val ↔ a ≠ 0

Tactic:
by
  simp [pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
conv_lhs =>
    rw [← a.natCast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, natCast_eq_zero_iff]

Goal state after:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ n✝ + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n✝ + 1
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case2
p n : ℕ
h : ¬(1 < p ∧ n ≠ 0)
⊢ (0, n).snd * p ^ (0, n).fst = n

Tactic:
| case2 h =>

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
simp only [h, List.append_nil] at h_append ⊢
      exact getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
n : ℕ
hn1 : n < m
hn2 : ¬a ^ (n + 1) ∣ b
⊢ False

Tactic:
exact hn2 ((pow_dvd_pow _ hn1).trans nh)

Goal state after: