mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
· set p := m - 1; have hp : m = p + 1 := (succ_pred_eq_of_ne_zero hm).symm
    simp only [hp]
    rw [Nat.add_mul, Nat.one_mul, choose_mul_add hn]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
⊢ IsPretransitive G X

Tactic:
by
  constructor
  intro x y
  rcases ha x with ⟨g, rfl⟩
  rcases ha y with ⟨h, rfl⟩
  exact ⟨h * g⁻¹, by simp [mul_smul]⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ (⋂ i, f i) ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j

Tactic:
simp_rw [iInter_union, union_iInter]

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

Goal state before:
pp: α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ (⋂ i₁, ⋂ i₂, f i₁ i₂) ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂

Tactic:
simp_rw [iInter_union, union_iInter]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
⊢ ⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x

Tactic:
by
  ext ⟨z, w⟩; simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]; constructor
  · intro x hz hw
    exact ⟨⟨x, hz⟩, x, hw⟩
  · intro x hz x' hw
    exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
refine ⟨a, b, ?_, ?_, H ha hb⟩ <;> refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩

Goal state after:
case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a

case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (insert 1 s) = closure s

Tactic:
closure_insert_one

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure s = closure s
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1.refine_3
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i✝ : ι
hp : p i✝
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x✝ : G
hx : x✝ ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
x y : G
hx✝ : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
hy✝ : y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
i : ι
hip : p i
hi : x ∈ K i
j : ι
hjp : p j
hj : y ∈ K j
⊢ ∃ i, p i ∧ x * y ∈ K i

Tactic:
rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩

Goal state after:
case refine_1.refine_3
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i✝ : ι
hp : p i✝
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x✝ : G
hx : x✝ ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
x y : G
hx✝ : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
hy✝ : y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
i : ι
hip : p i
hi : x ∈ K i
j : ι
hjp : p j
hj : y ∈ K j
k : ι
hk : k ∈ {i | p i}
hki : ((fun x1 x2 ↦ x1 ≤ x2) on K) i k
hkj : ((fun x1 x2 ↦ x1 ≤ x2) on K) j k
⊢ ∃ i, p i ∧ x * y ∈ K i
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
refine closure_induction ?_ ?_ ?_ ?_ hx

Goal state after:
case mp.refine_1
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ ↑s ∪ ↑t, ∃ y ∈ s, ∃ z ∈ t, y * z = x

case mp.refine_2
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = 1

case mp.refine_3
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : G),
    x ∈ closure (↑s ∪ ↑t) →
      y ∈ closure (↑s ∪ ↑t) →
        (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y

case mp.refine_4
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ n ≤ m + n

Tactic:
exact Nat.le_add_left _ _

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

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

Tactic:
exact Nat.le_add_left _ _

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

Goal state before:
pp: case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s

pp: case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s

Tactic:
· rw [← conj_mul]
      exact mul_mem ihx ihy

Goal state after:
case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s
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
s : Set G
H : Subgroup G
a : G
⊢ a * a⁻¹ ∈ H

Tactic:
mul_inv_cancel

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
s : Set G
H : Subgroup G
a : G
⊢ 1 ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

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

Tactic:
refine normal_iff_map_conj_eq.mpr fun g ↦ ?_

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ a • (univ \ s) = univ \ a • s

Tactic:
smul_set_sdiff,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ a • univ \ a • s = univ \ a • s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
⊢ map f (normalClosure s) = normalClosure (⇑f '' s)

Tactic:
have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) = normalClosure (⇑f '' s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) ≤ normalClosure (⇑f '' s)

pp: case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ normalClosure (⇑f '' s) ≤ map f (normalClosure s)

Tactic:
· exact map_normalClosure_le s f

Goal state after:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ normalClosure (⇑f '' s) ≤ map f (normalClosure s)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
⊢ l₁.prod ≤ l₂.prod

Tactic:
induction h with
  | slnil => rfl
  | cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
  | cons_cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    grw [ih' h₁.2]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx
  exact ⟨l, h1, (Multiset.prod_coe l).trans h2⟩

Goal state after:
Module: Mathlib.Logic.Denumerable

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

Tactic:
card_eq_zero,

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ {y ∈ range ↑(ofNat s 0) | y ∈ s} = ∅
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ ↑a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b

Tactic:
by
  induction l <;> simp [maximum_cons, *]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ofDual (s.min' hs) = (image (⇑ofDual) s).max' ⋯

Tactic:
simp [min'_eq_inf', max'_eq_sup']

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ofDual (s.max' hs) = (image (⇑ofDual) s).min' ⋯

Tactic:
simp [min'_eq_inf', max'_eq_sup']

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ toDual (s.min' hs) = (image (⇑toDual) s).max' ⋯

Tactic:
simp [min'_eq_inf', max'_eq_sup']

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ toDual (s.max' hs) = (image (⇑toDual) s).min' ⋯

Tactic:
simp [min'_eq_inf', max'_eq_sup']

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

Goal state before:
pp: case trans
α : Type u_1
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : powersetAux' l₁✝ ~ powersetAux' l₂✝
IH₂ : powersetAux' l₂✝ ~ powersetAux' l₃✝
⊢ powersetAux' l₁✝ ~ powersetAux' l₃✝

Tactic:
| trans _ _ IH₁ IH₂ =>

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

Goal state before:
pp: case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
x : ι
hx : x ∈ s.erase a
⊢ f x ≤ f a

Tactic:
hfa

Goal state after:
case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
x : ι
hx : x ∈ s.erase a
⊢ f x ≤ (image f s).max' hne
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case succ.trans
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₂✝
IH₂ : powersetCardAux (n + 1) l₂✝ ~ powersetCardAux (n + 1) l₃✝
⊢ powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₃✝

Tactic:
| trans _ _ IH₁ IH₂ =>

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

Goal state before:
pp: case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r → ∀ (n : κ), (f n).Pairwise r

pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (∀ (n : κ), (f n).Pairwise r) → (⋃ n, f n).Pairwise r

Tactic:
· intro H n
    exact Pairwise.mono (subset_iUnion _ _) H

Goal state after:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (∀ (n : κ), (f n).Pairwise r) → (⋃ n, f n).Pairwise r
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r ↔ ∀ (n : κ), (f n).Pairwise r

Tactic:
constructor
  · intro H n
    exact Pairwise.mono (subset_iUnion _ _) H
  · intro H i hi j hj hij
    rcases mem_iUnion.1 hi with ⟨m, hm⟩
    rcases mem_iUnion.1 hj with ⟨n, hn⟩
    rcases hd m n with ⟨p, mp, np⟩
    exact H p (mp hm) (np hn) hij

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b

Tactic:
apply Iff.intro

Goal state after:
case mp
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ s.sup f → ∃ b ∈ s, a ≤ f b

case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f
Module: Mathlib.Data.Finset.Lattice.Fold

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

Tactic:
apply Iff.intro

Goal state after:
case mp
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < s.sup f → ∃ b ∈ s, a < f b

case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b ∈ s, a < f b) → a < s.sup f
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 ∅
⊢ ⨅ i ∈ ↑s, f i ∈ f '' ↑s

Tactic:
simpa using Finset.ciInf_mem_image f h

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Iic a = Iic ↑a

Tactic:
by
  rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨆ x, ↑(f x) = ⊤ ↔ ¬BddAbove (range f)

Tactic:
iSup_eq_top,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ (∀ b < ⊤, ∃ i, b < ↑(f i)) ↔ ¬BddAbove (range f)
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ f ⁻¹' ↑s ⊆ ↑t

Tactic:
exact Set.preimage_subset (mod_cast hs) hf

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
P : α → Prop
a : α
ha : P a
⊢ ∃ b, b ≤ a ∧ Minimal P b

Tactic:
by
  obtain ⟨b, ⟨hba, hb⟩, hbmin⟩ :=
    exists_minimal_of_wellFoundedLT (fun b ↦ b ≤ a ∧ P b) ⟨a, le_rfl, ha⟩
  exact ⟨b, hba, hb, fun c hc hcb ↦ hbmin ⟨hcb.trans hba, hc⟩ hcb⟩

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : α
hx : Minimal P x
⊢ f x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}

Tactic:
exact (minimal_mem_image_monotone_iff hx.prop hf).2 hx

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ f x ∈ t) x
y : α
hyt : f y ∈ t
⊢ f y ≤ f x → f x ≤ f y

Tactic:
simp_rw [f.le_iff_le]

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ f x ∈ t) x
y : α
hyt : f y ∈ t
⊢ y ≤ x → x ≤ y
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}

Tactic:
by
  suffices h₁ : n ≤ sInf {m | p (m - n)} by
    convert! sInf_add h₁
    simp_rw [Nat.add_sub_cancel_right]
  obtain ⟨m, hm⟩ := nonempty_of_pos_sInf h
  refine
    le_csInf ⟨m + n, ?_⟩ fun b hb ↦
      le_of_not_gt fun hbn ↦
        ne_of_mem_of_not_mem ?_ (notMem_of_lt_sInf h) (Nat.sub_eq_zero_of_le hbn.le)
  · dsimp
    rwa [Nat.add_sub_cancel_right]
  · exact hb

Goal state after:
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
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩

Goal state after:
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
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad) m)) (f ((Nat.orderEmbeddingOfSet bad) n))
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ioo a b) = Ioo ↑a ↑b

Tactic:
by
  rw [subtype_Ioo_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Ioo] at hx
  exact hp hx.1.le hx.2.le a.prop b.prop

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

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1⁻¹ ∈ ↑S

Tactic:
rw [inv_one]; exact S.one_mem'

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ioc a b ∪ Ioc b c = Ioc a c

Tactic:
by
  rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
· obtain ⟨z, hxz, hz⟩ :=
      (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 <| hxy.lt_of_not_ge hxy'
    have z_card := calc
      #(Icc x z) ≤ #(Ico x y) := card_le_card <| Icc_subset_Ico_right hz.1.2
      _          < #(Icc x y) := this
    have h₁ := transGen_wcovBy_of_le hz.1.1
    have h₂ : z ⩿ y :=
      ⟨hz.1.2.le, fun c hzc hcy ↦ hzc.not_ge <| hz.2 ⟨hz.1.1.trans hzc.le, hcy⟩ hzc.le⟩
    exact .tail h₁ h₂

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
h : Injective fun x ↦ x • b
⊢ stabilizer G (a • b) = stabilizer G a

Tactic:
refine (le_stabilizer_smul_left _ _).antisymm' fun a ha ↦ ?_
  simpa only [mem_stabilizer_iff, ← smul_assoc, h.eq_iff] using ha

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
h : Injective fun x ↦ x • b
⊢ stabilizer G (a • b) = stabilizer G a

Tactic:
by
  refine (le_stabilizer_smul_left _ _).antisymm' fun a ha ↦ ?_
  simpa only [mem_stabilizer_iff, ← smul_assoc, h.eq_iff] using ha

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ x, IsBadSeq r s x

Tactic:
· rintro ⟨f, hf1, -⟩
    exact ⟨f, hf1⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ g✝ * x✝ = x✝ * g✝

Tactic:
← Units.val_inj,

Goal state after:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ ↑(g✝ * x✝) = ↑(x✝ * g✝)
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : Commute (f x) (f y)
⊢ f (x * y) = f (y * x)

Tactic:
by simpa only [map_mul] using h.eq

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

Goal state before:
pp: case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ List.foldr (fun x1 x2 ↦ x1 * x2) 1 (hd :: tl) = hd * tl.prod

Tactic:
List.foldr,

Goal state after:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ hd * List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = hd * tl.prod
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case inr
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
b : α
hb : b ∈ s.erase a
hab : a ≠ b
⊢ Commute a b

Tactic:
exact comm h (mem_of_mem_erase hb) hab

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

Goal state before:
pp: case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i * (univ.erase i).noncommProd (fun j ↦ Pi.mulSingle j (x j) i) ⋯ = x i

Tactic:
noncommProd_eq_pow_card (univ.erase i),

Goal state after:
case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i * ?convert_8.m ^ #(univ.erase i) = x i

case convert_8.m
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ M i

case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = ?convert_8.m
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ r ⊔ s = EqvGen.setoid (⇑r ⊔ ⇑s)

Tactic:
sup_eq_eqvGen

Goal state after:
α : Type u_1
r s : Setoid α
⊢ (EqvGen.setoid fun x y ↦ r x y ∨ s x y) = EqvGen.setoid (⇑r ⊔ ⇑s)