mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ⊆ ↑(closure s)

Tactic:
rintro x (hx | hx)
    · exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)
    · exact Subsemigroup.closure_le.mpr subset_closure hx

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
ι : Sort u_7
inst✝ : Nonempty ι
f : G →* N
hf : Injective ⇑f
s : ι → Subgroup G
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Goal state after:
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
h : Surjective ⇑f
⊢ ⊤ ≤ map f ⊤

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
x : N
⊢ x ∈ ⊤ → x ∈ map f ⊤
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
H : Subgroup G
⊢ comap f (map f H) ≤ H ⊔ f.ker

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
⊢ x ∈ comap f (map f H) → x ∈ H ⊔ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
⊢ Injective fun g ↦ ↑g.1 * ↑g.2

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x : ↥H₁ × ↥H₂
⊢ ∀ ⦃a₂ : ↥H₁ × ↥H₂⦄, (fun g ↦ ↑g.1 * ↑g.2) x = (fun g ↦ ↑g.1 * ↑g.2) a₂ → x = a₂
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
ι : Sort u_5
inst✝ : Nonempty ι
f : F
hf : Injective ⇑f
s : ι → Submonoid M
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
⊢ H ≤ normalizer ↑(closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s

Tactic:
by
  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
  rw [mem_normalizer_iff_map_conj_eq, MonoidHom.map_closure]
  apply le_antisymm <| by simpa using! hH h hh
  rw [closure_le, ← MonoidHom.map_closure]
  exact fun g hg ↦ ⟨_, hH _ (inv_mem hh) g hg, by simp [mul_assoc]⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ map f (normalizer ↑H) ≤ normalizer ↑(map f H)

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : N
⊢ x ∈ map f (normalizer ↑H) → x ∈ normalizer ↑(map f H)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore

Tactic:
normal_le_normalCore

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
rintro ⟨a, h, ha⟩

Goal state after:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
rintro ⟨a, h, ha⟩

Goal state after:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
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
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
⊢ ∀ (x y : G₂), g (f_inv (x * y)) = g (f_inv x) * g (f_inv y)

Tactic:
intro x

Goal state after:
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
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₂
⊢ ∀ (y : G₂), g (f_inv (x * y)) = g (f_inv x) * g (f_inv y)
Module: Mathlib.Logic.Embedding.Set

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

Tactic:
suffices ¬p x by simpa
        intro hp
        simpa using h.le_bot x ⟨hp, x.prop⟩

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

Goal state before:
pp: case h.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
obtain ⟨v, hv⟩ := exists_gt x.2

Goal state after:
case h.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
v : β
hv : x.2 < v
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
⊢ motive x

Tactic:
have : x ∈ closure s := by simp [hs]
  induction this using closure_induction_right with
  | one => exact one
  | mul_right x _ y hy ih => exact mul_right x y hy ih

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 x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ ↑(⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ ^ (Int.negSucc m).natMod ↑n) =
    ↑((⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ ^ (↑m.succ).natMod ↑n) ^ (n - 1))

Tactic:
simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (Int.negSucc m % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
⊢ ∀ x ∈ s,
    ∀ (y : M),
      (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z

Tactic:
intro x

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
⊢ x ∈ s →
    ∀ (y : M),
      (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ ∀ x ∈ s, ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a

Tactic:
intro x

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ x ∈ s → ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
Module: Mathlib.Data.List.MinMax

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

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

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
n : ℕ
⊢ encode (ofNat α n) = n

Tactic:
by
  obtain ⟨a, h, e⟩ := decode_inv (α := α) n
  rwa [ofNat_of_decode h]

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.length = l.length

Tactic:
simp only [revzip, length_zip, length_reverse, min_self]

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.length = l.length

Tactic:
by
  simp only [revzip, length_zip, length_reverse, min_self]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y

Tactic:
intro x

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
⊢ x ∈ s → ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
⊢ StrictMonoOn f ↑s

Tactic:
intro x

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
⊢ x ∈ ↑s → ∀ ⦃b : α⦄, b ∈ ↑s → x < b → f x < f b
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).sublists = do
    let x ← l₂.sublists
    map (fun x_1 ↦ x_1 ++ x) l₁.sublists

Tactic:
simp only [sublists, foldr_append]
  induction l₁ with
  | nil => simp
  | cons a l₁ ih =>
    rw [foldr_cons, ih]
    simp [List.flatMap, flatten_flatten, Function.comp_def]

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : List α → β
r : List β
⊢ sublistsLenAux 0 l f r = f [] :: r

Tactic:
cases l

Goal state after:
case nil
α : Type u
β : Type v
f : List α → β
r : List β
⊢ sublistsLenAux 0 [] f r = f [] :: r

case cons
α : Type u
β : Type v
f : List α → β
r : List β
head✝ : α
tail✝ : List α
⊢ sublistsLenAux 0 (head✝ :: tail✝) f r = f [] :: r
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
⊢ ∀ ⦃x : α⦄, ∀ x_1 ∈ s, x ∈ x_1 → ∀ ⦃y : α⦄, ∀ x_2 ∈ s, y ∈ x_2 → x ≠ y → r x y

Tactic:
intro x

Goal state after:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
⊢ ∀ x_1 ∈ s, x ∈ x_1 → ∀ ⦃y : α⦄, ∀ x_2 ∈ s, y ∈ x_2 → x ≠ y → r x y
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ l₁ ++ l₂ ~ l

Tactic:
rw [revzip] at h
  induction l generalizing l₁ l₂ with
  | nil =>
    simp_all only [sublists'_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons,
      zip_nil_right, mem_singleton, Prod.mk.injEq, append_nil, Perm.refl]
  | cons a l IH =>
    rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
      <;> [simp only [mem_append, mem_map, Prod.map_apply, id_eq, Prod.mk.injEq, Prod.exists,
        exists_eq_right_right] at h; simp]
    rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
    · exact perm_middle.trans ((IH _ _ h).cons _)
    · exact (IH _ _ h).cons _

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

Goal state before:
pp: case insert
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x

Tactic:
use z, hzs

Goal state after:
case right
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ (insert a r).sup id ≤ z
Module: Mathlib.Data.Finset.Option

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

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

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ powersetCard (#s) s = {s}

Tactic:
by
  ext
  rw [mem_powersetCard, mem_singleton]
  constructor
  · exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge
  · rintro rfl
    simp

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

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

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

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ (powersetCard n.succ u).biUnion id

Tactic:
intro x

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
⊢ x ∈ u → x ∈ (powersetCard n.succ u).biUnion id
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := ⋯
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑⟨i, hi⟩ = ↑⟨j, hj⟩

Tactic:
refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨i, hi⟩) ∈ s ↑⟨j, hj⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
⊢ iSup f ≤ iSup g

Tactic:
cases isEmpty_or_nonempty ι
  · rw [iSup_of_empty', iSup_of_empty']
  · exact ciSup_le fun x => le_ciSup_of_le B x (H x)

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Ico a b ⊆ {a}

Tactic:
← Icc_sdiff_right,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Icc a b \ {b} ⊆ {a}
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Ico a b = {c}
⊢ a = c ∧ a ⋖ b

Tactic:
simp_rw [Set.ext_iff, mem_Ico, mem_singleton_iff] at h
    have ⟨hac, hcb⟩ := (h c).mpr rfl
    obtain rfl := (h a).mp ⟨le_refl a, hac.trans_lt hcb⟩
    exact ⟨rfl, ⟨hcb, fun d hcd hdb ↦ hcd.ne ((h d).mp ⟨hcd.le, hdb⟩).symm⟩⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
γ : Type u_7
f : (i : ι) × α i → γ
⊢ f '' s.sigma t = ⋃ i ∈ s, f ∘ Sigma.mk i '' t i

Tactic:
by
  aesop

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ s.sigma t = ⋃ i ∈ s, Sigma.mk i '' t i

Tactic:
by
  aesop

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:
rintro ⟨a, ha, rfl⟩

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s ⋖ insert a s
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (∃ a ∈ t, t \ {a} = s) → s ⋖ t

Tactic:
rintro ⟨a, ha, rfl⟩

Goal state after:
α : Type u_1
t : Set α
a : α
ha : a ∈ t
⊢ t \ {a} ⋖ t
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_1.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⩿ (a₂, b₁)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₁ ∨ b₁ ⩿ b₁ ∧ a₁ = a₂

Tactic:
· exact Or.inl ⟨mk_wcovBy_mk_iff_left.1 h, rfl⟩

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) := Subtype.orderBot Pbot
⊢ SurjOn Subtype.val (Subtype.val ⁻¹' ↑t) ↑t

Tactic:
intro x

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
x : α
⊢ x ∈ ↑t → x ∈ Subtype.val '' Subtype.val ⁻¹' ↑t
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : OrderTop α
a✝ x✝ a x : α
⊢ x ∈ Ioc a ⊤ ↔ a < x

Tactic:
rw [mem_Ioc, and_iff_left le_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀ h₁ : LocallyFiniteOrderTop α
⊢ h₀ = h₁

Tactic:
obtain ⟨h₀_finset_Ioi, h₀_finset_Ici, h₀_finset_mem_Ici, h₀_finset_mem_Ioi⟩ := h₀

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : LocallyFiniteOrderTop α
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    h₁
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
m n : ℕ
mn : m < n
h : (Nat.orderEmbeddingOfSet bad) m ∈ bad
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad) m)) (f ((Nat.orderEmbeddingOfSet bad) n))

Tactic:
exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hIncreasing : ∀ (m n : ℕ), m < n → f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)

pp: case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)

Tactic:
· exact Or.inl hIncreasing

Goal state after:
case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)
Module: Mathlib.Order.WellFoundedSet

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

Tactic:
simpa only [hfs, and_true] using @hf

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert b (Set.Ico a b) = Set.Icc a b

Tactic:
Set.insert_eq,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ {b} ∪ Set.Ico a b = Set.Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert a (Set.Ioc a b) = Set.Icc a b

Tactic:
Set.insert_eq,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ {a} ∪ Set.Ioc a b = Set.Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
Set.insert_eq,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ {a} ∪ Set.Ioo a b = Set.Ico a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b (Set.Ioo a b) = Set.Ioc a b

Tactic:
Set.insert_eq,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ {b} ∪ Set.Ioo a b = Set.Ioc a b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
⊢ (insert a s).IsPWO ↔ s.IsPWO

Tactic:
simp only [← singleton_union, isPWO_union, isPWO_singleton, true_and]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ ⋯.min ⋯ = Min.min (hs.min hsn) (ht.min htn)

Tactic:
refine le_antisymm (le_min (IsWF.min_le_min_of_subset subset_union_left)
    (IsWF.min_le_min_of_subset subset_union_right)) ?_
  rw [min_le_iff]
  exact ((mem_union _ _ _).1 ((hs.union ht).min_mem (union_nonempty.2 (.inl hsn)))).imp
    (hs.min_le _) (ht.min_le _)

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 α
⊢ Injective orbit

Tactic:
intro x

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
⊢ ∀ ⦃a₂ : Quotient G α⦄, x.orbit = a₂.orbit → x = a₂
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
⊢ ∀ (x : G), x ∈ center G

Tactic:
intro x

Goal state after:
G : Type u_2
inst✝ : CommGroup G
x : G
⊢ x ∈ center G
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ center G
__src✝ : Group G := inst✝
⊢ ∀ (a b : G), a * b = b * a

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ center G
__src✝ : Group G := inst✝
x : G
⊢ ∀ (b : G), x * b = b * x
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ center G ≤ normalizer s

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ center G → x ∈ normalizer s