mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : i.castSucc < a
hu : b < i.succ
⊢ b < a

Tactic:
by
  simp [Fin.lt_def, -val_fin_lt] at *; lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
⊢ ¬x = y → ¬f x = f y

Tactic:
exact hz x hx y hy

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

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
· rw [hij] at hi
    cases hj <| Nat.lt_trans j.castSucc_lt_succ hi

Goal state after:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
h : #s < #t
⊢ ∃ e ∈ t, e ∉ s

Tactic:
by
  classical simpa [Finset.Nonempty] using sdiff_nonempty_of_card_lt_card h

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (ofFn f).Nodup

Tactic:
rw [ofFn_eq_pmap]
  exact nodup_range.pmap fun _ _ _ _ H => Fin.val_eq_of_eq <| hf H

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup ↔ Function.Injective f

Tactic:
refine ⟨?_, nodup_ofFn_ofInjective⟩

Goal state after:
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup → Function.Injective f
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
have := Nat.lt_add_right m lt_n

Goal state after:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
this : i < n + m
⊢ as ⟨i, ⋯⟩ = b
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.List.Sort

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
simpa [h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
· suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by
        simpa [orderedInsert_cons, h', h.of_cons.orderedInsert a l]
      intro b' bm
      rcases (mem_orderedInsert r).mp bm with rfl | bm
      · exact (total_of r _ _).resolve_left h'
      · exact rel_of_pairwise_cons h bm

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

Goal state before:
pp: case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → ∀ (d : List α), d ~ c → d <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hs : Pairwise r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h

Goal state after:
case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
ih : c.erase a <+ insertionSort r tail✝
hs : Pairwise r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
⊢ c <+ insertionSort r (a :: tail✝)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case pos
α : 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:
refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_

Goal state after:
case pos
α : 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
⊢ (count a (filter p (a :: as).dedup) • if a = a then 1 else 0) = if p a = true then 1 else 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n)

Tactic:
rotate_eq_drop_append_take_mod,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    zipWith f (l.rotate n) (l'.rotate n)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    zipWith f (l.rotate n) (l'.rotate n)

Tactic:
rotate_eq_drop_append_take_mod,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    zipWith f (drop (n % l.length) l ++ take (n % l.length) l) (l'.rotate n)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    zipWith f (drop (n % l.length) l ++ take (n % l.length) l) (l'.rotate n)

Tactic:
rotate_eq_drop_append_take_mod,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    zipWith f (drop (n % l.length) l ++ take (n % l.length) l) (drop (n % l'.length) l' ++ take (n % l'.length) l')
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
hle : l.length = l'.length
⊢ l = l'

Tactic:
rotate_eq_drop_append_take_mod,

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

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid O
s : Multiset ι
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
l : List ι
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) ⟦l⟧).prod = f (map f₁ ⟦l⟧).prod (map f₂ ⟦l⟧).prod

Tactic:
simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, map_coe, prod_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})

Tactic:
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    grind
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _

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

Goal state before:
pp: case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
· rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
        Nat.zero_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s

Tactic:
by
  rw [sInter_eq_biInter]
  apply image_iInter₂_subset

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ 1 ∈ closure s

Tactic:
apply one_mem

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
⊢ closure (s \ t) = closure s

Tactic:
refine (closure_mono Set.sdiff_subset).antisymm <| closure_le.mpr <| fun x hxs ↦ ?_

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
⊢ x ∈ ↑(closure (s \ t))
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ map f H ⊓ map f K = ⊥

Tactic:
← map_inf _ _ f hf,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ map f (H ⊓ K) = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
⊢ H ≤ comap f (map f K) ↔ H ≤ K

Tactic:
comap_map_eq_self_of_injective hf

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
⊢ H ≤ K ↔ H ≤ K
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 : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ map f H ⊓ map f K = ⊥

Tactic:
← map_inf _ _ f hf,

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ map f (H ⊓ K) = ⊥
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = shiftLeft' b m (n + 1) >>> (k + 1)

Tactic:
shiftLeft',

Goal state after:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = bit b (shiftLeft' b m n) >>> (k + 1)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ closure (⇑↑(MulAut.conj h) '' s) ≤ closure s

Tactic:
by simpa using! hH h hh

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ {a} * s / ({b} * t) = {a / b} * (s / t)

Tactic:
mul_div_mul_comm _ s,

Goal state after:
α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ {a} / {b} * (s / t) = {a / b} * (s / t)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G✝ : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁷ : Group G✝
inst✝⁶ : Group G'
inst✝⁵ : Group G''
A : Type u_4
inst✝⁴ : AddGroup A
N : Type u_5
inst✝³ : Group N
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
a : G
ha : a ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
x : M
⊢ a⁻¹ • x - x ∈ I

Tactic:
simpa using sub_mem_comm_iff.mp (ha (a⁻¹ • x))

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i

Tactic:
iSup_subtype',

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ x ∈ ⨆ x, S ↑x ↔ ∃ i, p i ∧ x ∈ S i
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ toLex (a₁, b₁) < toLex (a₁, b₂)

Tactic:
exact right _ (Prod.mk_lt_mk_iff_right.1 h)

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

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a n✝ n : M
i : ℕ
⊢ (fun x ↦ n✝ ^ x) i = n ↔ ((powersHom M) n✝) i = n

Tactic:
simp; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : α
⊢ x✝ ∈ u.toLeft → x✝ ∈ v.toLeft

Tactic:
simpa only [mem_toLeft] using @h _

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

Goal state before:
pp: case cons.tail
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
· exact le_max_of_le_right (IH (by assumption))

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 ≤ f b

Tactic:
rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h]

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

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
s : Finset β
f : β → α
a : α
⊢ (s.sup fun b ↦ f b \ a) = s.sup f \ a

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, bot_sdiff]
  | cons _ _ _ h => rw [sup_cons, sup_cons, h, sup_sdiff]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ S.sup f = ⊥

Tactic:
Finset.sup_eq_bot_iff

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ ∀ s ∈ S, f s = ⊥
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ (𝒫 s).PairwiseDisjoint fun t ↦ {t, insert a t}

Tactic:
rw [pairwiseDisjoint_iff]
  rintro i hi j hj
  have := insert_erase_invOn.2.injOn (notMem_subset hi ha) (notMem_subset hj ha)
  aesop (add simp [Set.Nonempty, Set.subset_def])

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ a < s.sup' H f ↔ ∃ b ∈ s, a < f b

Tactic:
rw [← WithBot.coe_lt_coe, coe_sup', Finset.lt_sup_iff]
  exact exists_congr (fun _ => and_congr_right' WithBot.coe_lt_coe)

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup (WithBot.some ∘ f) < ↑a ↔ ∀ i ∈ s, f i < a

Tactic:
Finset.sup_lt_iff (WithBot.bot_lt_coe a)

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∀ b ∈ s, (WithBot.some ∘ f) b < ↑a) ↔ ∀ i ∈ s, f i < a
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
| ∀ (i : β), ⨆ c, f (i, c) ≤ c

Tactic:
enter [

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
| ∀ (i : β), ⨆ c, f (i, c) ≤ c
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 → α
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
classical
  suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    have : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down
  intro κ _ f
  have := hs.to_subtype
  have : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a
  simp [← iInf_subtype'', iInf_iSup_eq_of_finite (ι := s),
    ← Equiv.piEquivPiSubtypeProd (· ∈ s) _ |>.symm.iSup_comp, iSup_prod, iSup_const]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a ⩿ b ↔ a ≤ b

Tactic:
unfold WCovBy; decide

Goal state after:
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⟩)

Goal state after:
case refine_2.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⩿ a₂
⊢ (a₁, b₁) ⩿ (a₂, b₁)

case refine_2.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)
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⟩)

Goal state after:
case refine_2.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⋖ a₂
⊢ (a₁, b₁) ⋖ (a₂, b₁)

case refine_2.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⋖ b₂
⊢ (a₁, b₁) ⋖ (a₁, b₂)
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
ha : a.fst = x.fst
hb : b.fst = x.fst
hx : x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)

Tactic:
exact ⟨ha, hb, h hx⟩

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
x : α
inst✝ : LE α
⊢ Minimal (fun x ↦ True) x ↔ IsMin x

Tactic:
simp [IsMin, Minimal]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
⊢ Minimal (fun x ↦ x ∈ f '' s) (f a) ↔ Minimal (fun x ↦ x ∈ s) a

Tactic:
refine ⟨fun h ↦ ⟨ha, fun y hys ↦ ?_⟩, minimal_mem_image_monotone hf⟩

Goal state after:
α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x ↦ x ∈ f '' s) (f a)
y : α
hys : (fun x ↦ x ∈ s) y
⊢ y ≤ a → a ≤ y
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = Iic n

Tactic:
range_succ_eq_Icc_zero

Goal state after:
n : ℕ
⊢ Icc 0 n = Iic n
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: ⊢ sSup ∅ = ⊥

Tactic:
simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
        not_false_iff, exists_const]
      apply bot_unique (Nat.find_min' _ _)
      trivial

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n : ℕ
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))

Tactic:
have h := hm _ (Nat.le_add_left m n)

Goal state after:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n : ℕ
h : n + m ∉ bad
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (InvImage (Subrel r fun x ↦ x ∈ range f) f') c

Tactic:
· exact h.apply _

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Tactic:
by
  rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]

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

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
rw [← coe_eq_empty, coe_Ioi, Set.Ioi_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ (↑(Submonoid.closure s)).IsPWO

Tactic:
rw [Submonoid.closure_eq_image_prod]

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ (List.prod '' {l | ∀ x ∈ l, x ∈ s}).IsPWO
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f (g m) i) (f (g n) i)

Tactic:
simpa only [Finset.mem_univ, true_imp_iff] using! this Finset.univ f hf

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : Quotient.out x ∈ MulAction.orbit G (Quotient.out y)
⊢ x = y

Tactic:
← orbitRel_apply

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : (orbitRel G α) (Quotient.out x) (Quotient.out y)
⊢ x = y
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case h
α : Type u_2
r : α → α → Prop
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
m n : ℕ
hmn : m < n
hr : r (f (φ m)) (f (φ n))
⊢ φ m < φ n ∧ r (f (φ m)) (f (φ n))

Tactic:
exact ⟨hφm hmn, hr⟩

Goal state after: