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

Goal state before:
pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ q.coeff.support, b ≠ aq → (if ap + b = ap + aq then p.coeff ap * q.coeff b else 0) = 0

Tactic:
refine fun a ha hne => if_neg (fun he => ?_)
    apply_fun D at he; simp_rw [hadd] at he
    exact (add_lt_add_right (((Finset.le_sup ha).trans hq).lt_of_ne <| hD.ne_iff.2 hne) _).ne he

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

Goal state before:
pp: R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ

Tactic:
rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]

Goal state after:
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

Goal state after:
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
n : ℕ
i : ι
⊢ p.coeff n i = q.coeff n i
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
p : R[X]
i : ℤ
⊢ eval (↑i) (map f p) = f (eval (↑i) p)

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), Std.Trichotomous s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex r s a b
hba : ¬Pi.Lex r s b a
h : ∃ a_1, a a_1 ≠ b a_1
i : ι := wf.min {i | a i ≠ b i} h
hri : ∀ (j : ι), r j i → a j = b j
this : ¬s (b i) (a i) → a i = b i
⊢ False

Tactic:
exact hba ⟨i, (hri · · |>.symm), Not.imp_symm this <| wf.min_mem {i | a i ≠ b i} h⟩

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
hl : ∀ (x : ι), x ∈ {i | a i ≠ b i} → ¬x < i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ toLex a j = toLex b j

Tactic:
by
    contrapose! hl
    exact ⟨j, hl, hj⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    one_mul]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ C r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

Tactic:
by
  constructor
  · rintro ⟨φ, rfl⟩ c
    rw [coeff_C_mul]
    apply dvd_mul_right
  · intro h
    choose C hc using h
    classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]

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

Goal state before:
pp: σ : Type u_1
S : Type u_2
inst✝ : CommSemiring S
⊢ aevalTower (AlgHom.id S S) = aeval

Tactic:
by
  ext
  simp only [aevalTower_X, aeval_X]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
induction cg generalizing g with
    | zero =>
      rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
      simp_rw [mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), reflect_C_mul,
        reflect_monomial, add_comm, revAt_add Nf Og, mul_assoc, X_pow_mul, mul_assoc, ←
        pow_add (X : R[X]), add_comm]
    | succ cg hcg =>
      by_cases g0 : g = 0
      · rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
      rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
        try assumption
      · exact le_add_left card_support_C_mul_X_pow_le_one
      · exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
      · exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt g0) Cg)
      · exact le_trans eraseLead_natDegree_le_aux Og

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
⊢ (sumRingEquiv R S₁ S₂) (C r) = C (C r)

Tactic:
by
  unfold sumRingEquiv C MvPolynomial; simp [monomial]

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

Goal state before:
pp: case neg.inl.succ
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ 0 - 0 = 0

Tactic:
sub_zero

Goal state after:
case neg.inl.succ
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → eval₂ i (⅟x) (reflect N (C r * X ^ n)) * x ^ N = eval₂ i x (C r * X ^ n)

pp: case refine_3
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ N →
        eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f →
          eval₂ i (⅟x) (reflect N g) * x ^ N = eval₂ i x g →
            eval₂ i (⅟x) (reflect N (f + g)) * x ^ N = eval₂ i x (f + g)

Tactic:
· intro n r _ hnN
    simp only [revAt_le hnN, reflect_C_mul_X_pow, eval₂_X_pow, eval₂_C, eval₂_mul]
    conv in x ^ N => rw [← Nat.sub_add_cancel hnN]
    rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]

Goal state after:
case refine_3
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ N →
        eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f →
          eval₂ i (⅟x) (reflect N g) * x ^ N = eval₂ i x g →
            eval₂ i (⅟x) (reflect N (f + g)) * x ^ N = eval₂ i x (f + g)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ (p.comp (-X)).natDegree = p.natDegree

Tactic:
natDegree_comp_eq_of_mul_ne_zero (by simp [hp]),

Goal state after:
case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.natDegree * (-X).natDegree = p.natDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : ¬p = 0
⊢ ((optionEquivLeft R σ) p).natDegree = degreeOf none p

Tactic:
· rw [Polynomial.natDegree, degree_optionEquivLeft R c, Nat.cast_withBot, WithBot.unbotD_coe]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff ((revAt f.natDegree) 1) = f.nextCoeff

Tactic:
nextCoeff

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff ((revAt f.natDegree) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Tactic:
hp.irreducible_iff_natDegree,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)
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₂) = p

Tactic:
rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ,
          Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1]

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 + 1 * X ^ 2
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0

Tactic:
rw [Ne, ← degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, WithBot.add_eq_bot, not_or,
    degree_eq_bot]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬p.degree = ⊥
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f S ≤ f.range

Tactic:
← Algebra.map_top

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f S ≤ map f ⊤
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
S : Subalgebra R A
h : ⊤.FG
⊢ S.val.range.FG

Tactic:
← Algebra.map_top

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ⊤.FG
⊢ (map S.val ⊤).FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f g : R[X]
x✝¹ : f ∈ Submodule.span R[X] (⇑C '' ↑I)
x✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hf : ∀ (n : ℕ), f.coeff n ∈ I
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ (f + g).coeff n ∈ I

Tactic:
by simp [I.add_mem (hf n) (hg n)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
⊢ f ∈ map C I ↔ ∀ (n : ℕ), f.coeff n ∈ I

Tactic:
by
  constructor
  · intro hf
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
    · intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [h]
    · simp
    · exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
    · intro f g _ hg n
      rw [smul_eq_mul, coeff_mul]
      exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)
  · intro hf
    rw [← sum_monomial_eq f]
    refine (I.map C : Ideal R[X]).sum_mem fun n _ => ?_
    simp only [← C_mul_X_pow_eq_monomial]
    rw [mul_comm]
    exact (I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ coeff 1 0 ∉ P

Tactic:
rw [coeff_one_zero, ← eq_top_iff_one]

Goal state after:
case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬P = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ∈ (antidiagonal ((m, n).1 + (m, n).2)).erase (m, n)
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
Finset.mem_erase,

Goal state after:
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ≠ (m, n) ∧ (i, j) ∈ antidiagonal ((m, n).1 + (m, n).2)
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hlt : f.eraseLead.natDegree < f.natDegree
he : f.eraseLead ∈ I
⊢ f.eraseLead.natDegree < n✝

Tactic:
simpa [hn] using hlt

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), C (f.coeff i) ∈ I
⊢ Ideal.span {g | ∃ i, g = C (f.coeff i)} ≤ I

Tactic:
by
  simp only [@eq_comm _ _ (C _)]
  exact (Ideal.span_le.trans range_subset_iff).mpr cf

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ ∃ a, (MvPolynomial.aeval Subtype.val) a = x

Tactic:
← Set.mem_range,

Goal state after:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ x ∈ Set.range ⇑(MvPolynomial.aeval Subtype.val)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Type uA
hfintype : Fintype ι
f : FreeAlgebra R ι →ₐ[R] A
hsur : Surjective ⇑f
⊢ FiniteType R A

Tactic:
let : Fintype ι := hfintype

Goal state after:
case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Type uA
hfintype : Fintype ι
f : FreeAlgebra R ι →ₐ[R] A
hsur : Surjective ⇑f
this : Fintype ι := hfintype
⊢ FiniteType R A
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
⊢ FiniteType R S

Tactic:
let : Fintype ι := hfintype

Goal state after:
case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
this : Fintype ι := hfintype
⊢ FiniteType R S
Module: Mathlib.Algebra.Algebra.Subalgebra.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)

Tactic:
rcases subsingleton_or_nontrivial R with _ | _
  · have := Module.subsingleton R S; simp
  nontriviality S using rank_subsingleton'
  let : Algebra A (Algebra.adjoin A (B : Set S)) := Subalgebra.algebra _
  let : SMul A (Algebra.adjoin A (B : Set S)) := Algebra.toSMul
  have : IsScalarTower R A (Algebra.adjoin A (B : Set S)) :=
    IsScalarTower.of_algebraMap_eq (congrFun rfl)
  rw [rank_mul_rank R A (Algebra.adjoin A (B : Set S))]
  change _ = Module.rank R ((Algebra.adjoin A (B : Set S)).restrictScalars R)
  rw [Algebra.restrictScalars_adjoin]; rfl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f g : MvPolynomial σ R
x✝¹ : f ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I)
x✝ : g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I)
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
n : σ →₀ ℕ
⊢ coeff n (f + g) ∈ I

Tactic:
by simp [I.add_mem (hf n) (hg n)]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Ring

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ (n • x) • y = n • x • y

Tactic:
smul_assoc

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs < b ∧ ↑z.natAbs ≡ a [ZMOD b]

Tactic:
constructor <;> rw [natAbs_of_nonneg hz1] <;> assumption

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
⊢ ↑a = ↑b

Tactic:
wlog hle : a ≤ b

Goal state after:
case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
this : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ}, a ≡ b [MOD p] → a ≤ b → ↑a = ↑b
hle : ¬a ≤ b
⊢ ↑a = ↑b

R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
hle : a ≤ b
⊢ ↑a = ↑b
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

Tactic:
wlog hle : a ≤ b

Goal state after:
case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a ≡ b [MOD p])
hle : ¬a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: 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
⊢ Function.Injective ⇑f

Tactic:
refine (injective_iff_map_eq_zero f).mpr fun x hx => ?_

Goal state after:
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
x : Unitization R ↥s
hx : f x = 0
⊢ x = 0
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd ++ r = (permutationsAux2 t ts r ys f).snd

Tactic:
induction ys generalizing f

Goal state after:
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t ts [] [] f).snd ++ r = (permutationsAux2 t ts r [] f).snd

case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), (permutationsAux2 t ts [] tail✝ f).snd ++ r = (permutationsAux2 t ts r tail✝ f).snd
f : List α → β
⊢ (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd ++ r = (permutationsAux2 t ts r (head✝ :: tail✝) f).snd
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
x y : A
hx : star x ∈ S
hy : star y ∈ S
⊢ star (x + y) ∈ S

Tactic:
exact (star_add x y).symm ▸ add_mem hx hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd.length = ys.length

Tactic:
induction ys generalizing f

Goal state after:
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
f : List α → β
⊢ (permutationsAux2 t ts [] [] f).snd.length = [].length

case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), (permutationsAux2 t ts [] tail✝ f).snd.length = tail✝.length
f : List α → β
⊢ (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd.length = (head✝ :: tail✝).length
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case star
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 : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)
b x✝ : A
hx✝ : x✝ ∈ adjoin R s
h : p ⟨x✝, hx✝⟩
⊢ p ⟨Star.star x✝, ⋯⟩

Tactic:
exact star _ h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (y :: z :: l).next x h = z

Tactic:
rw [next, nextOr, if_pos hx]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

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

Tactic:
simp_rw [orbitRel_apply]

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