mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ IsLeast (f '' s) (f a) ↔ IsGreatest s a

Tactic:
by
  simp [IsLeast, IsGreatest, hf.injective.eq_iff, hf.mem_lowerBounds_image]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
⊢ a = c ∧ b = d

Tactic:
obtain ⟨h₂, -⟩ := (heq a).mp ⟨le_refl _, h⟩

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ a = c ∧ b = d
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: γ : Type u_3
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB ({a} ∪ s) (a ⊔ b)

Tactic:
exact isLUB_singleton.union hs

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a k a' : α
h : a + k = a'
⊢ termg n x a + k = termg n x a'

Tactic:
simp [h.symm, termg, add_assoc]

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a ≤ 1 / b
⊢ b ≤ a

Tactic:
simpa using one_div_le_one_div_of_le (by simpa) h

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b c d : α
h : a * (b / c) ≤ d
hc : 0 < c
⊢ b * a ≤ d * c

Tactic:
rw [← mul_div_assoc] at h
  rwa [mul_comm b, ← div_le_iff₀ hc]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ 1 / a ≤ b⁻¹ ↔ b ≤ a

Tactic:
div_le_iff_of_neg ha,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ b⁻¹ * a ≤ 1 ↔ b ≤ a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 2⁻¹ ≤ 1 - 1 / a

Tactic:
rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 / a ≤ 1 - 2⁻¹
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ {x, y} = [x, y]

Tactic:
insert_neg,

Goal state after:
α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ x :: {y} = [x, y]

α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x ∈ {y}
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map g ∘ map f = map (g ∘ f)

Tactic:
by
  ext l; rw [comp_map, Function.comp_apply]

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

Goal state before:
pp: case cons.zero
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
⊢ take (take 0 (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take 0 (head✝ :: tail✝)).flatten

Tactic:
simp [take_length_add_append, *]

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

Goal state before:
pp: case cons.succ
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
n✝ : ℕ
⊢ take (take (n✝ + 1) (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten =
    (take (n✝ + 1) (head✝ :: tail✝)).flatten

Tactic:
simp [take_length_add_append, *]

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

Goal state before:
pp: α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ Forall p l → q x ∧ Forall q l

Tactic:
exact And.imp (h x) (Forall.imp h)

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

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n / (x /. d) = d /. n

Tactic:
by
  rw [div_eq_mul_inv, inv_divInt, mul_comm, divInt_mul_divInt_cancel hx]

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

Goal state before:
pp: case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b

pp: case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b

Tactic:
· simp [b0]

Goal state after:
case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑a / ↑b

Tactic:
rw [← cast_natCast, ← cast_natCast b, ← cast_div]

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ b ≠ 0

Tactic:
refine mt ?_ b0

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ b = 0 → ↑b = 0
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
by
  rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n ↦ ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n + k), f i

Tactic:
simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : SupSet α
g : β → α
f : ι → β
⊢ sSup (range fun b ↦ g ↑b) = sSup (range fun i ↦ g (f i))

Tactic:
← image_eq_range,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : SupSet α
g : β → α
f : ι → β
⊢ sSup (g '' range f) = sSup (range fun i ↦ g (f i))
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
⊢ ∃ i', f i ≤ f ↑i'

Tactic:
by_cases hi : f i = ⊥

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'

case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ ∅

Tactic:
by
    rw [← h]; exact inter_subset_inter_right _ (subset_sUnion_of_mem hs)

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ ⨆ ij, f ij.fst ij.snd = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j

Tactic:
iSup_eq_top,

Goal state after:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ (∀ b < ⊤, ∃ i, b < f i.fst i.snd) ↔ ∀ b < ⊤, ∃ i j, b < f i j
Module: Mathlib.Data.Set.Lattice

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

Tactic:
simp_rw [union_distrib_iInter_right]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, Ici (f i j)

Tactic:
Ici_iSup

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

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
⊢ sSup ∅ = ⊥

Tactic:
sSup_eq (by simp) (OrderTop.bddAbove _),

Goal state after:
α : Type u_5
inst✝ : CompleteLattice α
⊢ ↑(sSup (some ⁻¹' ∅)) = ⊥
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ (⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2

Tactic:
simp only [iSup_subtype', iSup_inf_iSup]

Goal state after:
α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ ⨆ i, f ↑i.1 ⊓ g ↑i.2 = ⨆ x, f (↑x).1 ⊓ g (↑x).2
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ a ∆ sSup s ≤ sSup ((fun x ↦ a ∆ x) '' s)

Tactic:
by
  simpa [symmDiff_comm] using sSup_symmDiff_le (a := a) hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
⊢ (t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s) ↔ InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)

Tactic:
refine ⟨fun ht x hx y hy (h : f _ _ = _) => ?_, fun ht x hx y hy h => ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x = y

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b ↦ (fun a ↦ f a b) '' s) x y
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
hq : 0 < q
⊢ 0 < ↑q

Tactic:
Rat.cast_def

Goal state after:
q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
hq : 0 < q
⊢ 0 < ↑q.num / ↑q.den
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
ha : a < 1
⊢ 1 < a⁻ᵐ

Tactic:
leOnePart_eq_inv.2 ha.le,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
ha : a < 1
⊢ 1 < a⁻¹
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
⊢ (mulSupport (mulSingle i a)).Subsingleton

Tactic:
classical
  rw [mulSupport_mulSingle]
  split_ifs with h <;> simp

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 1 → (n + 1) ^ 1 < (n + 1).ascFactorial 1

Tactic:
intro; contradiction

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 1 → (n + 1).ascFactorial 1 < (n + 1) ^ 1

Tactic:
intro; contradiction

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 1 → 1 ≤ n → (n + 1 - 1) ^ 1 < n.descFactorial 1

Tactic:
intro; contradiction

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 2 ≤ 1 → n.descFactorial 1 < n ^ 1

Tactic:
intro; contradiction

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

Goal state before:
pp: case case2
n✝ : ℕ
⊢ n✝.ascFactorial 1 = n✝

Tactic:
| case2 =>

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
| -(x - ↑z)

Tactic:
← fract_add_floor x

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
| -(fract x + ↑⌊x⌋ - ↑z)
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
h : k ∣ m
⊢ k * m.divExact k = m

Tactic:
apply PNat.eq; rw [mul_coe]
  change (k : ℕ) * (div m k).succ = m
  rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]

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 ℤ := ⋯
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
n : ℤ
hn : n ∈ s
⊢ a ^ n ≤ a ^ ↑k

Tactic:
rw [← zpow_natCast] at hk

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
n : ℤ
hn : n ∈ s
⊢ a ^ n ≤ a ^ ↑k
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
s t : Set P
⊢ v • s /ₛ v • t = s /ₛ t

Tactic:
by
  ext; simp [mem_sdiv, mem_smul_set]

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)

Tactic:
· intro a m ih h
    exact Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
⊢ s - t + t = s

Tactic:
ext a; simp [Nat.sub_add_cancel <| count_le_of_le _ hts]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝ : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
hab : r a✝ b✝
hst : Rel r as✝ bs✝
ih : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝ ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)

Tactic:
simpa using ih.cons hab

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

Goal state before:
pp: α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l.concat a).Nodup

Tactic:
rw [concat_eq_append]

Goal state after:
α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ ¬x ∈ xs ∪ ys
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ map f (filter p s) = filterMap (fun a ↦ if p a then some (f a) else none) s

Tactic:
by
  induction s using Multiset.induction with
  | empty => simp
  | cons a s ih =>
    simp only [filter_cons, map_add, ih, filterMap_cons, Option.map_if]; clear ih; congr
    split_ifs <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
⊢ _root_.Disjoint (map f s) (map g t) ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a ≠ g b

Tactic:
simp [disjoint_iff_ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : #(image f s) = #s
⊢ Set.InjOn f ↑s

Tactic:
rw [card_def, card_def, image, toFinset] at H
  dsimp only at H
  have : (s.1.map f).dedup = s.1.map f := by
    refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
    simp only [H, Multiset.card_map, le_rfl]
  rw [Multiset.dedup_eq_self] at this
  exact inj_on_of_nodup_map this

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ #(filter p s) = 0 ↔ ∀ x ∈ s, ¬p x

Tactic:
card_eq_zero,

Goal state after:
α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p s = ∅ ↔ ∀ x ∈ s, ¬p x
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
b : Fin (n + 1)
hb : b ≠ last n
hab : last n ≤ b
⊢ False

Tactic:
exact Nat.not_lt_of_le hab (lt_last_iff_ne_last.mpr hb)

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

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i ≤ j
⊢ ↑(j - i) < n - ↑i

Tactic:
by
  simp [sub_val_of_le hij, Nat.sub_lt_sub_right hij j.isLt]

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

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ (ofFn fun i ↦ ofFn fun j ↦ f (Fin.cast ⋯ ⟨↑i * m + ↑j, ⋯⟩)).flatten =
    (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * m + ↑j, ⋯⟩).flatten

Tactic:
Fin.cast_mk

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ cons (q 0) (tail q) j = q j

Tactic:
cases j using Fin.cases <;> simp [tail]

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

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝ : Nonempty α
H : #∅ ≤ 1
⊢ ∃ x, ∅ ⊆ {x}

pp: case refine_1.inr
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}

Tactic:
· exact ⟨Classical.arbitrary α, empty_subset _⟩

Goal state after:
case refine_1.inr
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
i : Fin n
hi : x i = x₀
h : cons x₀ x i.succ = cons x₀ x 0 → i.succ = 0
⊢ False

Tactic:
simp [hi] at h

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
⊢ tail (update q i.succ y) j = update (tail q) i y j

Tactic:
by_cases h : j = i

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : ¬j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
⊢ init (update q i.castSucc y) j = update (init q) i y j

Tactic:
by_cases h : j = i

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : ¬j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ ∃ f, map f univ = s

Tactic:
use f

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ map f univ = s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
p i : Fin (n + 1)
hi : P i
⊢ P p ∨ ∃ i, P (p.succAbove i)

Tactic:
induction i using p.succAboveCases

Goal state after:
case x
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
hi : P p
⊢ P p ∨ ∃ i, P (p.succAbove i)

case p
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
j✝ : Fin n
hi : P (p.succAbove j✝)
⊢ P p ∨ ∃ i, P (p.succAbove i)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ ↥hs.toFinset = ↑s

Tactic:
← Finset.coe_sort_coe _,

Goal state after:
α : Type u
s : Set α
hs : s.Finite
⊢ ↑↑hs.toFinset = ↑s
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
h : s.Infinite
⊢ s ≠ ∅

Tactic:
rintro rfl
    exact h finite_empty

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ countP p (n • s) = n * countP p s

Tactic:
induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
s : Multiset α
⊢ count a (n • s) = n * count a s

Tactic:
induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
hl : List.IsChain (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ Acc (List.lex_chains r) ⟨[], hl⟩

pp: case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
· apply Acc.intro; rintro ⟨_⟩ ⟨_⟩

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.IsChain (flip r) [a]
hl' : List.IsChain (flip r) []
l' : List.chains r := ⟨[], hl'⟩
⊢ Acc (List.lex_chains r) l'

pp: case cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
b : α
l : List α
hl : List.IsChain (flip r) (a :: b :: l)
hl' : List.IsChain (flip r) (b :: l)
l' : List.chains r := ⟨b :: l, hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
· apply Acc.intro; rintro ⟨_⟩ ⟨_⟩

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
b : α
l : List α
hl : List.IsChain (flip r) (a :: b :: l)
hl' : List.IsChain (flip r) (b :: l)
l' : List.chains r := ⟨b :: l, hl'⟩
⊢ Acc (List.lex_chains r) l'
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn
    · simp [← hn]
    · rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]
      exact (Nat.mod_lt _ hl).le

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

Goal state before:
pp: ι : Type u_2
G : Type u_4
inst✝ : DivisionCommMonoid G
m : Multiset ι
f : ι → G
⊢ (map (fun i ↦ (f i)⁻¹) m).prod = (map f m).prod⁻¹

Tactic:
rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).sigma fun a ↦ ↑(l₂ a)) = ↑(l₁.sigma l₂)

Tactic:
by
  rw [Multiset.sigma, List.sigma, ← coe_bind]
  simp

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn f s ↔ FactorsThrough f s.domRestrict

Tactic:
DependsOn,

Goal state after:
ι : 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) ↔ FactorsThrough f s.domRestrict