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

Goal state before:
pp: α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
hx : x ≠ y
⊢ x ∈+ l

Tactic:
by
  simpa [duplicate_cons_iff, hx.symm] using h

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

Goal state before:
pp: case slnil
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ []
⊢ x ∈+ []

Tactic:
exact hx

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

Goal state before:
pp: case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
this : l'[f 0]? = some hd
⊢ hd :: tl <+ l'

Tactic:
List.getElem?_eq_some_iff

Goal state after:
case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
this : ∃ h, l'[f 0] = hd
⊢ hd :: tl <+ l'
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ b = bs ⟨i - n, ⋯⟩

Tactic:
have := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp lt_n) lt_add
    contradiction

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

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

Tactic:
rintro (h | ⟨i, hi⟩)

Goal state after:
case inl
n : ℕ
P : Fin (n + 1) → Prop
h : P (last n)
⊢ ∃ i, P i

case inr
n : ℕ
P : Fin (n + 1) → Prop
i : Fin n
hi : P i.castSucc
⊢ ∃ i, P i
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
rintro (h | ⟨i, hi⟩)

Goal state after:
case inl
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
h : P p
⊢ ∃ i, P i

case inr
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
i : Fin n
hi : P (p.succAbove i)
⊢ ∃ i, P i
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ orderedInsert r a (b :: m) = a :: b :: m

Tactic:
rw [orderedInsert_cons_of_le]

Goal state after:
case cons.h
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ r a b
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ ∃ s', ↑s' = s

Tactic:
cases h.nonempty_fintype
  exact ⟨s.toFinset, s.coe_toFinset⟩

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
⊢ t.Infinite

Tactic:
exact infinite_of_injOn_mapsTo (fun x hx y hy => not_imp_not.1 (ht x hx y hy)) hf hs

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

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h✝ : ¬p 0
⊢ Fin.find p h = (Fin.find (fun k ↦ p k.succ) ⋯).succ

Tactic:
· grind [find_of_not_zero]

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

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑j < ↑k
⊢ (if ↑k = ↑j then op (g k.castSucc) (g k.succ) else g k.succ) = g k.succ

Tactic:
if_neg (Ne.symm <| ne_of_lt h)

Goal state after:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑j < ↑k
⊢ g k.succ = g k.succ
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : 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 : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
Finset.fold_insert ha,

Goal state after:
case insert
α : 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 : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ r c (op (f a) (fold op b f s)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : 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 : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
Finset.fold_insert ha,

Goal state after:
case insert
α : 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 : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ r c (op (f a) (fold op b f s)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.List.Range

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n + 1 - 1 → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
Nat.add_one_sub_one

Goal state after:
r : ℕ → ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ (l ++ [a]).length

Tactic:
length_append,

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ l.length + [a].length
Module: Mathlib.Data.List.Chain

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

Tactic:
apply hl

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

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ some (l.rotate n)[k] = some l[(k + n) % l.length]

Tactic:
← getElem?_eq_getElem,

Goal state after:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ (l.rotate n)[k]? = some l[(k + n) % l.length]
Module: Mathlib.Data.List.Rotate

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

Tactic:
← getElem?_eq_getElem,

Goal state after:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ (l.rotate n)[k]? = l[(k + n) % l.length]?
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ some (a :: l)[n] = some a

Tactic:
← getElem?_eq_getElem,

Goal state after:
α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ (a :: l)[n]? = some a
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : 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⟩
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ l = ↑l'

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
l : List α
h : l = []
⊢ l ~r l

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
l : List α
x : α
h : l = [x]
⊢ l ~r l

Tactic:
by rfl

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

Goal state before:
pp: case nil
α : Type u
hL : [] ≠ []
⊢ [].getLast hL :: [].dropLast ~r []

Tactic:
simp at hL

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

Goal state before:
pp: n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
⊢ (n - 1).choose l + (n - 1).choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)

Tactic:
Nat.add_one_sub_one

Goal state after:
n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
⊢ (n - 1).choose l + (n - 1).choose (l + 1) = (n - 1).choose l + (n - 1).choose (l + 1)
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : ¬z = x
⊢ count (x, y) (map (fun x ↦ (z, x)) l) = 0

Tactic:
· simp [count_eq_zero, h]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : ¬z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = 0

Tactic:
· simp [count_eq_zero, h]

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 !
⊢ k * n ! + 1 * n ! + (n * n ! - k * n !) = (n + 1)!

Tactic:
factorial_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 !
⊢ k * n ! + 1 * n ! + (n * n ! - k * n !) = (n + 1) * n !
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map (Prod.map f f) l.offDiag = (map f l).offDiag

Tactic:
simp [offDiag, map_flatMap, zipIdx_map, flatMap_map, eraseIdx_map, Function.comp_def]

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1)

Tactic:
by
  rw [← Nat.mul_left_inj (Nat.mul_ne_zero (factorial_ne_zero (m * n)) (factorial_ne_zero n))]
  set p := n - 1
  have hp : n = p + 1 := (succ_pred_eq_of_ne_zero hn).symm
  simp only [hp, add_succ_sub_one]
  calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia

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

Goal state before:
pp: a b c : ℕ
⊢ a.choose c ≤ (a + b).choose c

Tactic:
induction b with

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)

Tactic:
by
  contrapose! +distrib; exact Set.infinite_prod

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑x ⋯

Tactic:
apply InjOn.image_iInter_eq

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ InjOn f (⋃ i, s ↑i ⋯)
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
hy : y ∈ closure s
⊢ p x y hx hy

Tactic:
by
  induction hx using closure_induction with
  | mem z hz => induction hy using closure_induction with
    | mem _ h => exact mem _ _ hz h
    | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ hy h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
have hk := congr_fun h k

Goal state after:
case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹

Tactic:
by
      simp_rw [← image_inv_eq_inv]
      exact image_image2_antidistrib mul_inv_rev

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

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
induction x using dense_induction s with
  | closure => exact closure
  | mem x hx => exact mem x hx
  | one => exact one
  | mul _ _ h₁ h₂ => exact mul _ _ h₁ h₂

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ↑H = ↑⊤ ↔ ↑H = Set.univ

Tactic:
by rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ (∀ (x : M), x ∈ S ↔ x ∈ ⊥) ↔ ∀ x ∈ S, x = 1

Tactic:
by simp +contextual [iff_def, S.one_mem]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
x✝ : n % 2 = 0 ∨ n % 2 = 1
⊢ n.succ.testBit 0 = !n.testBit 0

Tactic:
cases mod_two_eq_zero_or_one n with

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x

Tactic:
rw [conjugatesOfSet, Set.mem_iUnion₂]

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ (∃ i, ∃ (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) ×' α i
h : Lex r₁ s₁ a b
⊢ Lex r₂ s₂ a b

Tactic:
obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h

Goal state after:
case left
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ ⟨a₁✝, a⟩ ⟨a₂✝, b⟩

case right
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i : ι
b₁✝ b₂✝ : α i
hab : s₁ i b₁✝ b₂✝
⊢ Lex r₂ s₂ ⟨i, b₁✝⟩ ⟨i, b₂✝⟩
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (a m : α), m ∈ foldl (argAux r) (some a) l → m ∈ a :: l) →
      ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l ++ [a]) → m ∈ a_2 :: (l ++ [a])

Tactic:
intro _ _ _ _
    simp only [foldl_append, foldl_cons, foldl_nil, argAux]
    cases _ : foldl _ _ _ <;> grind

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (a ⊔ b) = f b

Tactic:
sup_eq_right.2 h

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f b = f b
Module: Mathlib.Data.Finset.Lattice.Union

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
a✝ : β
⊢ a✝ ∈ s.sup t ↔ a✝ ∈ s.biUnion t

Tactic:
mem_sup,

Goal state after:
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
a✝ : β
⊢ (∃ i ∈ s, a✝ ∈ t i) ↔ a✝ ∈ s.biUnion t
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
ih : map pure l <+ l.sublists
⊢ [] ++ [a] = pure a

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ map (fun x ↦ [x]) s.reverse ++ map (cons a) (sublistsLen 0 s) = map (fun x ↦ [x]) s.reverse ++ map (fun x ↦ [x]) [a]

Tactic:
sublistsLen_zero

Goal state after:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ map (fun x ↦ [x]) s.reverse ++ map (cons a) [[]] = map (fun x ↦ [x]) s.reverse ++ map (fun x ↦ [x]) [a]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ (sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)).length = (a :: l).length.choose (n + 1)

Tactic:
length_append,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ (sublistsLen (n + 1) l).length + (map (cons a) (sublistsLen n l)).length = (a :: l).length.choose (n + 1)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
⊢ ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (Function.swap R) a_1 b

Tactic:
rintro l₁ sl₁ x l₂ _ rfl

Goal state after:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₁ : List α
sl₁ : l₁ <+ l
l₂ : List α
a✝ : l₂ <+ l
⊢ Lex (Function.swap R) l₁ (a :: l₂)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (a :: l).sublists' ~ l.sublists ++ map (cons a) l.sublists

Tactic:
rw [sublists'_cons]
  exact Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : (⋃ a ∈ s, a).Pairwise r
a : Set α
ha : a ∈ s
⊢ a ⊆ a

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ image some (eraseNone s) = s.erase none

Tactic:
ext (_ | x) <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ insertNone (eraseNone s) = insert none s

Tactic:
ext (_ | x) <;> simp

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ a \ f b) = a \ s✝.inf f
⊢ ((cons a✝ s✝ h✝).sup fun b ↦ a \ f b) = a \ (cons a✝ s✝ h✝).inf f

Tactic:
rw [sup_cons, inf_cons, h, sdiff_inf]

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

Goal state before:
pp: case insert.inr.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s

Tactic:
sup_eq_right.mpr ha

Goal state after:
case insert.inr.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ s.sup f ∈ f '' insert a ↑s
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i

Tactic:
induction s using cons_induction

Goal state after:
case empty
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ ∅.sup f ↔ ∃ i ∈ ∅, a ∈ f i

case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : a ∈ s✝.sup f ↔ ∃ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).sup f ↔ ∃ i ∈ cons a✝¹ s✝ h✝, a ∈ f i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (a ∈ s.sup fun b ↦ {f b}) ↔ a ∈ image f s

Tactic:
mem_sup,

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (∃ i ∈ s, a ∈ {f i}) ↔ a ∈ image f s
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
h : i ∉ s
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(⨅ (_ : i ∈ s), f i)

Tactic:
· simp [iInf_neg h]

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

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, s ⊆ t

Tactic:
rw [← hs.coe_toFinset, sUnion_eq_biUnion] at hsc

Goal state after:
α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : ↑hs.toFinset ⊆ ⋃ i ∈ c, i
⊢ ∃ t ∈ c, s ⊆ t
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)

Tactic:
· rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
    · exact mk_covBy_mk_iff_left.2 h
    · exact mk_covBy_mk_iff_right.2 h

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ s.sigma t = s.biUnion fun i ↦ map (Embedding.sigmaMk i) (t i)

Tactic:
by
  ext ⟨x, y⟩
  simp [and_left_comm]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
hx : x ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd
⊢ x ∈ f a b

Tactic:
exact hx

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

Tactic:
obtain rfl | hn := s.eq_empty_or_nonempty
  · use ∅; simpa
  · obtain ⟨a, ha⟩ := hs.exists_maximal hn
    use {a}
    suffices IsTop a by simpa [IsCofinal]
    intro b
    obtain ⟨c, hc, hbc⟩ := hs' b
    exact hbc.trans (ha.le hc)

Goal state after: