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

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
l : List α
h : l.rotate 1 = l
n✝ n : ℕ
hn : l.rotate n = l
⊢ l.rotate n.succ = l

Tactic:
Nat.succ_eq_add_one,

Goal state after:
α : Type u
inst✝ : Nonempty α
l : List α
h : l.rotate 1 = l
n✝ n : ℕ
hn : l.rotate n = l
⊢ l.rotate (n + 1) = l
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ Function.onFun Disjoint (fun a ↦ {x ∈ s | f x = a}) x' y'

Tactic:
simp_rw [disjoint_left, mem_filter]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset ι
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
g : ι → M
⊢ (map (fun i ↦ f (g i)) s).prod = f (map g s).prod

Tactic:
by
  convert! (s.map g).prod_hom f
  exact (map_map _ _ _).symm

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

Goal state before:
pp: n : ℕ
⊢ n.choose 1 = n

Tactic:
induction n <;> simp [*, choose, Nat.add_comm]

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

Goal state before:

Tactic:
_ = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) := by
      grind [choose_mul_factorial_mul_factorial]
    _ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) := by
      grind

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ f '' s⁻¹ = g '' s

Tactic:
rw [← Set.image_inv_eq_inv, Set.image_image]; exact Set.image_congr H

Goal state after:
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 α β
f : F
s : Set α
⊢ ⇑f '' s⁻¹ = (⇑f '' s)⁻¹

Tactic:
rw [← image_inv_eq_inv, ← image_inv_eq_inv]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' (fun x ↦ x⁻¹) '' s = (fun x ↦ x⁻¹) '' ⇑f '' s
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: S : Type u_3
G : Type u_4
inst✝² : Inv G
inst✝¹ : SetLike S G
s : S
inst✝ : HasMemOrInvMem s
x : G
h : ¬x ∈ s
⊢ x⁻¹ ∈ s

Tactic:
have := mem_or_inv_mem s x

Goal state after:
S : Type u_3
G : Type u_4
inst✝² : Inv G
inst✝¹ : SetLike S G
s : S
inst✝ : HasMemOrInvMem s
x : G
h : ¬x ∈ s
this : x ∈ s ∨ x⁻¹ ∈ s
⊢ x⁻¹ ∈ s
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: S : Type u_3
G : Type u_4
inst✝² : Inv G
inst✝¹ : SetLike S G
s : S
inst✝ : HasMemOrInvMem s
x : G
h : ¬x⁻¹ ∈ s
⊢ x ∈ s

Tactic:
have := mem_or_inv_mem s x

Goal state after:
S : Type u_3
G : Type u_4
inst✝² : Inv G
inst✝¹ : SetLike S G
s : S
inst✝ : HasMemOrInvMem s
x : G
h : ¬x⁻¹ ∈ s
this : x ∈ s ∨ x⁻¹ ∈ s
⊢ x ∈ s
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
⊢ a = 1

Tactic:
refine h ha (one_mem s) ?_
    rwa [map_one]

Goal state after:
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
⊢ map f f.ker = ⊥

Tactic:
map_eq_bot_iff

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ f.ker ≤ f.ker
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
s : Submonoid M
t : Submonoid N
⊢ s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Tactic:
by
  simp only [eq_top_iff, le_prod_iff, ← mrange_eq_map, mrange_fst, mrange_snd]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ map f ⊤ = ⊤

Tactic:
← MonoidHom.mrange_eq_map,

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
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ mrange f = ⊤
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.bodd.toNat + 2 * n.div2 = n

Tactic:
cases n using bitCasesOn with
  | bit b n => simpa using (bit_val b n).symm

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Normal ↔ ∀ (g : G), map (↑(MulAut.conj g)) H = H

Tactic:
simp_rw [← normalizer_eq_top_iff, Subgroup.eq_top_iff', mem_normalizer_iff_map_conj_eq]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ normalClosure ∅ = ⊥

Tactic:
rw [← normalClosure_closure_eq_normalClosure, closure_empty, normalClosure_eq_self]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a = 1

Tactic:
rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]

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

Goal state before:
pp: M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
H : Subgroup G
⊢ Subgroup.map H.subtype (I.inertia ↥H) = I.inertia G ⊓ H

Tactic:
← AddSubgroup.subgroupOf_inertia,

Goal state after:
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
H : Subgroup G
⊢ Subgroup.map H.subtype ((I.inertia G).subgroupOf H) = I.inertia G ⊓ H
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b → Lex r (fun i ↦ Function.swap (s i)) b a

Tactic:
rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
      · exact Lex.left _ _ h
      · exact Lex.right _ _ h

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r (fun i ↦ Function.swap (s i)) b a → Lex (Function.swap r) s a b

Tactic:
rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
      · exact Lex.left _ _ h
      · exact Lex.right _ _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
⊢ (Option.casesOn (Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a) (some tl) fun c ↦
      if f c < f tl then some tl else some c) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c ↦ if f a < f c then some c else some a

Tactic:
argmax_concat

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
⊢ (Option.casesOn (Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a) (some tl) fun c ↦
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn (argmax f hd) (some tl) fun c ↦ if f c < f tl then some tl else some c) (some a)
      fun c ↦ if f a < f c then some c else some a
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by
      simpa [bit_bodd_div2]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a ∈ decodeSum n, encodeSum a = bit n.bodd n.div2
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∀ (x : ℕ), x ∉ {y ∈ range ↑(ofNat s 0) | y ∈ s}

Tactic:
rintro n hn

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
hn : n ∈ {y ∈ range ↑(ofNat s 0) | y ∈ s}
⊢ False
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this✝ : DecidablePred fun x ↦ x ∈ Set.range encode := decidableRangeEncode α
this : Infinite ↑(Set.range encode) :=
  Infinite.of_injective (⇑(Equiv.ofInjective encode encode_injective))
    (Equiv.injective (Equiv.ofInjective encode encode_injective))
⊢ Denumerable α

Tactic:
letI := Nat.Subtype.denumerable (Set.range (@encode α _))

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this✝¹ : DecidablePred fun x ↦ x ∈ Set.range encode := decidableRangeEncode α
this✝ : Infinite ↑(Set.range encode) :=
  Infinite.of_injective (⇑(Equiv.ofInjective encode encode_injective))
    (Equiv.injective (Equiv.ofInjective encode encode_injective))
this : Denumerable ↑(Set.range encode) := Subtype.denumerable (Set.range encode)
⊢ Denumerable α
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ f a = ⊤ ↔ a = ⊤

Tactic:
by
  rw [← map_top f, (EquivLike.injective f).eq_iff]

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

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

Tactic:
by rw [comp_apply, map_top, map_top]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : s.max = ↑a
⊢ s = ∅

Tactic:
rw [h] at ha

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : ⊥ = ↑a
⊢ s = ∅
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mp.inr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ tl.inits.zip tl.tails
⊢ (fun t ↦ hd :: t) w✝¹ ++ id w✝ = hd :: tl

Tactic:
· simp [ih.mp h]

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

Goal state before:
pp: α : Type u_7
R : Type u_8
inst✝ : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)
  exact ⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (powerset ⟦l⟧).Nodup

Tactic:
by
      simp only [quot_mk_to_coe, powerset_coe', coe_nodup]
      refine (nodup_sublists'.2 h).map_on ?_
      exact fun x sx y sy e =>
        (h.perm_iff_eq_of_sublist (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑(t.sup f) = t.sup fun x ↦ ↑(f x)

Tactic:
apply apply_sup_eq_sup_comp Subtype.val <;> intros <;> rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
H : Set.InjOn f ↑s
⊢ Set.InjOn (fun x ↦ image f x) ↑s.powerset

Tactic:
have {z a} (_ : z ⊆ s) (_ : a ∈ s) : a ∈ z ↔ f a ∈ z.image f := by grind [H.eq_iff]

Goal state after:
α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
H : Set.InjOn f ↑s
this : ∀ {z : Finset α} {a : α}, z ⊆ s → a ∈ s → (a ∈ z ↔ f a ∈ image f z)
⊢ Set.InjOn (fun x ↦ image f x) ↑s.powerset
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ (x ⊆ t ∧ #x = n) ∧ s ⊆ x → ∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x

pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ (∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x) → (x ⊆ t ∧ #x = n) ∧ s ⊆ x

Tactic:
· intro ⟨⟨hxt, hxn⟩, hsx⟩
    exact ⟨x \ s, ⟨fun y hy => mem_sdiff.mpr ⟨hxt (mem_sdiff.mp hy).1, (mem_sdiff.mp hy).2⟩,
           by rw [card_sdiff_of_subset hsx, hxn]⟩, sdiff_union_of_subset hsx⟩

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ (∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x) → (x ⊆ t ∧ #x = n) ∧ s ⊆ x
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
b : β
hb : b ∉ s
⊢ ↑((cons b s hb).sup' ⋯ f) = ↑(f b ⊔ s.sup' H f)

Tactic:
simp [WithBot.coe_sup]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
inst✝ : DecidableEq β
b : β
⊢ ↑((insert b s).sup' ⋯ f) = ↑(f b ⊔ s.sup' H f)

Tactic:
simp [WithBot.coe_sup]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ ⨅ i ∈ s, f i = (image f s).min' h'

Tactic:
rw [← OrderDual.toDual_inj, toDual_min', toDual_iInf]
  simp only [toDual_iInf]
  rw [ciSup_eq_max'_image _ h]
  simp only [image_image]
  congr

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

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

Tactic:
classical
      refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow
      intro
      simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.mk i '' g i ⁻¹' s = Sigma.map f g ⁻¹' Sigma.mk (f i) '' s

Tactic:
refine (image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm ?_

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.map f g ⁻¹' Sigma.mk (f i) '' s ⊆ Sigma.mk i '' g i ⁻¹' s
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ ⨆ x, l ↑x = sSup (l '' s)

Tactic:
sSup_image'

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ ⨆ x, l ↑x = ⨆ a, l ↑a
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Tactic:
simp [Finset.Nonempty]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (∀ (a : ι) (b : α a), a ∈ s → b ∈ t a → f ⟨a, b⟩ ≤ s.sup fun i ↦ (t i).sup fun b ↦ f ⟨i, b⟩) ∧
    ∀ b ∈ s, ∀ b_1 ∈ t b, f ⟨b, b_1⟩ ≤ (s.sigma t).sup f

Tactic:
exact
    ⟨fun i a hi ha => (le_sup hi).trans' <| le_sup (f := fun a => f ⟨i, a⟩) ha, fun i hi a ha =>
      le_sup <| mem_sigma.2 ⟨hi, ha⟩⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := ⋯
⊢ BijOn Subtype.val (Subtype.val ⁻¹' ↑t) ↑t

Tactic:
refine ⟨mapsTo_preimage _ _, injOn_of_injective Subtype.val_injective, ?_⟩

Goal state after:
α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
⊢ SurjOn Subtype.val (Subtype.val ⁻¹' ↑t) ↑t
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ s) b

Tactic:
by
  classical
  obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩
  exact ⟨b, hab, hb, fun c hc hbc ↦ hbmin hc (hab.trans hbc) hbc⟩

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Q x ∧ Minimal P x ↔ Minimal (fun x ↦ P x ∧ Q x) x

Tactic:
minimal_and_iff_right_of_imp hPQ,

Goal state after:
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Q x ∧ Minimal P x ↔ Minimal P x ∧ Q x
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico a b).val - (Finset.Ico a c).val = (Finset.Ico (max a c) b).val

Tactic:
← Finset.sdiff_val,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico a b \ Finset.Ico a c).val = (Finset.Ico (max a c) b).val
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico a b).val - (Finset.Ico c b).val = (Finset.Ico a (min b c)).val

Tactic:
← Finset.sdiff_val,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico a b \ Finset.Ico c b).val = (Finset.Ico a (min b c)).val
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m} - n + n)

Tactic:
Nat.sub_add_cancel hn

Goal state after:
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m})
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

pp: case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
· refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩
    obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)
    induction x with
    | zero => apply hr
    | succ x ih =>
      apply IsTrans.trans _ _ _ _ (hr _)
      exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))

Goal state after:
case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b = ∅ ↔ ¬a < b

Tactic:
rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_1
ι : 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)
f : ℕ → (i : ι) → α i
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ ∅, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)

Tactic:
exists RelEmbedding.refl (· ≤ ·)

Goal state after:
case refine_1
ι : 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)
f : ℕ → (i : ι) → α i
⊢ ∀ ⦃a b : ℕ⦄,
    a ≤ b →
      ∀ i ∈ ∅,
        r i ((f ∘ ⇑(RelEmbedding.refl fun x1 x2 ↦ x1 ≤ x2)) a i) ((f ∘ ⇑(RelEmbedding.refl fun x1 x2 ↦ x1 ≤ x2)) b i)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∃ x, ∀ (n : ℕ), x n ∈ s

Tactic:
refine ⟨⟨f, ?_⟩, H⟩

Goal state after:
case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ (Ioi a).Nonempty ↔ ¬IsMax a

Tactic:
simp [Finset.Nonempty]

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

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
simp [Finset.Nonempty]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = insert a (Ioo a b)

Tactic:
Ioo_insert_left h

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = Ico a b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
ι : 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)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ ∅, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)

Tactic:
exists RelEmbedding.refl (· ≤ ·)

Goal state after:
case refine_1
ι : 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)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
⊢ ∀ ⦃a b : ℕ⦄,
    a ≤ b →
      ∀ i ∈ ∅,
        r i ((f ∘ ⇑(RelEmbedding.refl fun x1 x2 ↦ x1 ≤ x2)) a i) ((f ∘ ⇑(RelEmbedding.refl fun x1 x2 ↦ x1 ≤ x2)) b i)