mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
⊢ ↑m * (↑m)⁻¹ = 1

Tactic:
ZMod.coe_mul_inv_eq_one _ hmn

Goal state after:
case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
⊢ 1 = 1
Module: Mathlib.NumberTheory.Divisors

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

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

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

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

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

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

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

Tactic:
all_goals
    simp [divisorsAntidiag]
    grind

Goal state after:
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1 + 1).choose (k + 1) ≤ 2 ^ (n + 1)

Tactic:
rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

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

Goal state before:
pp: m : ℕ
inst✝¹ : NeZero m
n : ℕ
inst✝ : NeZero n
a : ZMod m
⊢ a.cast.val < m

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)
  by_cases! h : m < n
  · obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne n)
    rw [← natCast_val, val_cast_of_lt]
    · apply a.val_lt
    apply lt_of_le_of_lt (Nat.le_of_lt_succ (ZMod.val_lt a)) h
  · apply lt_of_lt_of_le (ZMod.val_lt _) (le_trans h (Nat.le_succ m))

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

Goal state before:
pp: case succ.e_head
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) = x

Tactic:
simp [Nat.add_mod, mod_eq_of_lt hxb]

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

Goal state before:
pp: case cons.hxy
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
· by_cases h' : L = []
      · rcases h' with rfl
        left
        simpa using w₂
      · right
        contrapose w₂
        refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
        rw [List.getLast_cons h']
        exact List.getLast_mem h'

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

Goal state before:
pp: case zero
n : ℕ
⊢ ofDigits 0 (digits 0 n) = n

pp: case succ
n b : ℕ
⊢ ofDigits (b + 1) ((b + 1).digits n) = n

Tactic:
· rcases n with - | n
    · rfl
    · simp

Goal state after:
case succ
n b : ℕ
⊢ ofDigits (b + 1) ((b + 1).digits n) = n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1

Tactic:
induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
  | succ f ih =>
    grind

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ orderOf x = n ↔ x ^ n = 1 ∧ ∀ m < n, 0 < m → x ^ m ≠ 1

Tactic:
simp_rw [Ne, ← isPeriodicPt_mul_iff_pow_eq_one, orderOf, minimalPeriod]
  split_ifs with h1
  · classical
    rw [find_eq_iff]
    simp only [h, true_and, not_and]
  · rw [iff_false_left h.ne]
    rintro ⟨h', -⟩
    exact h1 ⟨n, h, h'⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1

Tactic:
rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p

Tactic:
· simp [factorization_eq_zero_of_not_prime, pp]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
⊢ (single g 1 * x %ᵒᶠ g).coeff g' = 0

Tactic:
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)

Goal state after:
case inl
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
d : G
⊢ (single g 1 * x %ᵒᶠ g).coeff (g + d) = 0

case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * x %ᵒᶠ g).coeff g' = 0
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
⊢ (x * single g 1 %ᵒᶠ g).coeff g' = 0

Tactic:
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)

Goal state after:
case inl
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g d : G
⊢ (x * single g 1 %ᵒᶠ g).coeff (g + d) = 0

case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x * single g 1 %ᵒᶠ g).coeff g' = 0
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g g' : G
⊢ (single g 1 * (x /ᵒᶠ g)).coeff g' + (x %ᵒᶠ g).coeff g' = x.coeff g'

Tactic:
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)

Goal state after:
case inl
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g d : G
⊢ (single g 1 * (x /ᵒᶠ g)).coeff (g + d) + (x %ᵒᶠ g).coeff (g + d) = x.coeff (g + d)

case inr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * (x /ᵒᶠ g)).coeff g' + (x %ᵒᶠ g).coeff g' = x.coeff g'
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (C c * X ^ n).divX.natDegree = n - 1

Tactic:
divX_C_mul,

Goal state after:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (C c * (X ^ n).divX).natDegree = n - 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
by_cases hn0 : n = 0

Goal state after:
case pos
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : (aeval r) ((expand R p) f) = (aeval (r ^ p)) f
hg : (aeval r) ((expand R p) g) = (aeval (r ^ p)) g
⊢ (aeval r) ((expand R p) (f + g)) = (aeval (r ^ p)) (f + g)

Tactic:
rw [map_add, aeval_add, aeval_add, hf, hg]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
        else (0, p)).2
    else p) =
    p

Tactic:
rw [dif_pos hq, if_neg (mt And.left this)]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ (contract p (f * (expand R p) g)).coeff n = (contract p f * g).coeff n

Tactic:
rw [coeff_contract hp, coeff_mul, coeff_mul, ← sum_subset
    (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)), sum_image]

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff (x.1 * p, x.2 * p).1 * ((expand R p) g).coeff (x.1 * p, x.2 * p).2 =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ Set.InjOn (fun x ↦ (x.1 * p, x.2 * p)) ↑(antidiagonal n)

case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
have hp : p ≠ 0 := left_ne_zero_of_mul hpq

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
        else (0, p)).1
    else 0) =
    0

Tactic:
rw [dif_pos hq, if_neg (mt And.left this)]

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬(g.comp (X ^ p ^ n)).IsRoot r
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
← expand_eq_comp_X_pow

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (aeval x) p = 0

Tactic:
by
  rw [← aeval_map_algebraMap A, ← mapAlg_eq_map, hp, map_multiset_prod, Multiset.prod_eq_zero]
  rw [Multiset.map_map, Multiset.mem_map]
  exact ⟨x, hx, by simp⟩

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ generate (FilterBasis.ofSets s).sets = generate s

Tactic:
FilterBasis.ofSets_sets,

Goal state after:
α : Type u_1
s : Set (Set α)
⊢ generate (sInter '' {t | t.Finite ∧ t ⊆ s}) = generate s
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
⊢ p.natDegree = 0

Tactic:
by
    obtain rfl | hp' := eq_or_ne p 0
    · exact natDegree_zero
    rw [natDegree_eq_zero_iff_degree_le_zero]
    by_contra! f_nat_degree_pos
    rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos
    let m := p.natDegree - 1
    have hm : m + 1 = p.natDegree := tsub_add_cancel_of_le (by lia)
    have h2 := coeff_derivative p m
    rw [Polynomial.ext_iff] at hp
    rw [hp m, coeff_zero, ← Nat.cast_add_one, ← nsmul_eq_mul', eq_comm, smul_eq_zero] at h2
    replace h2 := h2.resolve_left m.succ_ne_zero
    rw [hm, ← leadingCoeff, leadingCoeff_eq_zero] at h2
    exact hp' h2

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

Goal state before:
pp: α : Type u_1
f : Filter α
h : ∃ x, f = ⨅ i, 𝓟 (x i)
⊢ f.IsCountablyGenerated

Tactic:
rcases h with ⟨x, rfl⟩
  apply isCountablyGenerated_seq

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

Goal state before:
pp: α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ t ∈ ⨅ a ∈ s, f a ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a

Tactic:
by
  classical
  simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
  refine ⟨fun h => ?_, ?_⟩
  · rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
    refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
    refine iInter_congr_of_surjective id surjective_id ?_
    rintro ⟨a, ha⟩
    simp [ha]
  · rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊔ g₂) = f ×ˢ g₁ ⊔ f ×ˢ g₂

Tactic:
simp only [prod_eq_inf, comap_sup, inf_sup_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
⊢ map m (f ×ˢ g) = (map (fun a b ↦ m (a, b)) f).seq g

Tactic:
by
  simp only [Filter.ext_iff, mem_map, mem_prod_iff, mem_map_seq_iff, exists_and_left]
  intro s
  constructor
  · exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩
  · exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩

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

Goal state before:
pp: ⊢ cofinite = atTop

Tactic:
by
  refine le_antisymm ?_ atTop_le_cofinite
  refine atTop_basis.ge_iff.2 fun N _ => ?_
  simpa only [mem_cofinite, compl_Ici] using! finite_lt_nat N

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)

Tactic:
simp only [prod_eq_inf, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = s ×ˢ t
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
have hqk := congrArg Filter.ker hq.2.2

Goal state after:
case refine_4
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = (𝓟 q.1 ⊔ q.2).ker
⊢ q = (f.ker, Coheyting.boundary f)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ derivative ((⇑derivative)^[k] (∏ a ∈ S, (X - C a))) =
    ↑(k + 1)! * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
ind,

Goal state after:
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ derivative (↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)) =
    ↑(k + 1)! * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case a
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
T : Finset R
hT : T ∈ powersetCard (#S - k) S
⊢ derivative (∏ a ∈ T, (X - C a)) = ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)

Tactic:
derivative_prod_finset,

Goal state after:
case a
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
T : Finset R
hT : T ∈ powersetCard (#S - k) S
⊢ ∑ a ∈ T, (∏ a ∈ T.erase a, (X - C a)) * derivative (X - C a) = ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
h₁ : X ^ 2 - C 1 = (X + C 1) * (X - C 1)
h : X ^ 2 - C 1 = 0
⊢ False

Tactic:
simpa using congrArg (coeff · 0) h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p = C p.content * p.primPart

Tactic:
by_cases h : p = 0; · simp [h]
  rw [primPart, if_neg h, ← Classical.choose_spec (C_content_dvd p)]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
hnezero : derivative p ≠ 0
⊢ rootMultiplicity t (derivative p) = m - 1

Tactic:
exact le_antisymm (by rwa [rootMultiplicity_le_iff hnezero, hm])
    (rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero _ t hnezero)

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p.degree < (q * C q.leadingCoeff⁻¹).degree

Tactic:
by rwa [degree_mul_leadingCoeff_inv q hq0]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (⊤, (a * c).leadingCoeff)

Tactic:
hac,

Goal state after:
case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (⊤, leadingCoeff 0)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
b : R
ha : a ≠ 0
⊢ (C a * X + C b).roots = {-(a⁻¹ * b)}

Tactic:
by
  simp [roots_C_mul_X_add_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

Tactic:
rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

Tactic:
rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    C (lcm p.content q.content) * r ∣ s
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    C (lcm p.content q.content) * r ∣ s

Tactic:
rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (C (lcm p.content q.content) * r).content ∣ s.content ∧ (C (lcm p.content q.content) * r).primPart ∣ s.primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case a
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ p.count a.factors ≤ Nat.find ⋯

Tactic:
have hph := pow_ne_zero (@Nat.find (fun n => a ∣ p ^ n) _ ⟨n, h⟩) hp.ne_zero

Goal state after:
case a
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
hph : p ^ Nat.find ⋯ ≠ 0
⊢ p.count a.factors ≤ Nat.find ⋯
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
| ↑f k ⟨↑l, hl⟩

Tactic:
← (piLTLim hi).right_inv f

Goal state after:
ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
| ↑((piLTLim hi).toFun ((piLTLim hi).invFun f)) k ⟨↑l, hl⟩