mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num.natAbs ^ n).Coprime (den ^ n)

Tactic:
exact hdn.pow _ _

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case inr
a : ℤ
ha : a ≤ 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0

Tactic:
· exact (mkRat_nonpos_iff a hb).mpr ha

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ |q| = ↑q.num.natAbs /. ↑q.den

Tactic:
by
  grind [abs_of_nonpos, neg_def, Rat.num_nonneg, abs_of_nonneg, num_divInt_den]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a * ↑u ∣ b ↔ a ∣ b

Tactic:
apply Units.mul_right_dvd

Goal state after:
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
a : α
h : IsLUB s a
b : β
hb : b ∈ upperBounds (l '' s)
⊢ u b ∈ upperBounds s

Tactic:
by rwa [gc.upperBounds_l_image] at hb

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ sSup (g '' f '' t) = sSup ((fun b ↦ g (f b)) '' t)

Tactic:
← image_comp,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ sSup (g ∘ f '' t) = sSup ((fun b ↦ g (f b)) '' t)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ

Tactic:
compl_iInter

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
π : α → Type u_12
ι : α → Type u_13
s : (a : α) → Set (ι a)
t : (a : α) → ι a → Set (π a)
⊢ (⋃ x ∈ univ.pi s, univ.pi fun a ↦ t a (x a)) = univ.pi fun a ↦ ⋃ j ∈ s a, t a j

Tactic:
by
  ext
  simp [Classical.skolem, forall_and]

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
this : ⋂ i, Iic (f i) = lowerBounds (range f)
⊢ (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)

Tactic:
simp [this, BddBelow]

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (i : α) × ↑(t i)
⊢ ↑((unionEqSigmaOfDisjoint h).symm x) = ↑x.snd

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompletelyDistribLattice (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
ext i; simp only [iInf_apply, iSup_apply, iInf_iSup_eq]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.coe
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ ↑a✝

Tactic:
· apply WithTop.coe_le_coe.2
          refine csInf_le ?_ haS
          use ⊥
          intro b _
          exact bot_le

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
⊢ Pairwise (Disjoint on extend e f ⊥)

Tactic:
by
  intro b₁ b₂ hne
  rcases em (∃ a₁, e a₁ = b₁) with ⟨a₁, rfl⟩ | hb₁
  · rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂
    · simpa only [onFun, he.extend_apply] using! hf (ne_of_apply_ne e hne)
    · simpa only [onFun, extend_apply' _ _ _ hb₂] using! disjoint_bot_right
  · simpa only [onFun, extend_apply' _ _ _ hb₁] using! disjoint_bot_left

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc a b ∪ Icc b a

Tactic:
rw [Icc_union_Icc', max_comm] <;> rfl

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s

Tactic:
simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', notMem_compl_iff, EqOn,
    Pi.one_apply]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
k : Set ι
h : mulSupport f ⊆ k
⊢ range f = f '' k ∨ range f = insert 1 (f '' k)

Tactic:
by
  have : range f ⊆ insert 1 (f '' k) :=
    (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_mono h))
  grind

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

Goal state before:
pp: m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

Tactic:
by
  refine ⟨fun h => ?_, congr_arg _⟩
  obtain hnm | rfl | hnm := lt_trichotomy n m
  · rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
    cases lt_irrefl _ hnm
  · rfl
  rw [← one_lt_factorial, h, one_lt_factorial] at hn
  rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
  cases lt_irrefl _ hnm

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

Goal state before:
pp: ⊢ 1 = 0!

Tactic:
factorial_zero

Goal state after:
⊢ 1 = 1
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommGroup β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ |f x - f y| ≤ f (x / y)

Tactic:
rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommGroup β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f x ≤ f y + f (x / y) ∧ f y ≤ f x + f (x / y)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : R
⊢ fract (↑n + a) = fract a

Tactic:
by
  rw [add_comm, fract_add_natCast]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ ↑k
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case below
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
⊢ ∃ n, ↑n ≤ x

Tactic:
obtain ⟨n, hn⟩ := exists_int_lt x
    exact ⟨n, hn.le⟩

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ y ^ (n + 1) < x

Tactic:
rwa [inv_pow, inv_lt_inv₀ xpos (pow_pos ypos _)] at h'n

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
tmp : (↑q.den - ↑q.num.natAbs * ⌊↑q.den / ↑q.num.natAbs⌋).natAbs.Coprime q.num.natAbs
⊢ (↑q.den - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs

Tactic:
simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using! tmp

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
H₁ H₂ : FloorRing R
this : FloorRing.floor = FloorRing.floor
⊢ H₁ = H₂

Tactic:
have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil_coe.l_unique H₂.gc_ceil_coe) fun _ => rfl

Goal state after:
R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
H₁ H₂ : FloorRing R
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ H₁ = H₂
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
x : M
⊢ 0 < y

Tactic:
by simpa using hxy

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
x : M
⊢ 1 < y

Tactic:
by simpa using hxy

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β✝ : Type v
γ : Type u_2
m : Multiset α
β : α → Type u_3
inst✝ : (a : α) → DecidableEq (β a)
f g : (a : α) → a ∈ m → β a
⊢ (∀ (a : α) (h : a ∈ m), f a h = g a h) ↔ f = g

Tactic:
simp [funext_iff]

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
l : List α
this : l <+~ a :: l ∧ ¬l ~ a :: l
⊢ Quot.mk (⇑(isSetoid α)) l < a ::ₘ Quot.mk (⇑(isSetoid α)) l

Tactic:
simpa [lt_iff_le_and_ne]

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp
α : Type u_1
s t : Multiset α
h : Rel (fun x1 x2 ↦ x1 = x2) s t
⊢ s = t

Tactic:
induction h <;> simp [*]

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p (a ::ₘ s) (b ::ₘ t)

Tactic:
apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)

Goal state after:
case cons
α : Type u_1
β : Type v
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p s t
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ s.card = t.card

Tactic:
induction h <;> simp [*]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : (hd :: tl).Nodup
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)

Tactic:
| cons hd tl ihl =>

Goal state after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : (hd :: tl).Nodup
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
h : a ∈ s
ht : ndinsert a s = s
⊢ s.attach = ndinsert ⟨a, ⋯⟩ s.attach

Tactic:
ndinsert_of_mem (mem_attach _ _)

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
h : a ∈ s
ht : ndinsert a s = s
⊢ s.attach = s.attach
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.toFinset.Nonempty ↔ l ≠ []

Tactic:
simp [Finset.nonempty_iff_ne_empty]

Goal state after:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.13
β : α → Type u_4
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : Fintype α
f g : (a : α) → β a
⊢ (∀ (a : α), a ∈ univ → f a = g a) ↔ f = g

Tactic:
simp [funext_iff]

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ s → x ∉ t₁ → x ∈ t₂ \ t₁

Tactic:
intro hx hx₂

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
hx : x ∈ s
hx₂ : x ∉ t₁
⊢ x ∈ t₂ \ t₁
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ ∅ = image f s ↔ s = ∅

Tactic:
by rw [eq_comm, image_eq_empty]

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ (castSucc 0).rev = rev 0

Tactic:
castSucc_zero'

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ rev 0 = rev 0
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: α : Sort u_1
k : ℕ
f g : Fin k → α
⊢ f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩

Tactic:
simp [funext_iff]

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

Goal state before:
pp: α : Sort u_1
k k' : ℕ
f g : Fin k → Fin k' → α
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Tactic:
simp [funext_iff]

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
h : a ≠ last (n + 1)
⊢ a.succAbove (last n) = last (n + 1)

Tactic:
rw [succAbove_of_lt_succ _ _ (succ_last _ ▸ lt_last_iff_ne_last.2 h), succ_last]

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

Goal state before:
pp: n : ℕ
⊢ Set.range succ = {0}ᶜ

Tactic:
by
  rw [← succAbove_zero, range_succAbove]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ predAbove 0 i.succ = i

Tactic:
rw [predAbove_succ_of_le _ _ (Fin.zero_le _)]

Goal state after:
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ {x} = univ

Tactic:
apply eq_of_subset_of_card_le (subset_univ {x})

Goal state after:
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ #univ ≤ #{x}
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
⊢ (∃ x, x ∈+ l) ↔ ¬l.Nodup

Tactic:
by
  simp [nodup_iff_forall_not_duplicate]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
⊢ snoc f a ∘ natAdd m = snoc (f ∘ natAdd m) a

Tactic:
by
  ext i
  refine Fin.lastCases ?_ (fun i ↦ ?_) i
  · simp only [Function.comp_apply]
    rw [snoc_last, natAdd_last, snoc_last]
  · simp only [comp_apply, snoc_castSucc]
    rw [natAdd_castSucc, snoc_castSucc]

Goal state after:
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op b a) s

Tactic:
rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]

Goal state after:
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
op' : β → β → β
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α),
    fold op' (m b) (map m s) = m (fold op b s) → fold op' (m b) (map m (a ::ₘ s)) = m (fold op b (a ::ₘ s))

Tactic:
by simp +contextual [hm]

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

Goal state before:
pp: case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
l₁✝ : List α
hr : Pairwise r (head✝ :: l₁✝)
h : l₁✝ <+ tail✝
⊢ head✝ :: l₁✝ <+ insertionSort r (head✝ :: tail✝)

Tactic:
| cons_cons _ h =>

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

Goal state before:
pp: case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → ∀ (d : List α), d ~ c → d <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hs : Pairwise r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
| cons_cons _ h =>

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ (l.rotate n).head? = l[n]?

Tactic:
by
  rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
h : Rel (Rel r) s t
⊢ Rel r s.join t.join

Tactic:
induction h with
  | zero => simp
  | cons hab hst ih => simpa using hab.add ih

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
g : α → Multiset β
⊢ ∀ (a : α) (s : Multiset α),
    (s.bind fun a ↦ f a ::ₘ g a) = map f s + s.bind g →
      ((a ::ₘ s).bind fun a ↦ f a ::ₘ g a) = map f (a ::ₘ s) + (a ::ₘ s).bind g

Tactic:
simp +contextual [add_comm, add_left_comm, add_assoc]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
p : M → Prop
inst✝ : DecidablePred p
⊢ (filter p s + filter (fun a ↦ ¬p a) s).prod = s.prod

Tactic:
filter_add_not

Goal state after:
M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
p : M → Prop
inst✝ : DecidablePred p
⊢ s.prod = s.prod
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
have : ∀ a, ∃ l : List β, f a = l := fun a => Quot.induction_on (f a) fun l => ⟨l, rfl⟩

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
this : ∀ (a : α), ∃ l, f a = ↑l
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ (n + 1).choose (k + 1) = 0

Tactic:
choose_succ_succ,

Goal state after:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ n.choose k + n.choose k.succ = 0
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 x✝

Tactic:
by rw [Nat.eq_zero_of_le_zero hk]; decide

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

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
choose_succ_succ,

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (n.choose k + n.choose k.succ) * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ ∀ (a_1 a'_1 : α), a_1 = a'_1 → cons (a' ::ₘ m) a b (cons m a' b' f) a_1 ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'_1

Tactic:
rintro a'' _ rfl

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) a'' ≍ cons (a ::ₘ m) a' b' (cons m a b f) a''
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

pp: case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
· have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
      have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by
        rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
      have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
      have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
      rw [choose_succ_succ, Nat.add_mul, Nat.add_mul, succ_sub_succ, h, h₁, h₂, Nat.add_mul,
        Nat.mul_sub_right_distrib, factorial_succ, ← Nat.add_sub_assoc h₃, Nat.add_assoc,
        ← Nat.add_mul, Nat.add_sub_cancel_left, Nat.add_comm]

Goal state after:
case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y) ↔
    ∀ ⦃a b : (i : ι) → α i⦄, s.domRestrict a = s.domRestrict b → f a = f b

Tactic:
simp [funext_iff]

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

Goal state before:
pp: n : ℕ
⊢ (n + 1 + 1).choose (n + 1) = n + 1 + 1

Tactic:
choose_succ_succ,

Goal state after:
n : ℕ
⊢ (n + 1).choose n + (n + 1).choose n.succ = n + 1 + 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
choose_succ_succ,

Goal state after:
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (range f)ᶜ ⊆ kernImage f s

Tactic:
by
  rw [← kernImage_empty]
  exact kernImage_mono (empty_subset _)

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap '' t ×ˢ s = ((fun b a ↦ (a, b)) '' t).seq s

Tactic:
prod_eq_seq,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap '' (Prod.mk '' t).seq s = ((fun b a ↦ (a, b)) '' t).seq s
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x / y ∈ H

Tactic:
rw [div_eq_mul_inv]; exact mul_mem hx (inv_mem hy)

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
⊢ ⇑↑H = Subtype.val

Tactic:
by
  rfl

Goal state after: