mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card ↥s ∣ Nat.card α

Tactic:
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
hx : ¬x ∈ s
⊢ (permutations'Aux x s).Nodup

Tactic:
induction s with

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

Goal state before:
pp: case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
⊢ ∀ (a : List α), a ∈ permutations'Aux x as → ∀ (b : List α), b ∈ permutations'Aux x bs → a ≠ b

Tactic:
rintro a ha' b hb' rfl

Goal state after:
case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
⊢ False
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ some (l.nextOr a d) = l[idxOf a l + 1]?

Tactic:
match l with
  | nil => simp at ha
  | [head] => simp at ha
  | x :: y :: tail =>
    rw [getElem?_cons_succ, nextOr]
    split_ifs with hx
    · grind
    rw [idxOf_cons_ne _ <| Ne.symm hx, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]
    grind

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

Goal state before:
pp: α : Type u_1
s : List α
⊢ s.permutations.Nodup ↔ s.Nodup

Tactic:
by
  refine ⟨?_, nodup_permutations s⟩
  contrapose
  rw [← exists_duplicate_iff_not_nodup]
  intro ⟨x, hs⟩
  rw [duplicate_iff_sublist] at hs
  obtain ⟨l, ht⟩ := List.Sublist.exists_perm_append hs
  rw [List.Perm.nodup_iff (List.Perm.permutations ht), ← exists_duplicate_iff_not_nodup]
  use x :: x :: l
  rw [List.duplicate_iff_sublist, ← permutations_take_two]
  exact take_sublist 2 _

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

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

Tactic:
rcases h with ⟨⟨gv, gp⟩, rfl⟩
    simp only
    refine mem_orbit _ (⟨gv, ?_⟩ : Subgroup.map K.subtype (H.subgroupOf K))
    simpa using! gp

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 α
g : G
a : α
h : G
⊢ (g⁻¹ * h * g) • a = a ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
← mem_stabilizer_iff,

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ g⁻¹ * h * g ∈ stabilizer G a ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ ∈ s

Tactic:
← mem_reverse_iff

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ ∈ s.reverse
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s

Tactic:
induction s with

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
⊢ (∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b) → Chain r ↑(a :: l)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r s → ∀ a ∈ s, ∀ b ∈ s, r a b

Tactic:
induction s with

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
⊢ Chain r ↑(a :: l) → ∀ a_2 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_2 b
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
h : Chain r s
⊢ s = Cycle.nil

Tactic:
induction s with

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

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
b : X
inst✝² : Fintype G
inst✝¹ : Fintype ↑(orbit G b)
inst✝ : Fintype ↥(stabilizer G b)
⊢ Fintype.card ↑(orbit G b) * Fintype.card ↥(stabilizer G b) = Fintype.card G

Tactic:
by
  rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup G b)]

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

Goal state before:
pp: n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ n.primeFactorsList.prod = p ^ k

Tactic:
← prod_replicate k p,

Goal state after:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ n.primeFactorsList.prod = (replicate k p).prod
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ H.index * f.range.index

Tactic:
apply dvd_mul_right

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
m : ℕ
hm : m < n
hdvd : m ∣ n
⊢ m = 1

Tactic:
simpa [h] using mem_properDivisors.mpr ⟨hdvd, hm⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k → ∃ j, ∃ (_ : j < k), x = p ^ j

Tactic:
rintro ⟨⟨j, hjk, rfl⟩, hlt⟩
    exact ⟨j, (Nat.pow_lt_pow_iff_right pp.one_lt).mp hlt, rfl⟩

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

Goal state before:
pp: b k : ℕ
l : List ℕ
⊢ ofDigits b (l ++ List.replicate k 0) = ofDigits b l

Tactic:
by
  rw [ofDigits_append]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (a ^ n) ^ (↑n)⁻¹.val = a

Tactic:
by rw [pow_right_comm, pow_zmod_val_inv_pow hn]

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

Goal state before:
pp: n : ℕ
⊢ n.divMaxPow 0 = n

Tactic:
by simp [divMaxPow]

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

Goal state before:
pp: n : ℕ
⊢ n.divMaxPow 1 = n

Tactic:
by simp [divMaxPow]

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

Goal state before:
pp: p : ℕ
⊢ divMaxPow 0 p = 0

Tactic:
by simp [divMaxPow]

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

Goal state before:
pp: p : ℕ
⊢ divMaxPow 1 p = 1

Tactic:
by simp [divMaxPow]

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

Goal state before:
pp: case h₁
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k ≤ (p.maxPowDvdDiv n).fst

Tactic:
rw [← padicValNat, ← pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn,
            pow_dvd_iff_le_of_spec hp hn h hl]
          apply Nat.le_refl

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

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

Tactic:
· by_cases h : digits b m = []
    · simp only [h, List.append_nil] at h_append ⊢
      exact getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append
    · exact (List.getLast_append_of_right_ne_nil _ _ h) ▸
          (getLast_digit_ne_zero _ <| digits_ne_nil_iff_ne_zero.mp h)

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

Goal state before:
pp: case ind.zero
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits 0
⊢ d < b + 2

Tactic:
rw [digits_zero] at hd

Goal state after:
case ind.zero
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ []
⊢ d < b + 2
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ 0 < bit false n

Tactic:
· simpa [Nat.bit, pos_iff_ne_zero]

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

Goal state before:
pp: case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (b.digits (n + 1)).head! % b

Tactic:
exact (Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <|
          Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: R : Type u_3
inst✝¹ : CommMonoidWithZero R
inst✝ : Subsingleton Rˣ
a b : R
ha : Irreducible a
hb : Irreducible b
h : a ≠ b
x✝ : Associated a b
u : Rˣ
h✝ : a * ↑u = b
⊢ False

Tactic:
simp_all [Subsingleton.elim u 1]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < 0
hnx : x ^ n = x ^ 0
⊢ False

Tactic:
exact irrefl 0 hn_pos

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b

Tactic:
rw [pow_add]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n / p ^ n.factorization p).factorization p

Tactic:
rw [Nat.factorization_div (Nat.ordProj_dvd n p)]

Goal state after:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n.factorization - (p ^ n.factorization p).factorization) p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
⊢ x ^ (m + k) = x ^ m * x ^ k

Tactic:
rw [pow_add]

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).coeff d = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).natDegree < d
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).coeff d = 0

Tactic:
· apply coeff_eq_zero_of_natDegree_lt
    apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ddf ?_)
    · exact natDegree_mul_le_of_le ‹_› ‹_›
    · exact ne_comm.mp h

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).coeff o = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree < o
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ ↑0 < ↑p.natDegree

Tactic:
by
      rw [← degree_eq_natDegree hp0]; exact hp

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a p + n ≤ rootMultiplicity a (p * (X - C a) ^ n)

Tactic:
rw [le_rootMultiplicity_iff h2, pow_add]
    exact mul_dvd_mul_right (pow_rootMultiplicity_dvd p a) _

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff = 1

Tactic:
apply monic_mul_C_of_leadingCoeff_mul_eq_one

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ (p.comp (-X)).leadingCoeff * (-1) ^ p.natDegree = 1
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ IsUnit (C (f.coeff 0))

Tactic:
apply IsUnit.map C

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ IsUnit (f.coeff 0)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (derivative p).natDegree ≤ p.natDegree - 1

Tactic:
by_cases p0 : p.natDegree = 0
  · simp [p0, derivative_of_natDegree_zero]
  · exact Nat.le_sub_one_of_lt (natDegree_derivative_lt p0)

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
degree_eq_natDegree hf,

Goal state after:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = ↑f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : ¬p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Goal state after:
case neg
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : ¬p.natDegree = 0
⊢ (p /ₘ (X - C a)).natDegree < n
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = (X - C a) ^ rootMultiplicity a p * q ∧ ¬X - C a ∣ q

Tactic:
classical
  rw [rootMultiplicity_eq_multiplicity, if_neg hp]
  apply (finiteMultiplicity_X_sub_C a hp).exists_eq_pow_mul_and_not_dvd

Goal state after:
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp.basic
α : Type u
s : Set (Set α)
U V : Set α
V_in : V ∈ s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ V

Tactic:
exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩

Goal state after:
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mpr
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) → U ∈ ⨅ i, s i

Tactic:
rintro ⟨I, Ifin, V, V_in, rfl⟩

Goal state after:
case mpr
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
Ifin : I.Finite
V : ↑I → Set α
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i ∈ ⨅ i, s i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
n : ℕ
c : R
k : ℕ
IH : (⇑derivative)^[k] ((X + C c) ^ n) = n.descFactorial k • (X + C c) ^ (n - k)
⊢ (⇑derivative)^[k + 1] ((X + C c) ^ n) = n.descFactorial (k + 1) • (X + C c) ^ (n - (k + 1))

Tactic:
simp [Nat.sub_succ', Function.iterate_succ_apply', IH, derivative_X_add_C_pow]
      ring

Goal state after:
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f ⊓ 𝓟 (univ.pi s) = ⊥ → ∃ i, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
simp only [inf_principal_eq_bot, mem_pi]

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ (univ.pi s)ᶜ) → ∃ i, (s i)ᶜ ∈ f i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff

Tactic:
nontriviality

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Sort u_2
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (∃ᶠ (x : α) in l, ∃ i, p i x) ↔ ∃ i, ∃ᶠ (x : α) in l, p i x

Tactic:
← not_iff_not

Goal state after:
α : Type u
ι : Sort u_2
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (¬∃ᶠ (x : α) in l, ∃ i, p i x) ↔ ¬∃ i, ∃ᶠ (x : α) in l, p i x
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

Tactic:
← not_iff_not

Goal state after:
α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (¬∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ¬∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Tactic:
nontriviality

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
⊢ (∃ t₂ ∈ 𝓟 t, u ×ˢ t₂ ⊆ s) → u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}

Tactic:
rintro ⟨v, v_in, hv⟩ a a_in b b_in

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
v : Set β
v_in : v ∈ 𝓟 t
hv : u ×ˢ v ⊆ s
a : α
a_in : a ∈ u
b : β
b_in : b ∈ t
⊢ (a, b) ∈ s
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
⊢ (∃ t₂ ∈ 𝓟 t, u ×ˢ t₂ ⊆ s) → u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}

pp: case refine_2
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s

Tactic:
· rintro ⟨v, v_in, hv⟩ a a_in b b_in
    exact hv (mk_mem_prod a_in <| v_in b_in)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)

Tactic:
sup_comm a,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (a ⊓ b)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case refine_1
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.fst ⁻¹' m₁ ⁻¹' u₁
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.fst ⁻¹' u₁

Tactic:
convert!
    hx

Goal state after:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case refine_2
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.snd ⁻¹' m₂ ⁻¹' u₂
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.snd ⁻¹' u₂

Tactic:
convert!
    hx

Goal state after:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
⊢ map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (map m₁ f₁).coprod (map m₂ f₂)

Tactic:
intro s
  simp only [mem_map, mem_coprod_iff]
  rintro ⟨⟨u₁, hu₁, h₁⟩, u₂, hu₂, h₂⟩
  refine ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩ <;> convert!
    hx

Goal state after:
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type ?u.3
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ Associated (gcd a b * lcm a b) (a * b)

Tactic:
rw [EuclideanDomain.gcd_mul_lcm]

Goal state after:
R : Type ?u.3
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ Associated (a * b) (a * b)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ normalizedFactors 1 = 0

Tactic:
rw [← Multiset.rel_zero_right]
    apply factors_unique irreducible_of_normalized_factor
    · intro x hx
      exfalso
      apply Multiset.notMem_zero x hx
    · apply prod_normalizedFactors one_ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
hr : r ≠ 0
s : R
hs : IsUnit s
hq : p = C r * C s
H : IsUnit (C s)
⊢ False

Tactic:
simp [hq, Polynomial.natDegree_C_mul hr] at hp'

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ Fintype.card ↑(Set.range f) = #(image f univ)

Tactic:
rw [← Set.toFinset_card, Set.toFinset_range]

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

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
p : A[X]
B : Type u_3
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
⊢ (p.rootSet B).ncard ≤ p.natDegree

Tactic:
classical
  grw [rootSet, Set.ncard_coe_finset, Multiset.toFinset_card_le]
  exact p.card_roots_map_le_natDegree

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

Goal state before:
pp: case pos
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
· rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]

Goal state after:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial (↥s) D
ha : (rename Subtype.val) a' ≠ 0
w : Multiset (MvPolynomial (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial (↥s) D)ˣ
hw : w.prod * ↑u = a'
⊢ (Multiset.map (⇑(rename Subtype.val)) w).prod * ↑((Units.map ↑(rename Subtype.val).toRingHom) u) =
    (rename Subtype.val) a'

Tactic:
by
      rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
        AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]

Goal state after: