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

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ⇑((lift R) f) ∘ ι R = f

Tactic:
by
  ext
  rw [Function.comp_apply, ι_def, lift]
  rfl

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
⊢ p.comp (C a) = C (eval a p)

Tactic:
simp [comp]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n

Tactic:
exact fun e => e.symm ▸ d

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ p = q ↔ Nat.Prime p

Tactic:
exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp ‹CharP R q›⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
r : R
c' : R[M]
_nm : g ∉ c'.coeff.support
_nz : r ≠ 0
⊢ f (c' • v) = (RingHom.id R[M]) c' • f v → f ((single g r + c') • v) = (RingHom.id R[M]) (single g r + c') • f v

Tactic:
w

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
r : R
c' : R[M]
_nm : g ∉ c'.coeff.support
_nz : r ≠ 0
w : f (c' • v) = (RingHom.id R[M]) c' • f v
⊢ f ((single g r + c') • v) = (RingHom.id R[M]) (single g r + c') • f v
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∑ x ∈ antidiagonal (d + n), p.coeff x.1 * (X ^ n).coeff x.2 = p.coeff d

Tactic:
Finset.sum_eq_single (d, n),

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = p.coeff d

case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0

case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (p.update n a).coeff n✝ = (p + C (a - p.coeff n) * X ^ n).coeff n✝

Tactic:
coeff_update_apply,

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (if n✝ = n then a else p.coeff n✝) = (p + C (a - p.coeff n) * X ^ n).coeff n✝
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : 0 ≠ 1
p : R[X]
hp : p.Monic
⊢ p ≠ 0

Tactic:
by
  nontriviality R
  exact hp.ne_zero

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

Goal state before:
pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 0 ↔ ↑a✝ = 0 ∧ m = 0

Tactic:
cases m

Goal state after:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 0 ↔ ↑a✝ = 0 ∧ ⊥ = 0

case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 0 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 1 ↔ ↑a✝ = 0 ∧ m = 1 ∨ ↑a✝ = 1 ∧ m = 0

Tactic:
cases m

Goal state after:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 1 ↔ ↑a✝ = 0 ∧ ⊥ = 1 ∨ ↑a✝ = 1 ∧ ⊥ = 0

case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 1 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 2 ↔ ↑a✝ = 0 ∧ m = 2 ∨ ↑a✝ = 1 ∧ m = 1 ∨ ↑a✝ = 2 ∧ m = 0

Tactic:
cases m

Goal state after:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 2 ↔ ↑a✝ = 0 ∧ ⊥ = 2 ∨ ↑a✝ = 1 ∧ ⊥ = 1 ∨ ↑a✝ = 2 ∧ ⊥ = 0

case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 2 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 3 ↔ ↑a✝ = 0 ∧ m = 3 ∨ ↑a✝ = 1 ∧ m = 2 ∨ ↑a✝ = 2 ∧ m = 1 ∨ ↑a✝ = 3 ∧ m = 0

Tactic:
cases m

Goal state after:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 3 ↔ ↑a✝ = 0 ∧ ⊥ = 3 ∨ ↑a✝ = 1 ∧ ⊥ = 2 ∨ ↑a✝ = 2 ∧ ⊥ = 1 ∨ ↑a✝ = 3 ∧ ⊥ = 0

case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 3 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 3 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 3 ∧ ↑a✝ = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
m : WithBot ℕ
a✝ : ℕ
h : ↑a✝ < m
⊢ ↑a✝ + 1 ≤ m

Tactic:
cases m

Goal state after:
case coe.bot
a✝ : ℕ
h : ↑a✝ < ⊥
⊢ ↑a✝ + 1 ≤ ⊥

case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ < ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p✝ q✝ r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p q : ((i : ι) → R i)[X]
h : (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) p = (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) q
⊢ p = q

Tactic:
ext n i; simpa using congr_arg (fun p ↦ coeff (p i) n) h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ (p.comp (C r * X)).coeff n = p.coeff n * r ^ n

Tactic:
by
  simp_rw [comp, eval₂_eq_sum_range, (commute_X _).symm.mul_pow,
    ← C_pow, finsetSum_coeff, coeff_C_mul, coeff_X_pow]
  rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]
  · intro b _ h; simp_rw [if_neg h.symm, mul_zero]
  · rw [coeff_eq_zero_of_natDegree_lt, zero_mul]
    rwa [Finset.mem_range_succ_iff, not_le] at h

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

Goal state before:
pp: case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ ≤ embDomain f g₂ → g₁ ≤ g₂

Tactic:
Finsupp.le_def

Goal state after:
case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ (∀ (i : κ), (embDomain f g₁) i ≤ (embDomain f g₂) i) → g₁ ≤ g₂
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
⊢ ∃ b, a < b

Tactic:
let ⟨b, hb⟩ := exists_gt (a i)

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ ∃ b, a < b
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case tmul
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
k : ℕ
s : S
n : N
⊢ X ^ k • (rTensor N (↑R (monomial 0))) (s ⊗ₜ[R] n) = (rTensor N (↑R (monomial k))) (s ⊗ₜ[R] n)

Tactic:
simp only [rTensor_tmul, coe_restrictScalars, monomial_zero_left]

Goal state after:
case tmul
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
k : ℕ
s : S
n : N
⊢ X ^ k • C s ⊗ₜ[R] n = (monomial k) s ⊗ₜ[R] n
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
⊢ eval₂ f g (C a) = f a

Tactic:
C_apply,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
⊢ eval₂ f g ((monomial 0) a) = f a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.support.Nonempty ↔ p ≠ 0

Tactic:
by
  rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
i : σ
⊢ (rename f) (X i) = X (f i)

Tactic:
simp [MvPolynomial, rename, X, monomial]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
hf : Injective f
⊢ (rename f) p = (rename f) 0 ↔ p = 0

Tactic:
(MvPolynomial.rename_injective _ hf).eq_iff

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
hf : Injective f
⊢ p = 0 ↔ p = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)

Tactic:
simp_rw [degreeOf_eq_sup]; exact supDegree_add_le

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

Goal state before:
pp: case pos
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : a = 0
⊢ (cons (t 0) t.tail) a = t a

Tactic:
rw [c_a, cons_zero]

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

Goal state before:
pp: case e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ p.degrees = p.degrees + (C c).degrees

Tactic:
simp only [degrees_C, add_zero]

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

Goal state before:
pp: R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ algebraMap R (MvPolynomial σ S) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).comp (algebraMap R (MvPolynomial σ R))

Tactic:
ext; simp [C, monomial, map]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ 0 ≤ trailingDegree 1

Tactic:
by
  rw [← C_1]
  exact le_trailingDegree_C

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
⊢ n ≤ p.natTrailingDegree

Tactic:
by
  rw [natTrailingDegree_eq_support_min' hp]
  exact Finset.le_min' _ _ _ fun m hm => not_lt.1 fun hmn => mem_support_iff.1 hm <| hn _ hmn

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
refine le_antisymm ?_ le_trailingDegree_mul

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ p.trailingDegree + q.trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
⊢ (p - q).natDegree = (q - p).natDegree

Tactic:
rw [← natDegree_neg, neg_sub]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
c : R
⊢ (C a * X + C c).nextCoeff = c

Tactic:
rw [nextCoeff_of_natDegree_pos] <;> simp [ha]

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

Goal state before:
pp: case neg.refine_1
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (σ.sum fun x e ↦ e) ≤ (embDomain Embedding.some σ + Finsupp.single none i).sum fun x e ↦ e

Tactic:
simp [Finsupp.sum_add_index, Finsupp.sum_embDomain]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (((optionEquivLeft R σ) p).coeff m) = coeff (optionElim m d) p

Tactic:
rw [← optionEquivLeft_coeff_some_coeff_none]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (((optionEquivLeft R σ) p).coeff m) =
    coeff (optionElim m d).some (((optionEquivLeft R σ) p).coeff ((optionElim m d) none))
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.natDegree < n
⊢ f.reverse.coeff n = 0

Tactic:
rw [coeff_reverse, revAt, Function.Embedding.coeFn_mk, if_neg (not_le_of_gt hn),
    coeff_eq_zero_of_natDegree_lt hn]

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

Goal state before:
pp: case refine_3
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * f * (C f.leadingCoeff * C g.leadingCoeff) = p

Tactic:
← C_mul,

Goal state after:
case refine_3
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * f * C (f.leadingCoeff * g.leadingCoeff) = p
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:
by
    rw [geom_sum_succ']
    simp [zero_geom_sum]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x * y ∈ ↑(Subalgebra.toSubmodule (adjoin R (s ∪ t)))

Tactic:
change x * y ∈ adjoin R (s ∪ t)

Goal state after:
case refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x * y ∈ adjoin R (s ∪ t)
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.linearCombination R _root_.id) l2 = ↑(l z)
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)

Tactic:
have := @Finsupp.linearCombination_apply A A R

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.linearCombination R _root_.id) l2 = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a ↦ a • v i
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
H : ∀ (i : ι), ∃ n, s i ^ n • x ∈ S'
⊢ x ∈ toSubmodule (ofId (↥S') S).range

Tactic:
choose n hn using H

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
⊢ x ∈ toSubmodule (ofId (↥S') S).range
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : ∃ p ∈ I, p.degree ≤ ↑m ∧ p.leadingCoeff = r
⊢ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = r

Tactic:
rcases hr with ⟨p, hpI, hpdeg, rfl⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.leadingCoeff
Module: Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder

Goal state before:
pp: case refine_1
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
⊢ finrank F ↥K = 1 → K = ⊥

Tactic:
exact fun h' => Subalgebra.eq_bot_of_finrank_one h'

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
f : MvPolynomial (↥s) R →ₐ[R] S
hsur : Surjective ⇑f
⊢ ∃ ι x f, Surjective ⇑f

Tactic:
use { x : S // x ∈ s }, inferInstance, f

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support))

Tactic:
have hincl : of R M '' f.coeff.support ⊆ ⋃ g ∈ S, of R M '' g.coeff.support :=
    fun s hs ↦ Set.mem_iUnion₂.2 ⟨f, hf, hs⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
hincl : ⇑(of R M) '' ↑f.coeff.support ⊆ ⋃ g ∈ S, ⇑(of R M) '' ↑g.coeff.support
⊢ f ∈ ↑(adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support))
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b - n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
← modEq_add_modulus_iff,

Goal state after:
n a b : ℤ
⊢ a ≡ b - n + n [ZMOD n] ↔ a ≡ b [ZMOD n]
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h : p ∣ q
⊢ False

Tactic:
rcases hq.eq_one_or_self_of_dvd _ h with rfl | h

Goal state after:
case inl
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
q : ℕ
hq : Nat.Prime q
inst✝ : CharP R 1
hneq : 1 ≠ q
h : 1 ∣ q
⊢ False

case inr
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = q
⊢ False
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
F : Type w
inst✝⁹ : Ring R
inst✝⁸ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Semiring B
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, f a = 0
r : R₁
this : (algebraMap R₁ (A ⧸ I)) r = (mk I) ((algebraMap R₁ A) r)
⊢ (↑↑(lift I (↑f) hI)).toFun ((algebraMap R₁ (A ⧸ I)) r) = (algebraMap R₁ B) r

Tactic:
rw [this, RingHom.toFun_eq_coe, Ideal.Quotient.lift_mk,
        AlgHom.coe_toRingHom, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one,
        map_smul, map_one]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m] x

Tactic:
rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m % n] x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : (ts.concat t).length < n + 1
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Tactic:
length_concat,

Goal state after:
case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length + 1 < n + 1
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
x✝ : ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
p : R
k : ℕ
hp : Prime p
hk : 0 < k
hn : p ^ k = n
⊢ p ^ (k - 1 + 1) = n

Tactic:
Nat.sub_add_cancel hk

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
x✝ : ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
p : R
k : ℕ
hp : Prime p
hk : 0 < k
hn : p ^ k = n
⊢ p ^ k = n
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯)
      ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) (Quotient.mk'' g)) =
    Quotient.mk'' g

Tactic:
| _ g
     => 

Goal state after:
case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯)
      ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) (Quotient.mk'' g)) =
    Quotient.mk'' g
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯)
      ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) (Quotient.mk'' g)) =
    Quotient.mk'' g

Tactic:
simp only [Quotient.liftOn'_mk'', QuotientGroup.mk]

Goal state after:
case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ Quotient.mk'' ⋯.choose = Quotient.mk'' g