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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ ∀ x ∈ s, ∀ y ∈ ⋂ i, t i, f x y ∈ ⋂ i, image2 f s (t i)

Tactic:
mem_iInter

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ x ∈ ⋂ i, ⋂ j, s i j, ∀ y ∈ t, f x y ∈ ⋂ i, ⋂ j, image2 f (s i j) t

Tactic:
mem_iInter

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ y ∈ t, ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ x ∈ s, ∀ y ∈ ⋂ i, ⋂ j, t i j, f x y ∈ ⋂ i, ⋂ j, image2 f s (t i j)

Tactic:
mem_iInter

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s * t) = ⇑m '' ⇑m ⁻¹' s * ⇑m '' ⇑m ⁻¹' t

Tactic:
image_preimage_eq_iff.2 hs,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s * t) = s * ⇑m '' ⇑m ⁻¹' t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s / t) = ⇑m '' ⇑m ⁻¹' s / ⇑m '' ⇑m ⁻¹' t

Tactic:
image_preimage_eq_iff.2 hs,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s / t) = s / ⇑m '' ⇑m ⁻¹' t
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ ↑H ↔ x * n * x⁻¹ ∈ ↑H

Tactic:
by
  rw [SetLike.mem_coe, SetLike.mem_coe, H.mul_mem_cancel_right <| H.inv_mem xH,
    H.mul_mem_cancel_left xH]

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

Goal state before:
pp: F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : InjOn ⇑f ↑s
a : G
ha : a ∈ s
ha' : f a = 1
⊢ f a = f 1

Tactic:
rwa [map_one]

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

Goal state before:
pp: case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
⊢ (x1, x2) ∈ u

Tactic:
have h1' : inl M N x1 ∈ u := by
      apply hH
      simpa using h1

Goal state after:
case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
⊢ (x1, x2) ∈ u
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (match n.boddDiv2 with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)

Tactic:
ih

Goal state after:
case succ
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (match (n.bodd, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : n✝.bodd = n✝.bits.headI
⊢ (bit b✝ n✝).bodd = (bit b✝ n✝).bits.headI

Tactic:
| bit _ _ h =>

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

Goal state before:
pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : n✝.div2.bits = n✝.bits.tail
⊢ (bit b✝ n✝).div2.bits = (bit b✝ n✝).bits.tail

Tactic:
| bit _ _ h =>

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

Goal state before:
pp: n : ℕ
⊢ n.div2.bits = n.bits.tail

Tactic:
induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [div2_bit, bits_append_bit _ _ h]

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

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ m ^ 2 + min m n ≤ m * m + m + n

Tactic:
min_eq_right h,

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ m ^ 2 + n ≤ m * m + m + n
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ N

Tactic:
exact conjugatesOfSet_subset h hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
α₁ : Type u_6
g : α₁ → α
x : FreeMonoid α₁
⊢ (map f) ((map g) x) = (map (f ∘ g)) x

Tactic:
unfold map

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
α₁ : Type u_6
g : α₁ → α
x : FreeMonoid α₁
⊢ { toFun := fun l ↦ ofList (List.map f (toList l)), map_one' := ⋯, map_mul' := ⋯ }
      ({ toFun := fun l ↦ ofList (List.map g (toList l)), map_one' := ⋯, map_mul' := ⋯ } x) =
    { toFun := fun l ↦ ofList (List.map (f ∘ g) (toList l)), map_one' := ⋯, map_mul' := ⋯ } x
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
hb : (map f) 1 = of d
⊢ ∃ a, f a = d

Tactic:
have H := congr_arg length hb
      simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ (subtypeOrLeftEmbedding p q)
      (Sum.elim (⇑(Subtype.impEmbedding p (fun x ↦ p x ∨ q x) ⋯)) (⇑(Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯))
        (Sum.inr x)) =
    Sum.inr x

Tactic:
simp only [Sum.elim_inr]

Goal state after:
case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ (subtypeOrLeftEmbedding p q) ((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x) = Sum.inr x
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if hd = val✝ then 0 else idxOf val✝ tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
· rw [if_neg, if_neg]
      · exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)
      · exact ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne
      · exact ne_of_apply_ne _ ‹f hd < f _›.ne

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case none
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ Option.rec (some a) (fun val ↦ if val < a then some a else some val) none = max none ↑a

pp: case some
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
val✝ : α
⊢ Option.rec (some a) (fun val ↦ if val < a then some a else some val) (some val✝) = max (some val✝) ↑a

Tactic:
· exact (max_eq_right bot_le).symm

Goal state after:
case some
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
val✝ : α
⊢ Option.rec (some a) (fun val ↦ if val < a then some a else some val) (some val✝) = max (some val✝) ↑a
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toLeft = cons a u.toLeft ⋯

Tactic:
ext y; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toLeft = u.toLeft

Tactic:
ext y; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toRight = u.toRight

Tactic:
ext y; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toRight = cons b u.toRight ⋯

Tactic:
ext y; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inl a) u).toLeft = insert a u.toLeft

Tactic:
ext y; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inr b) u).toLeft = u.toLeft

Tactic:
ext y; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inl a) u).toRight = u.toRight

Tactic:
ext y; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inr b) u).toRight = insert b u.toRight

Tactic:
ext y; simp

Goal state after:
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✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
f g : BoundedLatticeHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

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

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

Goal state before:
pp: case empty
α : Type u_2
inst✝ : LinearOrder α
⊢ ∀ {a : α}, ∅.max = ↑a → a ∈ ∅

Tactic:
intro _ H; cases H

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ List.map (ofList ∘ pure) l <+~ List.map ofList l.sublists

Tactic:
rw [← List.map_map]

Goal state after:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map ofList (List.map pure l) <+~ List.map ofList l.sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      l₁ =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)
⊢ flatMap (fun x ↦ [x, a :: x])
      (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc)
        (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂) l₁) =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] (a :: l₁))

Tactic:
ih

Goal state after:
case cons
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      l₁ =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)
⊢ (flatMap (fun x ↦ [x, a :: x]) do
      let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
      map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)) =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] (a :: l₁))
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
⊢ (f ⊔ g) a✝ ⊔ s✝.sup (f ⊔ g) = f a✝ ⊔ s✝.sup f ⊔ (g a✝ ⊔ s✝.sup g)

Tactic:
ih

Goal state after:
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
⊢ (f ⊔ g) a✝ ⊔ (s✝.sup f ⊔ s✝.sup g) = f a✝ ⊔ s✝.sup f ⊔ (g a✝ ⊔ s✝.sup g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.sup f = s₂.sup g

Tactic:
subst hs
  exact Finset.fold_congr hfg

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
⊢ i ∈ t

Tactic:
obtain ⟨a, hai⟩ := h₁ i hi

Goal state after:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
⊢ i ∈ t
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case inl
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Subsingleton α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

pp: case inr
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Nontrivial α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
· simpa [Subsingleton.elim _ (⊤ : α)]

Goal state after:
case inr
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Nontrivial α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs✝ : s.Nonempty
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : a ⊓ s✝.sup' hs f = s✝.sup' hs fun i ↦ a ⊓ f i
⊢ a ⊓ f a✝ ⊔ a ⊓ s✝.sup' hs f = a ⊓ f a✝ ⊔ s✝.sup' hs fun i ↦ a ⊓ f i

Tactic:
ih

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

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
⊢ (count b (s.sup f) = s.sup fun a ↦ count b (f a)) →
    count b ((insert i s).sup f) = (insert i s).sup fun a ↦ count b (f a)

Tactic:
ih

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
ih : count b (s.sup f) = s.sup fun a ↦ count b (f a)
⊢ count b ((insert i s).sup f) = (insert i s).sup fun a ↦ count b (f a)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
ih : count b (s.sup f) = s.sup fun a ↦ count b (f a)
⊢ max (count b (f i)) (count b (s.sup f)) = max (count b (f i)) (s.sup fun a ↦ count b (f a))

Tactic:
ih

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
ih : count b (s.sup f) = s.sup fun a ↦ count b (f a)
⊢ max (count b (f i)) (s.sup fun a ↦ count b (f a)) = max (count b (f i)) (s.sup fun a ↦ count b (f a))
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)

Tactic:
by_cases h : i ∈ s

Goal state after:
case pos
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∈ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)

case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

Tactic:
by_cases h : i ∈ s

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

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)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι✝ : Sort v
κ✝ : ι✝ → Sort w
inst✝² : Order.Frame α
inst✝¹ : Finite ι✝
f : (a : ι✝) → κ✝ a → α
ι : Type v
κ : ι → Type w
inst✝ : Finite ι
⊢ ∀ (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
f

Goal state after:
α : Type u
ι✝ : Sort v
κ✝ : ι✝ → Sort w
inst✝² : Order.Frame α
inst✝¹ : Finite ι✝
f✝ : (a : ι✝) → κ✝ a → α
ι : Type v
κ : ι → Type w
inst✝ : Finite ι
f : (a : ι) → κ a → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type v
κ✝ : ι → Sort w
inst✝² : Nonempty ((a : ι) → κ✝ a)
inst✝¹ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ✝ a → α
κ : ι → Type w
inst✝ : Nonempty ((a : ι) → κ a)
⊢ ∀ (f : (a : ι) → κ a → α), ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
f

Goal state after:
α : Type u
ι : Type v
κ✝ : ι → Sort w
inst✝² : Nonempty ((a : ι) → κ✝ a)
inst✝¹ : Order.Frame α
s : Set ι
hs : s.Finite
f✝ : (a : ι) → κ✝ a → α
κ : ι → Type w
inst✝ : Nonempty ((a : ι) → κ a)
f : (a : ι) → κ a → α
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : IsEmpty (Subtype p)
⊢ sSup ∅ = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
cbiSup_eq_of_forall_not fun i h ↦ isEmptyElim (⟨i, h⟩ : Subtype p)

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : IsEmpty (Subtype p)
⊢ sSup ∅ = sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ≤ ⨆ x, ⨆ (h : b = x), f x h

Tactic:
by
  refine le_ciSup₂ ⟨f b rfl, ?_⟩ b rfl
  rintro a ⟨_, ⟨b, rfl⟩, ⟨rfl, rfl⟩⟩
  rfl

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
p : ι → Prop
f : Exists p → α
i : ι
hi : p i
⊢ f ⋯ ≤ ⨆ (ih : Exists p), f ih

Tactic:
simp [show Exists p from ⟨i, hi⟩]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (∃ a ∉ s, insert a s = t) → s ⋖ t

Tactic:
by rintro ⟨a, ha, rfl⟩; exact covBy_insert ha

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⩿ y → x.1 = y.1 ∨ x.2 = y.2

Tactic:
intro h
  by_contra! ⟨ha, hb⟩
  exact
    h.2 (mk_lt_mk.2 <| Or.inl ⟨ha.lt_of_le h.1.1, le_rfl⟩)
      (mk_lt_mk.2 <| Or.inr ⟨le_rfl, hb.lt_of_le h.1.2⟩)

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b

Tactic:
rw [Ioo, ← Finset.mem_def, Finset.mem_Ioo]

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

Goal state before:
pp: a b c : ℕ
⊢ Unique ↥(Iic 0)

Tactic:
← Nat.bot_eq_zero

Goal state after:
a b c : ℕ
⊢ Unique ↥(Iic ⊥)
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 : ℕ
⊢ (∀ m ≥ n + 1, P m) → ∀ m ≥ n, P m

Tactic:
ih

Goal state after:
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 ≥ n, P m
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : Std.Refl r
⊢ WellQuasiOrdered r

Tactic:
intro f
  obtain ⟨m, n, h, hf⟩ := Set.finite_univ.exists_lt_map_eq_of_forall_mem (f := f)
    fun _ ↦ Set.mem_univ _
  exact ⟨m, n, h, hf ▸ refl _⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

pp: case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
· refine ⟨g, fun m n hle => ?_⟩
    obtain hlt | rfl := hle.lt_or_eq
    exacts [h1 m n hlt, refl_of r _]

Goal state after:
case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
⊢ ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
f

Goal state after:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
⊢ WellQuasiOrdered r

Tactic:
f

Goal state after:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
⊢ ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
⊢ WellQuasiOrdered fun a b ↦ r a.1 b.1 ∧ s a.2 b.2

Tactic:
intro f
  obtain ⟨g, h₁⟩ := hr.exists_monotone_subseq (Prod.fst ∘ f)
  obtain ⟨m, n, h, hf⟩ := hs (Prod.snd ∘ f ∘ g)
  exact ⟨g m, g n, g.strictMono h, h₁ _ _ h.le, hf⟩

Goal state after: