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

Goal state before:
pp: α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).rotate ↑⟨n, hn⟩ = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩

Tactic:
rotate_rotate,

Goal state after:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate (k + ↑⟨n, hn⟩) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
⊢ (cons m a (φ b) fun a' ha' ↦ φ (f a' ha')) = fun a' ha' ↦ φ (cons m a b f a' ha')

Tactic:
by
  ext a' ha'
  refine (congrArg₂ _ ?_ rfl).trans (apply_dite (@φ _) (a' = a) _ _).symm
  ext rfl
  rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
⊢ #u = (#s).choose 2

Tactic:
have disj : Disjoint u v := by grind [disjoint_left]

Goal state after:
α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
⊢ #u = (#s).choose 2
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!

Tactic:
add_choose_mul_factorial_mul_factorial

Goal state after:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1))! = (m * (p + 1) + (p + 1))!
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))

Tactic:
add_choose_mul_factorial_mul_factorial

Goal state after:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p)! * ((p + 1) * (m + 1))
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
· refine h.elim fun f => ?_
    have : Finite α := Finite.of_injective _ f.injective
    exact Finite.of_injective _ DFunLike.coe_injective

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this✝ : Finite ↑s
this : Finite ↑t
⊢ (s ×ˢ t).Finite

Tactic:
apply toFinite

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this✝ : Finite ↑s
this : Finite ↑t
⊢ (image2 f s t).Finite

Tactic:
apply toFinite

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 [iUnion_inter, inter_iUnion]

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 [iUnion_inter, inter_iUnion]

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

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

Tactic:
rw [← image_inv_eq_inv, image_image, ← image_inv_of_apply_inv_eq H]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : InvolutiveInv α
s : Set α
inst✝ : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
| f '' s⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x : ↥H
n : ℤ
⊢ ↑(x ^ n) = ↑x ^ n

Tactic:
by
  dsimp

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1

pp: case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

pp: case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹

Tactic:
· exact ⟨0, zpow_zero x⟩

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹
Module: Mathlib.Algebra.Group.Subgroup.MulOpposite

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.op.toSubsemigroup = H.op

Tactic:
by
  dsimp

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.toSubsemigroup = H.unop

Tactic:
by
  dsimp

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

Goal state before:
pp: a₁ a₂ b : ℕ
h : a₁ < a₂
⊢ pair a₁ b < pair a₂ b

Tactic:
by_cases h₁ : a₁ < b <;> simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
  · by_cases h₂ : a₂ < b
    · simp [h₂, h]
    simp only [h₂, ↓reduceIte]
    apply Nat.add_lt_add_of_le_of_lt
    · exact Nat.mul_self_le_mul_self (not_lt.mp h₂)
    · exact Nat.lt_add_right _ h
  · simp at h₁
    simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]
    apply add_lt_add
    · exact Nat.mul_self_lt_mul_self h
    · apply Nat.add_lt_add_right; assumption

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

Goal state before:
pp: m n : ℕ
a b : Bool
h : m < n
⊢ 2 * n ≤ bit b n

Tactic:
by cases b <;> dsimp [bit] <;> lia

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

Goal state before:
pp: ⊢ bits 0 = []

Tactic:
simp [Nat.bits]

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 : N →* G
h : H ≤ f.range
⊢ normalizer ↑(map f (comap f H)) ≤ normalizer ↑H

Tactic:
rw [map_comap_eq_self h]

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

Goal state before:
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:
← conj_inv

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
h : a ∈ H.normalCore
b c : G
⊢ c * (b * a * b⁻¹) * c⁻¹ ∈ H

Tactic:
by
    rw [mul_assoc, mul_assoc, ← mul_inv_rev, ← mul_assoc, ← mul_assoc]; exact h (c * b)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ (∀ ⦃i j : α⦄, i ≠ j → Disjoint ((j⁻¹ * i) • s) s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
← not_imp_not (b := _ ≠ _),

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ (∀ ⦃i j : α⦄, ¬Disjoint ((j⁻¹ * i) • s) s → ¬i ≠ j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
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₃
b : G₂
⊢ ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) ((fun φ ↦ ⟨φ.comp f, ⋯⟩) φ)) b = φ b

Tactic:
simp [liftOfRightInverseAux, hf b]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ normalizer ↑(comap f H) = ⊤ ↔ H.Normal

Tactic:
← comap_normalizer_eq_of_surjective H hf,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ comap f (normalizer ↑H) = ⊤ ↔ H.Normal
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case right
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i : ι
b₁✝ b₂✝ : α i
hab : s₁ i b₁✝ b₂✝
⊢ Lex r₂ s₂ ⟨i, b₁✝⟩ ⟨i, b₂✝⟩

Tactic:
exact Lex.right _ (hs _ _ _ hab)

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 : ℕ
x : ↥(powers x✝)
⊢ ↑(x ^ (↑m.succ).natMod ↑n) = ↑(x ^ (↑m).natMod ↑n * x)

Tactic:
obtain ⟨_, k, rfl⟩ := x

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

Tactic:
obtain ⟨_, k, rfl⟩ := x

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 : ℕ
⊢ ↑(⟨(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))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ argmax id l = some m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

Tactic:
argmax_eq_some_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → idxOf m l ≤ idxOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → idxOf m l ≤ idxOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

Tactic:
simp only [id_eq, and_congr_right_iff, and_iff_left_iff_imp]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → idxOf m l ≤ idxOf a l
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:
rw [← map_top f, (EquivLike.injective f).eq_iff]

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

Goal state before:
pp: case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails → init ++ tail = hd :: tl

Tactic:
rw [mem_cons, zip_map_left, mem_map, Prod.exists]

Goal state after:
case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ ((init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)) →
    init ++ tail = hd :: tl
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl → (init, tail) ∈ ([], hd :: tl) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails

Tactic:
rw [mem_cons, zip_map_left, mem_map, Prod.exists]

Goal state after:
case mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r : List (List α)
⊢ sublistsAux a [] = flatMap (fun l ↦ [l, a :: l]) []

Tactic:
simp [sublistsAux]

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

Goal state before:
pp: α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ foldl (fun r l ↦ r ++ [l, a :: l]) (foldl (fun r l ↦ r ++ [l, a :: l]) [] r) [l] = sublistsAux a r ++ [l, a :: l]

Tactic:
simp [sublistsAux]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

Tactic:
simp only [hp, ciSup_unique]
  simp only [iSup]
  congr
  apply Subset.antisymm
  · rintro - ⟨i, rfl⟩
    simp
  · rintro - ⟨i, rfl⟩
    simp

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

Goal state before:
pp: ι : Type u_5
s : Set ι
hs : s.Nonempty
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
⊢ ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)

Tactic:
by
  rcases hs with ⟨j, hj⟩
  have : Nonempty ι := Nonempty.intro j
  refine le_antisymm ((WithBot.coe_iSup (OrderTop.bddAbove _)).trans_le <|
    iSup_le_iff.mpr fun i ↦ ?_) <| iSup_le_iff.mpr <| fun _ ↦ iSup_le_iff.mpr <|
      fun hi ↦ WithBot.coe_le_coe.mpr (le_biSup _ hi)
  by_cases h : i ∈ s
  · simpa only [iSup_pos h] using by apply le_biSup _ h
  · simpa only [iSup_neg h] using le_trans (by simp) (le_biSup _ hj)

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

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

Tactic:
refine ciSup_le fun i ↦ ?_
    simp_rw [ciSup_eq_ite]
    split_ifs
    · exact le_ciSup hf ?_
    · exact hf'

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → t ⊆ s → P s
h : Minimal P s
x : α
hxs : x ∈ s
hx : P (s.erase x)
⊢ False

Tactic:
simpa using h.le_of_le hx (erase_subset _ _) hxs

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
x✝ : IsTop b ∧ a ⋖ b
hb : IsTop b
hab : a ⋖ b
⊢ Ioi a = {b}

Tactic:
by
    cases b, hb using IsTop.rec; rwa [← Ioc_top, Ioc_eq_singleton_right_iff]

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

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

Tactic:
by simp [isEmpty_iff]

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

Goal state before:
pp: α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
ht : image Sigma.fst s ⊆ t
⊢ {a ∈ s | a.fst ∈ t} = s

Tactic:
filter_true_of_mem <| image_subset_iff.1 ht

Goal state after:
α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
ht : image Sigma.fst s ⊆ t
⊢ s = s
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
Nat.sInf_def ⟨m, hm⟩,

Goal state after:
case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find ⋯ + n = sInf {m | p m}
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
obtain h := WellFoundedGT.monotone_chain_condition a

Goal state after:
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
h : ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m
⊢ a m ≤ monotonicSequenceLimit a
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ P n

Tactic:
by
  apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl
  · intro n ih m hm
    rcases hm.eq_or_lt with rfl | hm
    · exact step n ih
    · exact ih m hm
  · rintro ⟨b, hb⟩
    rcases base with ⟨n, hn⟩
    specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
    all_goals lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ a ≤ x ∧ ↑x < ↑b ↔ a ≤ x ∧ x < b

Tactic:
Subtype.coe_lt_coe

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑a < ↑x ∧ x ≤ b ↔ a < x ∧ x ≤ b

Tactic:
Subtype.coe_lt_coe

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑a < ↑x ∧ ↑x < ↑b ↔ a < x ∧ x < b

Tactic:
Subtype.coe_lt_coe

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ ↑a < ↑x ↔ a < x

Tactic:
Subtype.coe_lt_coe

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

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ False

Tactic:
induction hs : Finset.Icc a b using Finset.strongInduction generalizing b with | H i ih

Goal state after:
case H
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a : α
i : Finset α
ih : ∀ t ⊂ i, ∀ (b : α), a < b → Icc a b = t → False
b : α
h : a < b
hs : Icc a b = i
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) ⋯

Tactic:
classical rw [cons_eq_insert, Iio_insert]

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 α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ Disjoint (f '' U) (f '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V

Tactic:
refine
    ⟨fun h a a_in_U g g_in_V =>
      h.le_bot ⟨⟨a, a_in_U, Quotient.sound ⟨g⁻¹, ?_⟩⟩, ⟨g • a, g_in_V, rfl⟩⟩, ?_⟩

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : Disjoint (f '' U) (f '' V)
a : α
a_in_U : a ∈ U
g : G
g_in_V : g • a ∈ V
⊢ (fun m ↦ m • g • a) g⁻¹ = a

case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ (∀ x ∈ U, ∀ (g : G), g • x ∉ V) → Disjoint (f '' U) (f '' V)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ Quotient.mk'' a = Quotient.mk'' a✝

Tactic:
Quotient.eq''

Goal state after:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ (orbitRel G α) a a✝
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ Quotient.mk'' a = Quotient.mk'' b ↔ Quotient.mk'' ↑a = Quotient.mk'' ↑b

Tactic:
Quotient.eq''

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ (orbitRel ↥H ↑x.orbit) a b ↔ (orbitRel (↥H) α) ↑a ↑b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt]
  exact forall_congr' fun f => by simp [IsBadSeq]

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

Goal state before:
pp: case single
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y b✝ : α
hx : x ⋖ b✝
⊢ x < b✝

Tactic:
exact hx.1

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

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
⊢ a⁻¹ ∈ center M

Tactic:
rw [_root_.Semigroup.mem_center_iff]
  intro _
  rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
⊢ ∃ g', Monotone fun n ↦ (ofLex f (g (g' n))).2

Tactic:
simp_rw [isPWO_iff_exists_monotone_subseq] at hβ
      apply hβ (ofLex f (g 0)).1 fun n ↦ (ofLex f (g n)).2
      intro n
      rw [hhc n]
      simpa using! hf _

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

Goal state before:
pp: case mul.refine_1
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ x'⁻¹ * y * x' ∈ N

Tactic:
exact (mem_normalizer_iff''.mp (hLE hx') y).mp hy

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
hHnK : normalizer ↑H ≤ normalizer ↑K
⊢ normalizer ↑H ≤ normalizer ↑(H ⊔ K)

Tactic:
exact normalizer_le_normalizer_sup_of_normalizer_le_left hHnK

Goal state after: