mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
⊢ False

Tactic:
by
          obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa
          obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb
          refine disjoint_left.mp
            (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) ?_) hga
            hgb
          rintro rfl
          exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l.reverse ~r l'.reverse ↔ l ~r l'

Tactic:
simp [isRotated_reverse_comm_iff]

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

Goal state before:
pp: α : Type u
l' l : List α
h : l' ∈ l.cyclicPermutations
⊢ l'.length = l.length

Tactic:
obtain ⟨k, hk, rfl⟩ := get_of_mem h
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
and_comm

Goal state after:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
Nat.zero_mul,

Goal state after:
case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ 0 = 0 * (n + 1 - (k + 1))
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
b : β a'
hb : b ∈ t a'
ha' : a' ∈ a' ::ₘ m
⊢ Pi.cons m a' b f' a' ha' ∈ t a'

Tactic:
rwa [Pi.cons_same]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a = b
⊢ IsConj a b

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
h : a = 1
⊢ IsConj 1 a

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r ∈ {s} ×ˢ T, r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t

Tactic:
singleton_prod,

Goal state after:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r ∈ Prod.mk s '' T, r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a * x) '' t = (fun x ↦ a⁻¹ * x) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse]

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse (fun x ↦ a⁻¹ * x) fun x ↦ a * x

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse (fun x ↦ a⁻¹ * x) fun x ↦ a * x
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a * x) '' t = (fun x ↦ a⁻¹ * x) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x * b) '' t = (fun x ↦ x * b⁻¹) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse]

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse (fun x ↦ x * b⁻¹) fun x ↦ x * b

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse (fun x ↦ x * b⁻¹) fun x ↦ x * b
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x * b) '' t = (fun x ↦ x * b⁻¹) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a / x) '' t = (fun x ↦ x⁻¹ * a) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse]

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse (fun x ↦ x⁻¹ * a) fun x ↦ a / x

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse (fun x ↦ x⁻¹ * a) fun x ↦ a / x
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a / x) '' t = (fun x ↦ x⁻¹ * a) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x / b) '' t = (fun x ↦ x * b) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse]

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse (fun x ↦ x * b) fun x ↦ x / b

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse (fun x ↦ x * b) fun x ↦ x / b
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x / b) '' t = (fun x ↦ x * b) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

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
K : Subgroup G
f : G →* N
⊢ ∀ (x : N), (∃ x_1, ∃ (_ : x_1 ∈ K), f x_1 = x) ↔ ∃ x_1 ∈ K, f x_1 = x

Tactic:
exists_prop,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ ∀ (x : N), True
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ k ∈ f.range.subgroupOf K ↔ k ∈ (f.codRestrict K ⋯).range

Tactic:
refine exists_congr ?_

Goal state after:
G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ ∀ (a : G₁), f a = K.subtype k ↔ (f.codRestrict K ⋯) a = k
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0

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

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:
cases b <;> dsimp [bit] <;> lia

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ ¬decode₂ α n = none ↔ ∃ y, encode y = n

Tactic:
Option.eq_none_iff_forall_not_mem,

Goal state after:
α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ (¬∀ (a : α), a ∉ decode₂ α n) ↔ ∃ y, encode y = n
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
if_neg h.not_gt,

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ max m n ^ 2 + min m n ≤ m * m + m + n
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: a b k : ℤ
⊢ b = (fun x ↦ x • a) k ↔ b = k * a

Tactic:
← smul_eq_mul

Goal state after:
a b k : ℤ
⊢ b = (fun x ↦ x • a) k ↔ b = k • a
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
K : Subgroup N
⊢ H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥

Tactic:
by
  simpa only [← Subgroup.toSubmonoid_inj] using! Submonoid.prod_eq_bot_iff

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ g ∈ normalizer s ↔ ⇑(MulAut.conj g) '' s = s

Tactic:
by
  simp_rw [mem_set_normalizer_iff'', Set.ext_iff, Set.mem_image, MulAut.conj_apply]
  refine forall_congr' fun h ↦ ?_
  simp_rw [mul_inv_eq_iff_eq_mul, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, exists_eq_right, iff_comm]

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

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

Tactic:
rw [← (Equiv.inv G).iInf_comp, normalCore_eq_iInf_map_conj]
  simp [MulAut.inv_def, map_equiv_eq_comap_symm]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ map (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) ⊤ ≤ normalClosure {⟨c * g * c⁻¹, hg'⟩}

Tactic:
grw [eq_top_iff.1 ht]

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ map (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) (normalClosure {⟨g, hg⟩}) ≤
    normalClosure {⟨c * g * c⁻¹, hg'⟩}
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Set.range (Subtype.val ∘ ofNat s) = s

Tactic:
rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]

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

Goal state before:
pp: α : Type u
s : List α
h : s = []
⊢ s <+ []

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.reverse.sublists' = map reverse l.sublists

Tactic:
by
  simp only [sublists_eq_sublists', map_map, map_id'' reverse_reverse, Function.comp_def]

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

Goal state before:
pp: α : Type u
n : ℕ
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen n l₁ <+ sublistsLen n l₂

Tactic:
induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_
  induction h with
  | slnil => rfl
  | cons a _ IH =>
    refine IH.trans ?_
    rw [sublistsLen_succ_cons]
    apply sublist_append_left
  | cons_cons a s IH => simpa only [sublistsLen_succ_cons] using IH.append ((IHn s).map _)

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

Goal state before:
pp: case cons
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
b : α
l₁ : List α
sl₁ : b :: l₁ <+ l
⊢ Lex (Function.swap R) (b :: l₁) (a :: l₂)

Tactic:
exact Lex.rel (H₁ _ <| sl₁.subset mem_cons_self)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ≠ s ∧ t ⊆ s ↔ t ⊆ s ∧ t ≠ s

Tactic:
and_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ⊆ s ∧ t ≠ s ↔ t ⊆ s ∧ t ≠ s
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
H : BddAbove (range fun x ↦ f ↑x)
⊢ ⨆ x, f ↑x = f a

Tactic:
apply (hd.le_ciSup H (⟨a, le_refl a⟩ : Iic a)).antisymm'

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
H : BddAbove (range fun x ↦ f ↑x)
⊢ ⨆ j, f ↑j ≤ f ↑⟨a, ⋯⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr
α : 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 ι
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
refine le_antisymm (ciSup_le ?_) ?_

Goal state after:
case inr.refine_1
α : 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 ι
⊢ ∀ (x : Subtype p), f x ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

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
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
ciSup_of_not_bddAbove hf,

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (sSup ∅) (⨆ x, g x)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ (∃ x, ∃ (_ : a < x), ¬¬x < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
exists_prop,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ (∃ x, a < x ∧ ¬¬x < b) ↔ ∃ c, a < c ∧ c < b
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 ?_
  rintro ⟨j, x⟩ ⟨y, hys, hxy⟩
  simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy
  grind

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ (∃ x, ∃ (_ : a < x), ¬¬x < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
exists_prop,

Goal state after:
α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ (∃ x, a < x ∧ ¬¬x < b) ↔ ∃ c, a < c ∧ c < b
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ (¬∃ i ∈ s, (t i).Nonempty) ↔ ∀ i ∈ s, t i = ∅

Tactic:
simp only [not_nonempty_iff_eq_empty, not_and, not_exists]

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 P x ∧ Q x

Tactic:
and_comm

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x : α
inst✝ : Preorder α
hx : P x
⊢ (∃ y, P y ∧ y ≤ x ∧ ¬x ≤ y) ↔ ∃ y, (y ≤ x ∧ ¬x ≤ y) ∧ P y

Tactic:
and_comm

Goal state after:
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:
mem_Ioc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : OrderTop α
a✝ x✝ a x : α
⊢ a < x ∧ x ≤ ⊤ ↔ a < x
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n + 1), u k = (⨆ k, ⨆ (_ : k ≤ n), u k) ⊔ u (n + 1)

Tactic:
simp_rw [← Nat.lt_succ_iff, iSup_lt_succ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f x ∈ Ioc (f a) (f b) ↔ a < x ∧ x ≤ b

Tactic:
mem_Ioc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f a < f x ∧ f x ≤ f b ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g m)) ((Prod.fst ∘ f) (g n))
⊢ ∃ m n, m < n ∧ (fun a b ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
obtain ⟨m, n, h, hf⟩ := hs (Prod.snd ∘ f ∘ g)

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g m)) ((Prod.fst ∘ f) (g n))
m n : ℕ
h : m < n
hf : s ((Prod.snd ∘ f ∘ ⇑g) m) ((Prod.snd ∘ f ∘ ⇑g) n)
⊢ ∃ m n, m < n ∧ (fun a b ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: ι : 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 ι
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
have : IsPreorder (∀ i, α i) (fun a b : ∀ i, α i => ∀ i, r i (a i) (b i)) :=
    { refl a i := refl (a i)
      trans a b c hab hbc i := _root_.trans (hab i) (hbc i) }

Goal state after:
ι : 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)
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: ι : 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)
this : ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
by
    rw [wellQuasiOrdered_iff_exists_monotone_subseq]
    intro f
    simpa only [Finset.mem_univ, true_imp_iff] using! this Finset.univ f

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
⊢ ↑x ∈ Ioc ↑a ↑b ↔ a < x ∧ x ≤ b

Tactic:
mem_Ioc,

Goal state after:
α : 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
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inl
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), ↑(f (g n)) ∈ s
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
rcases hs.exists_lt hgs with ⟨m, n, hlt, hr⟩

Goal state after:
case inl
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), ↑(f (g n)) ∈ s
m n : ℕ
hlt : m < n
hr : r ↑(f (g m)) ↑(f (g n))
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this : Fintype ι
⊢ (univ.pi s).PartiallyWellOrderedOn fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
have : IsPreorder (∀ i, α i) (fun a b : ∀ i, α i => ∀ i, r i (a i) (b i)) :=
    { refl a i := refl (a i)
      trans a b c hab hbc i := _root_.trans (hab i) (hbc i) }

Goal state after:
ι : 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)
⊢ (univ.pi s).PartiallyWellOrderedOn fun a b ↦ ∀ (i : ι), r i (a i) (b i)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ≠ b ∧ a✝ ≤ b ↔ a✝ ≤ b ∧ a✝ ≠ b

Tactic:
and_comm

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

Goal state before:
pp: case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := ⋯
f : α → Quotient (orbitRel G α) := ⋯
a : α
⊢ a ∈ f ⁻¹' f '' U → a ∈ ⋃ g, (fun x ↦ g • x) '' U

Tactic:
rintro ⟨b, hb, hab⟩

Goal state after:
case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a b : α
hb : b ∈ U
hab : f b = f a
⊢ a ∈ ⋃ g, (fun x ↦ g • x) '' U
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
h : s.IsPWO
⊢ s.IsWF

Tactic:
by
  simpa only [← lt_iff_le_not_ge] using! h.wellFoundedOn

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
simp_rw [mem_uIcc]
  exact Set.eq_of_mem_uIcc_of_mem_uIcc'

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⩿ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
simpa [transGen_eq_self] using TransGen.lift f h a b <| le_iff_transGen_wcovBy.mp hab

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 : β
a : G
h : a • a✝ = a✝
⊢ (a • a✝) • b = a✝ • b

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a✝ : α
b : β
a : G'
h : a • b = b
⊢ a✝ • a • b = a✝ • b

Tactic:
rw [h]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x ↦ (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})
⊢ {y | toLex (a, y) ∈ s}.IsPWO

Tactic:
rw [h]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x ↦ (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})
⊢ (f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})).IsPWO
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ normalizer {g} → h ∈ centralizer {g}

Tactic:
rintro hh g rfl

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ normalizer {g}
⊢ g * h = h * g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
x✝ : ι
⊢ x✝ = (Equiv.symm σ) (σ x✝)

Tactic:
rw [Equiv.symm_apply_apply]

Goal state after: