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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (fold op b₁ f (s₁ ∪ s₂)) (fold op b₂ f (s₁ ∩ s₂)) = op (fold op b₂ f s₁) (fold op b₁ f s₂)

Tactic:
unfold fold

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ List.Pairwise rb (map (⇑e) l) ↔ List.Pairwise ra l

Tactic:
simp [pairwise_map, e.map_rel_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ List.Pairwise (Function.swap rb) (map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l

Tactic:
simp [pairwise_map, e.map_rel_iff]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧
    True ∧ ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ

Tactic:
true_and,

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧ ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
inst✝ : Trans R R R
hl : IsChain R l₂
h : l₁ <+ l₂
⊢ IsChain R l₁

Tactic:
by
  rw [isChain_iff_pairwise] at hl ⊢
  exact hl.sublist h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case nil
M : Type u_8
inst✝ : CommMonoid M
h : IsUnit [].prod
⊢ ∀ (m : M), m ∈ [] → IsUnit m

Tactic:
exact fun m' h' => False.elim (not_mem_nil h')

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
⊢ a ∣ l.prod

Tactic:
let ⟨s, t, h⟩ := append_of_mem ha

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ l.prod
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-1) ^ (l.length + 1) * a ^ (-1) ^ l.reverse.length =
    (a / l.alternatingProd) ^ (-1) ^ ((a :: l).length + 1)

Tactic:
length_reverse,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-1) ^ (l.length + 1) * a ^ (-1) ^ l.length =
    (a / l.alternatingProd) ^ (-1) ^ ((a :: l).length + 1)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
x : α
⊢ l.rotate n = [x] ↔ [x] = l

Tactic:
rotate_eq_singleton_iff,

Goal state after:
α : Type u
l : List α
n : ℕ
x : α
⊢ l = [x] ↔ [x] = l
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
i : ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1
⊢ (map f m).prod = f i ^ count i m

Tactic:
induction m using Quotient.inductionOn
  simp [List.prod_map_eq_pow_single i f hf]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.offDiag = #s * #s - #s

Tactic:
rw [← sq]
  rcases s with ⟨⟨s⟩, hs⟩
  apply List.length_offDiag

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

Goal state before:
pp: a c : ℕ
⊢ a.choose c ≤ a.succ.choose c

Tactic:
cases c

Goal state after:
case zero
a : ℕ
⊢ a.choose 0 ≤ a.succ.choose 0

case succ
a n✝ : ℕ
⊢ a.choose (n✝ + 1) ≤ a.succ.choose (n✝ + 1)
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_4
inst✝ : MulOneClass M
S : Submonoid M
a : M
ha : a ∈ S
⊢ ⟨a, ha⟩ = 1 ↔ a = 1

Tactic:
by simp [← SetLike.coe_eq_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃ i ∈ C, i = ⋃ y ∈ C, s ×ˢ y

Tactic:
prod_iUnion₂

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
· rintro ⟨rfl, hn⟩
    exact empty_pow hn

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
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
have hst : (s * t).Nonempty := h.symm.subst one_nonempty

Goal state after:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ b ∈ t, (fun x ↦ f x b) '' s = image2 (fun a b ↦ f b a) t s

Tactic:
iUnion_image_left

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 (fun b x ↦ f x b) t s = image2 (fun a b ↦ f b a) t s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
⊢ image2 (fun f a ↦ f a) s t = ⋃ f ∈ s, f '' t

Tactic:
iUnion_image_left

Goal state after:
α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
⊢ image2 (fun f a ↦ f a) s t = image2 (fun f ↦ f) s t
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
x : ↥H
⊢ (inclusion ⋯) x = x

Tactic:
by
  cases x
  rfl

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
h : H ≤ K
x : ↥K
hx : ↑x ∈ H
⊢ (inclusion h) ⟨↑x, hx⟩ = x

Tactic:
by
  cases x
  rfl

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
L : S
hHK : H ≤ K
hKL : K ≤ L
x : ↥H
⊢ (inclusion hKL) ((inclusion hHK) x) = (inclusion ⋯) x

Tactic:
by
  cases x
  rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set M
⊢ sInf {a | s ⊆ ↑a.unop} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
Subsemigroup.coe_unop

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set M
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
⊢ ∀ {a b : N}, a ∈ ⇑f '' ↑S → b ∈ ⇑f '' ↑S → a * b ∈ ⇑f '' ↑S

Tactic:
rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f x * f y ∈ ⇑f '' ↑S
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ some x = some y

Tactic:
rw [← encodek, e, encodek]

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

Goal state before:
pp: case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b

Tactic:
apply Nat.add_lt_add_right

Goal state after:
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < 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
J : Subgroup (G × N)
⊢ J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K

Tactic:
by
  simpa only [← Subgroup.toSubmonoid_le] using! Submonoid.le_prod_iff

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
let k := Nat.find H
  have hk : p k := Nat.find_spec H
  suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
  by_contra! contra
  rw [le_zero_eq] at contra
  exact H' (contra ▸ hk)

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

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

Tactic:
rw [← apply_ite, ← apply_ite]

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val ↦ if f val < f tl then some tl else some val) (some (if f a < f m then m else a)) =
    Option.rec (some a) (fun val ↦ if f a < f val then some val else some a) (some (if f m < f tl then tl else m))
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.max = ↑a

Tactic:
rw [← insert_empty_eq]
  exact max_insert

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

Goal state before:
pp: α : Type u
β : Type u_1
⊢ RightInverse unzip (uncurry zip)

Tactic:
grind [zip_unzip]

Goal state after:
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) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)

Tactic:
· rcases init with - | ⟨hd', tl'⟩
      · simp
      · intro h
        right
        use tl', tail
        simp_all

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (cons a✝ s✝ h✝).sup (f ⊔ g) = (cons a✝ s✝ h✝).sup f ⊔ (cons a✝ s✝ h✝).sup g

Tactic:
| cons _ _ _ ih =>

Goal state after:
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 : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
hT : T ∈ s
hy : y ∈ T
⊢ x ≠ y → r x y

Tactic:
hne

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 : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
hT : T ∈ s
hy : y ∈ T
hne : x ≠ y
⊢ r x y
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : (∀ b ∈ s✝, p (f b)) → p (s✝.sup f)
hs : ∀ b ∈ cons a✝ s✝ h✝, p (f b)
⊢ p ((cons a✝ s✝ h✝).sup f)

Tactic:
| cons _ _ _ ih =>

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

Goal state before:
pp: case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ a ∈ (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯

Tactic:
rw [mem_disjiUnion]

Goal state after:
case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ ∃ a_1 ∈ range (#s + 1), a ∈ powersetCard a_1 s
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: ι : Type u_5
s : Set ι
x : ι
⊢ x ∈ ⋃ s', Subtype.val '' ↑s' ↔ x ∈ s

Tactic:
simp only [Set.mem_iUnion, Set.mem_image, SetLike.mem_coe, Subtype.exists,
    exists_and_right, exists_eq_right]

Goal state after:
ι : Type u_5
s : Set ι
x : ι
⊢ (∃ i, ∃ (x_1 : x ∈ s), ⟨x, ⋯⟩ ∈ i) ↔ x ∈ s
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
true_and,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ (¬∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
true_and,

Goal state after:
α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ (¬∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b
Module: Mathlib.Order.Cover

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s \ {a} ⩿ s

Tactic:
· simp [ha]

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
⊢ ∃ i, a < ↑(f i)

Tactic:
rcases hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩

Goal state after:
case refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ ∃ i, a < ↑(f i)
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, a i ⩿ x ∧ b = Function.update a i x

Tactic:
rintro ⟨i, hi, h⟩
    exact ⟨i, b i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, a i ⋖ x ∧ b = Function.update a i x

Tactic:
rintro ⟨i, hi, h⟩
    exact ⟨i, b i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩

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

Goal state before:
pp: b : ℕ
⊢ #(Ico ⊥ b) = b

Tactic:
card_Ico,

Goal state after:
b : ℕ
⊢ b - ⊥ = b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Set.uIcc a b)
x✝ : α
⊢ x✝ ∈ uIcc a b ↔ x✝ ∈ Set.uIcc a b

Tactic:
simp [Set.uIcc]

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case hnc
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ a ∈ s, a ≤ n

Tactic:
· exact hs

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂

Tactic:
by
  simpa [← coe_subset] using Set.Ioc_subset_Ioc ha hb

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
⊢ WellFounded fun a b ↦ r a b ∧ ¬r b a

Tactic:
by
  let _ : Preorder α :=
    { le := r
      le_refl := refl_of r
      le_trans := fun _ _ _ => trans_of r }
  have : WellQuasiOrderedLE α := ⟨h⟩
  exact wellFounded_lt

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : s.WellFoundedOn r
ht : t.WellFoundedOn r
⊢ (s ∪ t).WellFoundedOn r

Tactic:
wellFoundedOn_iff_no_descending_seq

Goal state after:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
⊢ ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s ∪ t
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ BddBelow s → s.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
wellFoundedOn_iff_no_descending_seq

Goal state after:
α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ BddBelow s → ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2), ¬∀ (n : ℕ), f n ∈ s
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)) ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f

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

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m < g 0 + n'
hn : ¬g 0 + n' < g 0
hm : m < g 0
hmn : List.SublistForall₂ r (f m) (f (g n')).tail
⊢ List.SublistForall₂ r (f m) (f (g n'))

Tactic:
exact _root_.trans hmn (List.tail_sublistForall₂_self _)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m < g 0 + n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ False

Tactic:
rw [← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)] at mn

Goal state after:
case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ False
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M

Tactic:
rw [div_eq_mul_inv]
  exact mul_mem_center ha (inv_mem_center hb)

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

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g = a⁻¹ * (g * a)

Tactic:
eq_inv_mul_iff_mul_eq,

Goal state after:
M : Type u_1
S : Set M
inst✝ : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ a * g = g * a
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
hg : g ∈ ⨅ i, normalizer ↑(H i)
⊢ g ∈ normalizer ↑(⨆ i, H i)

Tactic:
simp_rw [mem_iInf, mem_normalizer_iff_map_conj_eq, map_iSup, hg] at hg ⊢

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

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ ↑H * ↑K
g : G
⊢ g * n * g⁻¹ ∈ ↑H * ↑K

Tactic:
rcases hmem with ⟨h, hh, k, hk, rfl⟩

Goal state after:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
g h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
⊢ g * (fun x1 x2 ↦ x1 * x2) h k * g⁻¹ ∈ ↑H * ↑K
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ (MulAut.conj h)⁻¹ • H ≤ H

Tactic:
← map_inv

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ MulAut.conj h⁻¹ • H ≤ H
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ MulAut.conj h⁻¹ • H ≤ H

Tactic:
exact conj_smul_le_of_le (le_refl H) ⟨h⁻¹, H.inv_mem hh⟩

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

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

Tactic:
by
  ext i
  apply (univ.map_noncommProd (fun i ↦ MonoidHom.mulSingle M i (x i)) ?a
    (Pi.evalMonoidHom M i)).trans
  case a =>
    intro i _ j _ _
    exact Pi.mulSingle_apply_commute x i j
  convert! (noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _
  · intro j
    exact Pi.mulSingle j (x j) i
  · intro j _; dsimp
  · rw [noncommProd_insert_of_notMem _ _ _ _ (notMem_erase _ _),
      noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one]
    · simp only [Pi.mulSingle_eq_same]
    · simpa using fun _ a ↦ Pi.mulSingle_eq_of_ne (a ·.symm) _

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

Goal state before:
pp: case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ univ.noncommProd (fun i ↦ f (Pi.mulSingle i (x i))) ⋯ = g (univ.noncommProd (fun i ↦ Pi.mulSingle i (x i)) ⋯)

Tactic:
univ.map_noncommProd

Goal state after:
case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ univ.noncommProd (fun i ↦ f (Pi.mulSingle i (x i))) ⋯ = univ.noncommProd (fun i ↦ g (Pi.mulSingle i (x i))) ⋯
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ c.toSetoid = d.toSetoid → c = d

Tactic:
cases c

Goal state after:
case mk
M : Type u_1
inst✝ : Mul M
d : Con M
toSetoid✝ : Setoid M
mul'✝ : ∀ {w x y z : M}, toSetoid✝ w x → toSetoid✝ y z → toSetoid✝ (w * y) (x * z)
⊢ { toSetoid := toSetoid✝, mul' := mul'✝ }.toSetoid = d.toSetoid → { toSetoid := toSetoid✝, mul' := mul'✝ } = d