mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ (↑hs.toFinset).Nonempty ↔ s.Nonempty

Tactic:
Finite.coe_toFinset

Goal state after:
α : Type u
s : Set α
hs : s.Finite
⊢ s.Nonempty ↔ s.Nonempty
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl : ∀ (a : α), a ∈ x :: xs → ∀ (b : α), b ∈ x :: xs → (r a b ↔ s (f a) (f b))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))

Tactic:
List.forall_mem_cons,

Goal state after:
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    ∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x)) ∧ ∀ (x : α), x ∈ xs → (r x_1 x ↔ s (f x_1) (f x))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ ↑hs.toFinset ⊆ ↑t ↔ s ⊆ ↑t

Tactic:
Finite.coe_toFinset

Goal state after:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ s ⊆ ↑t ↔ s ⊆ ↑t
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ ↑hs.toFinset ⊂ ↑t ↔ s ⊂ ↑t

Tactic:
Finite.coe_toFinset

Goal state after:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ s ⊂ ↑t ↔ s ⊂ ↑t
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ ↑s ⊆ ↑ht.toFinset ↔ ↑s ⊆ t

Tactic:
Finite.coe_toFinset

Goal state after:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ ↑s ⊆ t ↔ ↑s ⊆ t
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ ↑s ⊂ ↑ht.toFinset ↔ ↑s ⊂ t

Tactic:
Finite.coe_toFinset

Goal state after:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ ↑s ⊂ t ↔ ↑s ⊂ t
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
p : Finset α → Prop
h : ∀ (s : Set α) (hs : s.Finite), p hs.toFinset
s : Finset α
⊢ p s

Tactic:
by simpa using h s s.finite_toSet

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

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).Finite

Tactic:
Set.Finite

Goal state after:
α : Type u
s t : Set α
hs : Finite ↑s
ht : Finite ↑t
⊢ (s ∪ t).Finite
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case H₁
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

pp: case H₂
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ Pairwise (fun x y ↦ x ≠ y → R x y) l

Tactic:
· exact fun _ _ ↦ absurd rfl

Goal state after:
case H₂
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ Pairwise (fun x y ↦ x ≠ y → R x y) l
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l hl, IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b

Tactic:
rcases exists_isChain_cons_of_relationReflTransGen h with ⟨l, _⟩

Goal state after:
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
l : List α
h✝ : IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
⊢ ∃ l hl, IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
exact _root_.trans (List.sum_eq_zero fun n hn => by grind) (by simp [hp])

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

Goal state before:
pp: α : 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
| (n + m) % l.length

Tactic:
← mod_add_mod,

Goal state after:
α : 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
| (n % l.length + m) % l.length
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_8
inst✝¹ : FunLike F M Nᵐᵒᵖ
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ (map MulOpposite.unop (map (⇑f) l)).reverse.prod = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod

Tactic:
List.map_map

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_8
inst✝¹ : FunLike F M Nᵐᵒᵖ
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)

Tactic:
rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]

Goal state after:
α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (List.map f (m.toList.erase a)).prod = (List.map f m.toList).prod

Tactic:
List.prod_map_erase f (mem_toList.2 h)

Goal state after:
ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ (List.map f m.toList).prod = (List.map f m.toList).prod
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = (↑(List.map ofList (List.map f l))).join

Tactic:
List.map_map

Goal state after:
α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = (↑(List.map (ofList ∘ f) l)).join
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
x : α × α
⊢ x ∈ l.offDiag ↔ ∃ i x_1 j x_2, i ≠ j ∧ l[i] = x.fst ∧ l[j] = x.snd

Tactic:
rcases x with ⟨x, y⟩

Goal state after:
α : Type u_1
l : List α
x y : α
⊢ (x, y) ∈ l.offDiag ↔ ∃ i x_1 j x_2, i ≠ j ∧ l[i] = (x, y).fst ∧ l[j] = (x, y).snd
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case pos
α : 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) = count y l

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:
· rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]

Goal state after:
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
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
x : α × α
⊢ x ∈ l.offDiag ↔ x.fst ∈ l ∧ x.snd ∈ l ∧ x.fst ≠ x.snd

Tactic:
rcases x with ⟨x, y⟩

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (x, y) ∈ l.offDiag ↔ (x, y).fst ∈ l ∧ (x, y).snd ∈ l ∧ (x, y).fst ≠ (x, y).snd
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
x✝¹ x✝ : Finset α
⊢ x✝¹ ⊆ x✝ → x✝¹.diag ⊆ x✝.diag

Tactic:
by simp [diag]

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.offDiag = ∅

Tactic:
simp [← Finset.card_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ Function.RightInverse (Quotient.lift id ⋯) ConjClasses.mk

Tactic:
Function.RightInverse,

Goal state after:
α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ Function.LeftInverse ConjClasses.mk (Quotient.lift id ⋯)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
hf : Bijective f
s : (i : ι) → κ i → Set α
⊢ f '' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f '' s i j

Tactic:
simp_rw [image_iInter hf]

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
⊢ z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i

Tactic:
hz

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
⊢ w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
⊢ z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
hz

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
⊢ ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mem
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : x ∈ closure k
z : G
hz : z ∈ k
⊢ p x z hx ⋯

Tactic:
induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | inv _ _ h => exact inv_left _ _ _ _ h

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

Goal state before:
pp: case refine_1.refine_4
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∀ x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i

Tactic:
· rintro _ _ ⟨i, hi', hi⟩
      exact ⟨i, hi', inv_mem hi⟩

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

Goal state before:
pp: case refine_3
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : C),
    x ∈ closure (↑s ∪ ↑t) →
      y ∈ closure (↑s ∪ ↑t) →
        (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y

Tactic:
rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩

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

Goal state before:
pp: case neg
m n : ℕ
h✝ : ¬m < n
⊢ m + n ≤ m * m + (m + n)

Tactic:
· exact Nat.le_add_left _ _

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mpr.of_mul
α : Type u_1
β : Type u_2
f : α → β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
a : α
⊢ ∃ a_1, (map f) a_1 = of (f a) * tail

Tactic:
rcases ih with ⟨b, rfl⟩

Goal state after:
case mpr.of_mul
α : Type u_1
β : Type u_2
f : α → β
a : α
b : FreeMonoid α
⊢ ∃ a_1, (map f) a_1 = of (f a) * (map f) b
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ x * y = y * x

Tactic:
rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      simpa

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

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ ∀ (x : M), x ∈ l → x ≤ l.prod

Tactic:
by
  induction l
  · simp
  simp_rw [prod_cons, forall_mem_cons] at hl₁ ⊢
  constructor
  case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)
  case cons.right hd tl ih => exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
⊢ m ∈ some n

Tactic:
have :=
          Nat.le_antisymm (hma n (argmax_mem harg) (le_of_mem_argmax hml harg))
            (index_of_argmax harg hml (ham _ (argmax_mem harg)))

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
this : idxOf m l = idxOf n l
⊢ m ∈ some n
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Max α
inst✝⁶ : Bot α
inst✝⁵ : Max β
inst✝⁴ : Bot β
inst✝³ : Max γ
inst✝² : Bot γ
inst✝¹ : Max δ
inst✝ : Bot δ
f g : SupBotHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

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

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux' l).revzip
⊢ x.1 + x.2 = ↑l

Tactic:
by
  rw [revzip, powersetAux', ← map_reverse, zip_map, ← revzip, List.mem_map] at h
  simp only [Prod.map_apply, Prod.exists] at h
  rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
  exact Quot.sound (revzip_sublists' _ _ _ h)

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

Goal state before:
pp: case cons_cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' ++ map (List.cons a) l₁✝.sublists' <+ l₂✝.sublists' ++ map (List.cons a) l₂✝.sublists'

Tactic:
exact ih.append (ih.map _)

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (cons a✝ s✝ h✝).sup (f ⊔ g) = (cons a✝ s✝ h✝).sup f ⊔ (cons a✝ s✝ h✝).sup g

Tactic:
rw [sup_cons, sup_cons, sup_cons, ih]
    exact sup_sup_sup_comm _ _ _ _

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

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ s ∈ t.powerset ↔ s ⊆ t

Tactic:
cases s
  simp [powerset, mem_mk, mem_pmap, mk.injEq, exists_prop, exists_eq_right,
    ← val_le_iff]

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

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ (Disjoint on f) (i, i') (i, j')

Tactic:
refine (ht hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 h).mono ?_ ?_

Goal state after:
case inl.refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') ≤ (fun i' ↦ ⨆ i ∈ s, f (i, i')) (i, i').2

case inl.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') ≤ (fun i' ↦ ⨆ i ∈ s, f (i, i')) (i, j').2
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
h : P (ULift.{u, 0} (Fin (card α)))
⊢ Trunc (P α)

Tactic:
apply Trunc.map _ (Fintype.truncEquivFin α)

Goal state after:
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
h : P (ULift.{u, 0} (Fin (card α)))
⊢ α ≃ Fin (card α) → P α
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (range fun x ↦ f ↑x)
hne : s.Nonempty
this : Nonempty ↑s
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ f ↑i

Tactic:
simpa [← directedOn_range, ← comp_def, range_comp]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i ∈ f '' s

Tactic:
by
  lift s to Finset ι using hs
  simp only [Finset.mem_coe] at h
  simpa using Finset.ciSup_mem_image f h

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

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ x ∈ univ, g x) = ⨆ i, f (g i)

Tactic:
← iSup_univ (f := fun i ↦ f (g i))

Goal state after:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ x ∈ univ, g x) = ⨆ x ∈ univ, f (g x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLinearOrder α
s : Set α
hfin : s.Finite
a : α
hne : a ≠ ⊥
hmem : a ∉ s
⊢ sSup s ≠ a

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | hnonempty
  · simp [eq_comm, hne]
  exact (hmem <| · ▸ hnonempty.csSup_mem hfin)

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ sSup (id '' ↑s) = sSup ↑s

Tactic:
Set.image_id

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ sSup ↑s = sSup ↑s
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
⊢ (∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) ↔ x ∈ f a b

Tactic:
refine ⟨?_, fun hx => ⟨_, hx, rfl⟩⟩

Goal state after:
ι : 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
⊢ (∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) → x ∈ f a b
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:
by
  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:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
n : ℕ
p : ℕ → Prop
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
hn : n ≤ Nat.find hp
⊢ Nat.find ⋯ + n = Nat.find hp

Tactic:
exact find_add hn

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

Goal state before:
pp: case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

Tactic:
refine (hln <| ih hl ?_ hkl.symm).elim

Goal state after:
case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n ∈ ↑(Ico n (n + a))
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
⊢ (range' 1 a).toFinset = Icc 1 a

Tactic:
ext x
  rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ), ¬IsMax (a n) → a n ⋖ a (n + 1)
this : ∀ (n : ℕ), ¬IsMax (a n)
⊢ False

Tactic:
exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
suffices ∀ (s : Finset ι) (f : ℕ → ∀ i, α i),
    ∃ g : ℕ ↪o ℕ, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i, i ∈ s → r i ((f ∘ g) a i) ((f ∘ g) b i) by
    rw [wellQuasiOrdered_iff_exists_monotone_subseq]
    intro f
    simpa only [Finset.mem_univ, true_imp_iff] using! this Finset.univ f

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)