mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r ≤ ↑r ! * ↑(n.choose r)

Tactic:
norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.pow_sub_le_descFactorial r

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = if a = 0 then 0 else n - a.val

Tactic:
neg_val'

Goal state after:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
⊢ 0 < b ^ k

Tactic:
positivity

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

Goal state before:
pp: b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ 0 < b * m

Tactic:
positivity

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

Goal state before:
pp: b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ 0 < ?m.22

Tactic:
positivity

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

Goal state before:
pp: b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ 0 < b ^ k * m

Tactic:
positivity

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ¬a ^ m ∣ b

Tactic:
apply not_pow_dvd_of_emultiplicity_lt

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ emultiplicity a b < ↑m
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b

Tactic:
apply not_pow_dvd_of_emultiplicity_lt

Goal state after:
case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ emultiplicity a b < ↑(n + 1)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
a b : α
⊢ emultiplicity (f a) (f b) = emultiplicity a b

Tactic:
simp [emultiplicity_eq_emultiplicity_iff, ← map_pow, map_dvd_iff]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ orderOf x = 1

Tactic:
convert! Eq.trans _ (isPeriodicPt_minimalPeriod (x * ·) 1)

Goal state after:
case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ orderOf x = (fun x_1 ↦ x * x_1)^[minimalPeriod (fun x_1 ↦ x * x_1) 1] 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (-b) = emultiplicity p b

Tactic:
rw [emultiplicity_neg]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (-b) < emultiplicity p a

Tactic:
rw [emultiplicity_neg]

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b < emultiplicity p a
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a ∣ b

Tactic:
← factorization_le_iff_dvd ha hb,

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a.factorization ≤ b.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
hn : n = 0
⊢ n.factorization p ≤ b

Tactic:
simp [hn]

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

Goal state before:
pp: n p : ℕ
hn : n = 0
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
simp [hn]

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ k ! * n ! ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ ¬p ∣ n

Tactic:
rw [← h]

Goal state after:
case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ ¬p ∣ n / p ^ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mpr.inr
n p : ℕ
hp : Prime p
not_dvd : ¬p ∣ n
⊢ n / p ^ n.factorization p = n

Tactic:
· simp [Nat.factorization_eq_zero_of_not_dvd not_dvd]

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

Goal state before:
pp: p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ k + 1 ≠ 0

Tactic:
positivity

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})

Tactic:
simp +contextual [Finset.disjoint_right, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]

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

Goal state before:
pp: case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
← factorization_le_iff_dvd ha hb,

Goal state after:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ (a / p ^ a.factorization p).factorization ≤ (b / p ^ b.factorization p).factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
simpa [prod_primeFactorsList hn] using (n.primeFactorsList : Multiset ℕ).toFinset_prod_dvd_prod

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

Goal state before:
pp: a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) = a.gcd b

Tactic:
apply gcd_greatest

Goal state after:
case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ a

case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ b

case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
a b : ℤ
⊢ x ^ (a - b) = 1 ↔ x ^ a = x ^ b

Tactic:
zpow_sub,

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
a b : ℤ
⊢ x ^ a * (x ^ b)⁻¹ = 1 ↔ x ^ a = x ^ b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)

Tactic:
WithTop.add_left_inj h,

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℕ
⊢ g ∈ zpowers (g ^ k) ↔ k.gcd (orderOf g) = 1

Tactic:
rw [← zpow_natCast g k, mem_zpowers_zpow_iff, Int.gcd_natCast_natCast]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : ¬p.coeff 0 = 0
hpX0 : p.divX = 0
⊢ M (p.divX * X)

Tactic:
rw [hpX0, zero_mul]; exact M0

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

Goal state before:
pp: case refine_2.inl.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
refine Or.inl ?_

Goal state after:
case refine_2.inl.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
this : ∀ (f g : R[X]), p = f * g → f.degree ≤ g.degree → IsUnit f ∨ IsUnit g
H : g.degree < f.degree
⊢ IsUnit f ∨ IsUnit g

Tactic:
rw [mul_comm] at h

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = g * f
this : ∀ (f g : R[X]), p = f * g → f.degree ≤ g.degree → IsUnit f ∨ IsUnit g
H : g.degree < f.degree
⊢ IsUnit f ∨ IsUnit g
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative ↑n = 0

Tactic:
rw [← map_natCast C n]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (C ↑n) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [hfg, natDegree_zero]

Goal state after:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = f.natDegree - g.natDegree
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.natDegree + (f /ₘ g).degree = ↑f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
degree_eq_natDegree hfg,

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.natDegree + ↑(f /ₘ g).natDegree = ↑f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
| (⇑derivative)^[k] p

Tactic:
rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
| ∑ i ∈ ((⇑derivative)^[k] p).support, C (((⇑derivative)^[k] p).coeff i) * X ^ i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ q * p %ₘ q = 0

Tactic:
modByMonic_eq_zero_iff_dvd hq

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ q ∣ q * p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : map f (y %ₘ x) = 0
⊢ 0 = map f 0

Tactic:
Polynomial.map_zero

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : map f (y %ₘ x) = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : y %ₘ x = 0
⊢ map f 0 = 0

Tactic:
Polynomial.map_zero

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : y %ₘ x = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
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

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:
· rw [(divByMonic_eq_zero_iff <| monic_X_sub_C a).mpr, coeff_zero]
    apply degree_lt_degree; rw [hp, natDegree_X_sub_C]; simp

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)).coeff n = 0
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : B.Nonempty
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Tactic:
· exact countable_biInf_eq_iInf_seq Bcbl Bnonempty f

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ p * q %ₘ q = 0

Tactic:
modByMonic_eq_zero_iff_dvd hq

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ q ∣ p * q
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
⊢ (f ⊓ g).IsCountablyGenerated

Tactic:
by
  rcases f.exists_antitone_basis with ⟨s, hs⟩
  rcases g.exists_antitone_basis with ⟨t, ht⟩
  exact HasCountableBasis.isCountablyGenerated ⟨hs.1.inf ht.1, Set.to_countable _⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
⊢ -p %ₘ q = -(p %ₘ q)

Tactic:
rw [eq_neg_iff_add_eq_zero, ← add_modByMonic, neg_add_cancel, zero_modByMonic]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) • X ^ (n - k)

Tactic:
iterate_derivative_X_pow_eq_C_mul n k,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ C ↑(n.descFactorial k) * X ^ (n - k) = ↑(n.descFactorial k) • X ^ (n - k)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
s : (i : ι) → { s // s ∈ l i }
hsd : Pairwise (Disjoint on fun i ↦ ↑((fun i ↦ s ↑i) i))
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
exact ⟨fun i => s i, fun i => (s i).2, hsd.set_of_subtype _ _⟩

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

Goal state before:
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 ⟨x, y⟩ ⟨hx, hy⟩
    exact h hx y hy

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a

pp: case inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
· exact Or.inr fun ha => hnab ⟨ha, hb⟩

Goal state after:
case inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s

Tactic:
rw [prod_comm, mem_map, mem_prod_iff_left]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t ∈ g, ∀ᶠ (y : α) in f, ∀ x ∈ t, (x, y) ∈ Prod.swap ⁻¹' s) ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ a \ ∂ a = ￢￢a

Tactic:
← hnot_hnot_sup_boundary a

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case succ
M : Type u_1
inst✝ : AddMonoid M
s : Set M
n : ℕ
IH : ⇑ofAdd '' (n • s) = (⇑ofAdd '' s) ^ n
⊢ ⇑ofAdd '' ((n + 1) • s) = (⇑ofAdd '' s) ^ (n + 1)

Tactic:
simp [succ_nsmul, pow_succ, IH]

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case succ
M : Type u_1
inst✝ : AddMonoid M
s : Set (Multiplicative M)
n : ℕ
IH : ⇑toAdd '' s ^ n = n • ⇑toAdd '' s
⊢ ⇑toAdd '' s ^ (n + 1) = (n + 1) • ⇑toAdd '' s

Tactic:
simp [succ_nsmul, pow_succ, IH]

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₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
⊢ (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s

Tactic:
refine ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩

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

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₂
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ ∀ {a : Associates α}, Irreducible a ↔ Prime a

Tactic:
rw [← Associates.irreducible_iff_prime_iff]
      apply UniqueFactorizationMonoid.irreducible_iff_prime

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
⊢ (p ::ₘ f).prod ~ᵤ g.prod → Multiset.Rel Associated (p ::ₘ f) g

Tactic:
hfg

Goal state after:
case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ Multiset.Rel Associated (p ::ₘ f) g
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
⊢ d ∈ ↑(Finset.image (fun uv ↦ uv.1) fg)

Tactic:
hfg

Goal state after:
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
⊢ d ∈ ↑(Finset.image (fun uv ↦ uv.1) (Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))))
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ {d | (weight w) d ≤ n}.Finite

Tactic:
classical
  set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
  suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
    exact Set.Finite.subset (Finset.finite_toSet _) this
  intro d hd
  rw [hfg]
  simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
    Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]
  use Finsupp.equivFunOnFinite.symm (Function.const σ n) - d
  ext x
  dsimp at hd
  grw [← le_weight _ (hw x)] at hd
  simp [*]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
hs : ∀ a ∈ 0, Irreducible a
⊢ 0 = Multiset.map normalize 0

Tactic:
Multiset.map_zero

Goal state after:
case empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
hs : ∀ a ∈ 0, Irreducible a
⊢ 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb)
⊢ p ∣ a ∨ p ∣ b

Tactic:
exact
          let ⟨q, hqf, hq⟩ := Multiset.exists_mem_of_rel_of_mem h (Multiset.mem_cons_self p _)
          (Multiset.mem_add.1 hqf).elim
            (fun hqa =>
              Or.inl <| hq.dvd_iff_dvd_left.2 <| hfa.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqa))
            fun hqb =>
            Or.inr <| hq.dvd_iff_dvd_left.2 <| hfb.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqb)

Goal state after: