mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
by_cases h : b ∈ l₂

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

case neg
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t = s + t

Tactic:
apply _root_.le_antisymm
  · rw [union_add_distrib]
    refine union_le (Multiset.add_le_add_left inter_le_right) ?_
    rw [Multiset.add_comm]
    exact Multiset.add_le_add_right inter_le_left
  · rw [Multiset.add_comm, add_inter_distrib]
    refine le_inter (Multiset.add_le_add_right le_union_right) ?_
    rw [Multiset.add_comm]
    exact Multiset.add_le_add_right le_union_left

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

Goal state before:
pp: case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
count_eq_zero_of_notMem H,

Goal state after:
case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ count (f x) (map f s) = 0
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t

Tactic:
← inter_eq_zero_iff_disjoint,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ s ∩ t = 0
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
xs : List α
x : α
⊢ xs <:+: [x] ↔ xs = [] ∨ xs = [x]

Tactic:
by
  match xs with
  | [] => simp
  | [_] => simp [List.singleton_infix_singleton_iff]
  | _ :: _ :: _ =>
    constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
⊢ RightInverse (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩

Tactic:
rintro (_ | y)

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) none) = none

case some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
y : ↥t
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) (some y)) = some y
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ _root_.Pairwise (r on fun a_1 ↦ f ↑a_1) ↔ _root_.Pairwise (r on fun a ↦ f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

Tactic:
simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ ((↑s).Pairwise (r on f) ∧ ∀ b ∈ ↑s, a ≠ b → (r on f) a b ∧ (r on f) b a) ↔
    (↑s).Pairwise (r on f) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
⊢ Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
by
  simp only [disjoint_left, mem_union, or_imp, forall_and]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
by
  rw [Finset.Nontrivial, coe_toFinset]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 0 < n

Tactic:
Nat.pos_iff_ne_zero

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ n ≠ 0
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ (∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a) → a ∈ s

Tactic:
· rintro ⟨i, hi, rfl⟩; apply hf'

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s

Tactic:
classical
  rw [← card_union_of_disjoint (disjoint_filter_filter_not _ _ _), filter_union_filter_not_eq]

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

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
r : Fin n
⊢ append u v (natAdd m r) = (u ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
· exact (Fin.cast hv r).elim0

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ append u v = u ∘ Fin.cast ⋯

Tactic:
by
  refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
  · rw [append_left, Function.comp_apply]
    refine congr_arg u (Fin.ext ?_)
    simp
  · exact (Fin.cast hv r).elim0

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

Goal state before:
pp: case mp.cons_cons.refine_1
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (a b : ℕ), ((if a = 0 then 0 else (f a.pred).succ) ≤ if b = 0 then 0 else (f b.pred).succ) ↔ a ≤ b

pp: case mp.cons_cons.refine_2
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ),
    (a✝¹ :: l₁✝)[ix]? =
      (a✝¹ ::
          l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ?mp.cons_cons.refine_1) ix]?

Tactic:
· rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]

Goal state after:
case mp.cons_cons.refine_2
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ),
    (a✝¹ :: l₁✝)[ix]? =
      (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) ix]?
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ P (u n) (u '' Iio n)

Tactic:
convert! hc (u '' Iio n) ((finite_lt_nat _).image _)

Goal state after:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ u n = c (u '' Iio n)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ fold op b f (cons a s h) = op (f a) (fold op b f s)

Tactic:
dsimp only [fold]

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Tactic:
change _ ≥ _ ↔ _

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Tactic:
change _ ≥ _ ↔ _

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold max b f s ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.reverse.head ⋯)

Tactic:
exact h.rel_head_tail (by rwa [tail_reverse, mem_reverse])

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

Goal state before:
pp: α : Type u
inst✝ : LT α
l l' : List α
⊢ l.lt l' ↔ Lex (fun x1 x2 ↦ x1 < x2) l l'

Tactic:
by
  rw [List.lt]

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

Goal state before:
pp: case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
← List.cons_head!_tail hl',

Goal state after:
case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) (l'.head! :: l'.tail) l
hl : ¬l = []
⊢ l'.head! ≤ l.head!
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
have H : IsChain (flip (flip r)) l := h
  replace H := (isChain_reverse.mpr H).induction _ _ (fun _ _ h ↦ carries h)
  grind

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

Goal state before:
pp: case succ
α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f l[i] = l[i + 1]

Tactic:
rw [List.isChain_iff_getElem] at hl

Goal state after:
case succ
α : Type u_3
f : α → α
l : List α
hl : ∀ (i : ℕ) (_hi : i + 1 < l.length), f l[i] = l[i + 1]
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f l[i] = l[i + 1]
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Tactic:
conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]

Goal state after:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = n % l.length + m - l.length
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset β
t : Finset α
f : α → Finset β
hf : (↑t).PairwiseDisjoint f
⊢ Disjoint s (t.disjiUnion f hf) ↔ ∀ i ∈ t, Disjoint s (f i)

Tactic:
by
  simpa only [_root_.disjoint_comm] using disjoint_disjiUnion_left t f hf s

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
⊢ (cons m a (φ b) fun a' ha' ↦ φ (f a' ha')) = fun a' ha' ↦ φ (cons m a b f a' ha')

Tactic:
ext a' ha'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
ha' : a' ∈ a ::ₘ m
⊢ cons m a (φ b) (fun a' ha' ↦ φ (f a' ha')) a' ha' = φ (cons m a b f a' ha')
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !

Tactic:
rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]; exact Nat.dvd_mul_left _ _

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ DecidablePred fun x ↦ x ∈ s ^ 0

Tactic:
simp only [pow_zero, mem_one]
    infer_instance

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
one_mem : 1 ∈ s
x : G
hx : x ∈ s
⊢ x⁻¹ ∈ s

Tactic:
by simpa using hs 1 one_mem x hx

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ map K.subtype (H.subgroupOf K) = H

Tactic:
rwa [subgroupOf_map_subtype, inf_eq_left]

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f (x / y) = 1

Tactic:
div_eq_mul_inv,

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f (x * y⁻¹) = 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y ↔ y⁻¹ * x ∈ f.ker

Tactic:
constructor <;> intro h
  · rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
  · rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
rw [← op_inj, op_unop, op_closure]
  simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
rw [← op_inj, op_unop, op_closure]
  simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
hf : Injective ⇑f
M' : Submonoid M
⊢ Injective ⇑(f.submonoidMap M')

Tactic:
by
  grind [Injective, submonoidMap_apply_coe]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
rw [← op_inj, op_unop, op_closure]
  simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g : G
a : ℤ
⊢ ((fun x ↦ g ^ x) a)⁻¹ ∈ Set.range fun x ↦ g ^ x

Tactic:
exact ⟨-a, zpow_neg ..⟩

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: ⊢ Countable ℕ+

Tactic:
delta PNat

Goal state after:
⊢ Countable { n // 0 < n }
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, H.Characteristic
⊢ (sSup Hs).Characteristic

Tactic:
by
  simp [sSup_eq_iSup', characteristic_iSup, h]

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
xs : List M
x : M
h₁ : x ∈ xs
⊢ x ≤ xs.prod

Tactic:
by
  induction xs with
  | nil => simp at h₁
  | cons y ys ih =>
    simp only [mem_cons] at h₁
    rcases h₁ with (rfl | h₁)
    · simp
    · specialize ih h₁
      simp only [List.prod_cons]
      exact le_mul_left ih

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Symm r
inst✝ : ∀ (i : ι), Std.Symm (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
⊢ Lex r s ⟨j✝, b⟩ ⟨i✝, a⟩

pp: case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Symm r
inst✝ : ∀ (i : ι), Std.Symm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ Lex r s ⟨i✝, b⟩ ⟨i✝, a⟩

Tactic:
· exact Lex.left _ _ (symm hij)

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Symm r
inst✝ : ∀ (i : ι), Std.Symm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ Lex r s ⟨i✝, b⟩ ⟨i✝, a⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mp
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

Tactic:
rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)

Goal state after:
case mp.left
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r a₁✝ a₂✝
⊢ r ⟨a₁✝, a⟩.fst ⟨a₂✝, b⟩.fst ∨ ∃ h, s ⟨a₂✝, b⟩.fst (h ▸ ⟨a₁✝, a⟩.snd) ⟨a₂✝, b⟩.snd

case mp.right
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
b₁✝ b₂✝ : α i
hab : s i b₁✝ b₂✝
⊢ r ⟨i, b₁✝⟩.fst ⟨i, b₂✝⟩.fst ∨ ∃ h, s ⟨i, b₂✝⟩.fst (h ▸ ⟨i, b₁✝⟩.snd) ⟨i, b₂✝⟩.snd
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ decode n = some (e.symm (ofNat α n))

Tactic:
decode_ofEquiv e

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Option.map (⇑e.symm) (decode n) = some (e.symm (ofNat α n))
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ some (ofNat (Sigma γ) n) = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
rw [← decode_eq_ofNat, decode_sigma_val]

Goal state after:
α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ((decode (unpair n).1).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeInf β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (⇑f ⊓ ⇑g) ⊤ = ⊤

Tactic:
Pi.inf_apply,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeInf β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ f ⊤ ⊓ g ⊤ = ⊤
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
⊢ f x < f y

Tactic:
rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ f x < f y
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ map pure l <+ l.sublists

Tactic:
by
  induction l using reverseRecOn <;> simp only [map, map_append, sublists_concat]
  · simp only [sublists_nil, sublist_cons_self]
  case append_singleton l a ih =>
    exact ((append_sublist_append_left _).2 <|
              singleton_sublist.2 <| mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by rfl⟩).trans
          ((append_sublist_append_right _).2 ih)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
⊢ ∃ t, ∀ (a : α), f a ≤ t.sup f

Tactic:
by
  cases isEmpty_or_nonempty α
  · exact ⟨⊥, isEmptyElim⟩
  obtain ⟨_, ⟨t, rfl⟩, ht⟩ := wellFounded_gt.has_min _ (Set.range_nonempty (sup · f))
  refine ⟨t, fun a ↦ ?_⟩
  classical
  have := ht (f a ⊔ t.sup f) ⟨insert a t, by simp⟩
  rwa [right_lt_sup, not_not] at this

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ s.sup f ⊓ a = s.sup fun i ↦ f i ⊓ a

Tactic:
by
  rw [_root_.inf_comm, s.sup_inf_distrib_left]
  simp_rw [_root_.inf_comm]

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

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
exact ciSup_le fun x => le_ciSup_of_le B x (H x)

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝⁴ : Finite ι
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirectedOrder ι'
inst✝ : Order.Frame α
f : ι → ι' → α
hf : ∀ (i : ι), Monotone (f i)
⊢ ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j

Tactic:
by
  simpa only [iInf_univ] using finite_univ.iSup_biInf_of_monotone fun i _ => hf i

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

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
a✝ : α
⊢ (a✝ ∈ range fun i ↦ ⨅ (_ : i ∈ s), f i) → a✝ ∈ f '' s ∪ {sInf ∅}

Tactic:
simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]

Goal state after:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
a✝ : α
⊢ ∀ (x : ι), (if x ∈ s then f x else sInf ∅) = a✝ → a✝ = sInf ∅ ∨ ∃ x ∈ s, f x = a✝
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → a j = b j

Tactic:
by
  obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_covBy h
  exact ⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b x : ℕ
⊢ x ∈ (range' a b).toFinset ↔ x ∈ Ico a (a + b)

Tactic:
rw [List.mem_toFinset, List.mem_range'_1, Finset.mem_Ico]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm : m ≥ n
⊢ P m

Tactic:
rcases hm.eq_or_lt with rfl | hm

Goal state after:
case inl
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
hm : n ≥ n
⊢ P n

case inr
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm✝ : m ≥ n
hm : n < m
⊢ P m
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ ⦃y : ℕ⦄, (fun x ↦ x ∈ {x | P x}) y → m ≤ y → y ≤ m
⊢ False

Tactic:
obtain ⟨y, hl, hy⟩ := hi m (le_of_not_gt <| not_lt_iff_le_imp_ge.2 <| hm hs) hP

Goal state after:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ ⦃y : ℕ⦄, (fun x ↦ x ∈ {x | P x}) y → m ≤ y → y ≤ m
y : ℕ
hl : m < y
hy : P y
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a < b
⊢ Iio a ⊂ Iio b

Tactic:
simpa [← coe_ssubset] using Set.Iio_ssubset_Iio h

Goal state after: