mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
simp_rw [isLUB_iff_le_iff, mem_upperBounds] at ha₀ hb₀

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SupSet α
s : Set α
⊢ sSup s = ⨆ a, ↑a

Tactic:
rw [iSup, Subtype.range_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
⊢ CompleteLattice α

Tactic:
let top := e.top

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
⊢ CompleteLattice α
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ Iic (⨅ a ∈ s, a) = ⋂ a ∈ s, Iic a

Tactic:
Iic_iInf₂

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ ⋂ i ∈ s, Iic i = ⋂ a ∈ s, Iic a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
a : α
f : (i : ι) → κ i → α
⊢ Disjoint a (⨆ i, ⨆ j, f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)

Tactic:
simp_rw [disjoint_iSup_iff]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
⊢ (sInf s)ᶜ = ⨆ i ∈ s, iᶜ

Tactic:
by simp only [sInf_eq_iInf, compl_iInf]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ z ∈ s

Tactic:
rwa [hz]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
f : ι → M
g : ι → N
x : ι
⊢ (x ∈ mulSupport fun x ↦ (f x, g x)) ↔ x ∈ mulSupport f ∪ mulSupport g

Tactic:
by
    simp only [mulSupport, not_and_or, mem_union, mem_ofPred_eq, Prod.mk_eq_one, Ne]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ = b⁺ᵐ / b⁻ᵐ

Tactic:
hpos,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ b⁺ᵐ / a⁻ᵐ = b⁺ᵐ / b⁻ᵐ
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!

Tactic:
rw [factorial_succ (i + _), Nat.add_mul, Nat.one_mul]
  have := (i + n).self_le_factorial
  refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_) <;> lia

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑(negOfNat n) / ↑d⌉ = negOfNat (n / d)

Tactic:
@negOfNat_eq (n / d),

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑(negOfNat n) / ↑d⌉ = -ofNat (n / d)
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: case empty
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
t : Multiset α
h : Rel r 0 t
⊢ countP (r x) 0 = countP (r x) t

Tactic:
| empty =>

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t → a ∈ t ∧ s = t.erase a

pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = t.erase a → a ::ₘ s = t

Tactic:
· rintro rfl
    exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = t.erase a → a ::ₘ s = t
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
u s : Multiset α
⊢ s - 0 ≤ u ↔ s ≤ u + 0

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ Rel r s u

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
⊢ map f (erase 0 x) = (map f 0).erase (f x)

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x : α
h : x ∈ 0
⊢ map f (erase 0 x) = (map f 0).erase (f x)

Tactic:
| empty =>

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

Goal state before:
pp: case cons.inr
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
hxy : y ≠ x
h : x ∈ s
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
rw [s.erase_cons_tail hxy, map_cons, map_cons, ih h, erase_cons_tail_of_mem (mem_map_of_mem f h)]

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ ∃ a, map f a = 0

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ (a : α), a ∈ 0 → q a
⊢ p (foldr f x 0)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x✝ : α
⊢ List.count x✝ (l₁.bagInter l₂) = List.count x✝ (l₂.bagInter l₁)

Tactic:
by simp [List.count_bagInter, Nat.min_comm]

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ 0 ∩ t ≤ t

Tactic:
| empty =>

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s ≤ a ::ₘ t ∩ u.erase a

Tactic:
← erase_le_iff_le_cons

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s.erase a ≤ t ∩ u.erase a
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s

Tactic:
split_ifs with h
  · rw [filter_cons_of_pos _ h, singleton_add]
  · rw [filter_cons_of_neg _ h, Multiset.zero_add]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)

pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a

Tactic:
· simp [-Bool.not_eq_true, -not_and]

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a
Module: Mathlib.Data.Multiset.Filter

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

Tactic:
| empty =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ Set.SurjOn toFinset {l | l.Nodup} Set.univ

Tactic:
rintro ⟨⟨l⟩, hl⟩ _

Goal state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
val✝ : Multiset α
l : List α
hl : Multiset.Nodup (Quot.mk (⇑(isSetoid α)) l)
a✝ : { val := Quot.mk (⇑(isSetoid α)) l, nodup := hl } ∈ Set.univ
⊢ { val := Quot.mk (⇑(isSetoid α)) l, nodup := hl } ∈ toFinset '' {l | l.Nodup}
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ _root_.Disjoint s (ndinsert a t) ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
rw [_root_.disjoint_comm, disjoint_ndinsert_left]; tauto

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s ∩ t).Nodup

Tactic:
by
  rw [← ndinter_eq_inter d]
  exact d.filter _

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

Goal state before:
pp: case empty
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
nd : Nodup 0
⊢ motive { val := 0, nodup := nd }

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
hs : ∅.Nonempty
⊢ motive ∅ hs

Tactic:
| empty =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
⊢ Disjoint (s.erase a) (insert a t) ↔ Disjoint s t

Tactic:
by
  rw [disjoint_erase_comm, erase_insert ha]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
⊢ n ≠ 0 ∧ x = a ↔ x ∈ if n = 0 then ∅ else {a}

Tactic:
split_ifs with hn

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
hn : n = 0
⊢ n ≠ 0 ∧ x = a ↔ x ∈ ∅

case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
hn : ¬n = 0
⊢ n ≠ 0 ∧ x = a ↔ x ∈ {a}
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ f.symm.symm x ∈ map f.toEmbedding s

Tactic:
by simp [hx]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
A : Fintype ↑∅ := Fintype.ofIsEmpty
⊢ s.toFinset = ∅ ↔ s = ∅

Tactic:
← toFinset_empty,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
A : Fintype ↑∅ := Fintype.ofIsEmpty
⊢ s.toFinset = ∅.toFinset ↔ s = ∅
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Option β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f_inj : ∀ (a a' : α) (b : β), f a = some b → f a' = some b → a = a'
s : List α
⊢ (List.filterMap f s).toFinset = filterMap f s.toFinset f_inj

Tactic:
by
  simp [← Finset.coe_inj]

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

Goal state before:
pp: n m : ℕ
⊢ Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨castLEEmb h⟩⟩
  induction n generalizing m with
  | zero => exact m.zero_le
  | succ n ihn =>
    obtain ⟨e⟩ := h
    rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
      with ⟨m, rfl⟩
    refine Nat.succ_le_succ <| ihn ⟨?_⟩
    refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
      fun i j h ↦ ?_⟩
    simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h

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

Goal state before:
pp: case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1

pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Tactic:
· exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)

Goal state after:
case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i < j
⊢ (j - i).castLT ⋯ ≠ 0

Tactic:
by
  refine Ne.symm (ne_of_val_ne ?_)
  simp [coe_sub_iff_le.mpr (Fin.le_of_lt hij)]
  lia

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a < a.succ.castPred ha

Tactic:
by rw [lt_castPred_succ_iff, le_def]

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
⊢ a.pred h₁ < a.castPred h₂

Tactic:
pred_lt_castPred_iff,

Goal state after:
n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
⊢ a ≤ a
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
← succAbove_zero,

Goal state after:
n : ℕ
⊢ Set.range (succAbove 0) = {0}ᶜ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
by
  rcases i.le_or_gt (castSucc j) with (h | h)
  · rw [succAbove_of_le_castSucc _ _ h, succAbove_castSucc_of_le _ _ h, succ_castSucc]
  · rw [succAbove_of_castSucc_lt _ _ h, succAbove_castSucc_of_lt _ _ h]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ snoc p x i.castSucc = p i

Tactic:
simp only [snoc, val_castSucc, is_lt, dite_true]

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ cast ⋯ (p (i.castSucc.castLT ⋯)) = p i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Tactic:
simp [h, snoc, castSucc_castLT]

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

Goal state before:
pp: case last.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h : snoc x x₀ (last n) = snoc x x₀ j.castSucc
⊢ last n = j.castSucc

Tactic:
simp only [snoc_castSucc, snoc_last] at h
      rw [h] at hx₀
      apply hx₀.elim (Set.mem_range_self j)

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

Goal state before:
pp: n : ℕ
α : Type u_3
f : Fin (n + 1) → α
x✝ : Fin n
⊢ (last n).removeNth f x✝ = init f x✝

Tactic:
simp [init, removeNth]

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ h.toFinset = s.toFinset

Tactic:
Finite.toFinset,

Goal state after:
α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ s.toFinset = s.toFinset
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: case empty
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
hs : (↑∅).Finite
⊢ motive (↑∅) hs

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s : Finset α
c : β
h : op c (op b c) = op b c
hd : Decidable (∅ = ∅)
⊢ fold op b (fun x ↦ c) ∅ = if ∅ = ∅ then b else op b c

Tactic:
| empty =>

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ ∃ u, ↑u ⊆ s ∧ InjOn f ↑u ∧ image f u = t

Tactic:
refine ⟨(Finite.of_finite_image (by simp [himg]) hf).toFinset, by simpa, by simpa, ?_⟩

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ image f ⋯.toFinset = t
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i ↦ if p i then f i else g i) ∅ = op (fold op b f (filter p ∅)) (fold op b g ({i ∈ ∅ | ¬p i}))

Tactic:
| empty =>

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

Goal state before:
pp: n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
⊢ (find? p).get ⋯ = Fin.find (fun x ↦ p x = true) ⋯

Tactic:
by
  simp_rw [find?_eq_dite, Option.get_dite]

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∧ ∀ x ∈ ∅, r c (f x)

Tactic:
| empty =>

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

Goal state before:
pp: case inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x < ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

pp: case inr.inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x = ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

pp: case inr.inr
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑j < ↑x
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
· simp only [Function.comp_apply, contractNth_apply_of_lt, h]

Goal state after:
case inr.inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x = ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

case inr.inr
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑j < ↑x
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∨ ∃ x ∈ ∅, r c (f x)

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
⊢ fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton ∅ = ∅

Tactic:
| empty =>

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

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (head :: head' :: tail)

Tactic:
refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
    apply h
    rw [eq, cons_append]

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

Goal state before:
pp: case empty
M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
hs : 0 ≠ ∅
p_s : ∀ (a : M), a ∈ 0 → p a
⊢ p (prod 0)

Tactic:
| empty =>

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : ¬([] = l₁ ∨ [] ∈ l₂ :: L)
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Tactic:
not_or,

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : ¬[] = l₁ ∧ ¬[] ∈ l₂ :: L
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬([] = l₂ ∨ [] ∈ L)
⊢ (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Tactic:
not_or,

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] = l₂ ∧ ¬[] ∈ L
⊢ (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
⊢ f 0 = g 0

Tactic:
simp only [_root_.map_zero]

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
⊢ f 0 = g 0

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → β
⊢ map f (join 0) = (map (map f) 0).join

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : CommMonoid α
⊢ (join 0).prod = (map prod 0).prod

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p (join 0) = (map (filter p) 0).join

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → Option β
⊢ filterMap f (join 0) = (map (filterMap f) 0).join

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p 0 = bind 0 fun a ↦ if p a then {a} else 0

Tactic:
| empty =>

Goal state after: