mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β))
      ((decode (unpair n).1).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (decode (unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
cases (decode n.unpair.1 : Option α) <;> cases (decode n.unpair.2 : Option β)
  <;> rfl

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

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ ↑(pi univ H) = ↑⊥ ↔ ∀ (i : η), ↑(H i) = ↑⊥

Tactic:
exact Set.univ_pi_eq_singleton_iff

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_6
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M
he : IsIdempotentElem e
f : F
⊢ IsIdempotentElem (f e)

Tactic:
rw [IsIdempotentElem, ← map_mul, he.eq]

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, map (↑(MulAut.conj g)) H

Tactic:
have : (⨅ g : G, H.map (MulAut.conj g) : Subgroup G).Normal := by
    refine normal_iff_map_conj_eq.mpr fun g ↦ ?_
    conv_rhs => rw [← Equiv.iInf_comp (Equiv.mulLeft g)]
    rw [map_iInf _ (MulAut.conj g).injective]
    simp [map_map, MulAut.mul_def]
  refine le_antisymm (le_iInf fun g ↦ ?_) ?_
  · grw [← Normal.map_conj_eq H.normalCore g, normalCore_le]
  · rw [normal_le_normalCore]
    apply iInf_le_of_le 1
    simp [MulAut.one_def]

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type ?u.3
s t : Set α
h✝ : s ⊆ t
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : (fun x ↦ ⟨↑x, ⋯⟩) ⟨x, hx⟩ = (fun x ↦ ⟨↑x, ⋯⟩) ⟨y, hy⟩
⊢ x = y

Tactic:
injection h

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

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

Tactic:
have : x ∈ closure s := by simp [hs]

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
this : x ∈ closure s
⊢ motive x
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
have : x ∈ closure s := by simp [hs]

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
this : x ∈ closure s
⊢ motive x
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
a : ℕ
ha : a ∈ s
hax : ↑x + 1 ≤ a
⊢ ↑x + (a - (↑x + 1)) + 1 ∈ s

Tactic:
by rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (a :: l).sublists'.length = 2 ^ (a :: l).length

Tactic:
simp +arith only [sublists'_cons, length_append, length_sublists' l,
      length_map, length, Nat.pow_succ']

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
⊢ sublistsAux a (r ++ [l]) = flatMap (fun l ↦ [l, a :: l]) (r ++ [l])

Tactic:
flatMap_append,

Goal state after:
α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ sublistsAux a (r ++ [l]) = flatMap (fun l ↦ [l, a :: l]) r ++ flatMap (fun l ↦ [l, a :: l]) [l]
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
S : Multiset α
⊢ ((range (S.card + 1)).bind fun k ↦ powersetCard k S) = S.powerset

Tactic:
induction S using Quotient.inductionOn

Goal state after:
case h
α : Type u_2
a✝ : List α
⊢ ((range (card ⟦a✝⟧ + 1)).bind fun k ↦ powersetCard k ⟦a✝⟧) = powerset ⟦a✝⟧
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (powerset ⟦l⟧).Nodup

Tactic:
simp only [quot_mk_to_coe, powerset_coe', coe_nodup]
      refine (nodup_sublists'.2 h).map_on ?_
      exact fun x sx y sy e =>
        (h.perm_iff_eq_of_sublist (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f (g i) ⊔ s.sup (⇑f ∘ g) = (⇑f ∘ g) i ⊔ s.sup (⇑f ∘ g)

Tactic:
Function.comp_apply

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f (g i) ⊔ s.sup (⇑f ∘ g) = f (g i) ⊔ s.sup (⇑f ∘ g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
⊢ (s.erase ⊥).sup id = s.sup id

Tactic:
refine (sup_mono (s.erase_subset _)).antisymm (Finset.sup_le_iff.2 fun a ha => ?_)

Goal state after:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ id a ≤ (s.erase ⊥).sup id
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c) ⊔ t.sup (g ∘ f) = (g ∘ f) c ⊔ t.sup (g ∘ f)

Tactic:
Function.comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c) ⊔ t.sup (g ∘ f) = g (f c) ⊔ t.sup (g ∘ f)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a ↦ sublistsLen (a + 1) tl) (range tl.length ++ [tl.length]) ~ tl.sublists'

Tactic:
flatMap_append,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++
      (flatMap (fun a ↦ sublistsLen (a + 1) tl) (range tl.length) ++
        flatMap (fun a ↦ sublistsLen (a + 1) tl) [tl.length]) ~
    tl.sublists'
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : 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₂)
hs : ∀ b ∈ s, p (f b)
⊢ p (s.sup f)

Tactic:
induction s using Finset.cons_induction with
  | empty => exact hb
  | cons _ _ _ ih =>
    simp only [sup_cons, forall_mem_cons] at hs ⊢
    exact hp _ hs.1 _ (ih hs.2)

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
    exists_eq_or_imp, exists_eq_left, or_imp, imp_self, true_and]

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: 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⟩

Tactic:
intro ⟨i, h⟩
    have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
    rw [this]
    refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i
    simp_rw [ciSup_eq_ite]
    refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_
    grind

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrder α
a : α
inst✝ : Nonempty ι
f : ι → α
hb : BddAbove (range f)
⊢ a < iSup f ↔ ∃ i, a < f i

Tactic:
by
  simpa only [mem_range, exists_exists_eq_and] using! lt_csSup_iff hb (range_nonempty _)

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

Tactic:
by_cases hp : p <;>
  by_cases hq : q

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : ¬q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : ¬q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
p : (i : ι) → α i → Prop
inst✝ : (i : ι) → DecidablePred (p i)
⊢ {x ∈ s.sigma t | p x.fst x.snd} = s.sigma fun i ↦ filter (p i) (t i)

Tactic:
simp [filter_sigma]

Goal state after:
Module: Mathlib.Order.Cover

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

Tactic:
rw [covBy_iff]
  constructor
  · rintro ⟨i, hi, h⟩
    exact ⟨i, a i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩
  · rintro ⟨i, x, h, rfl⟩
    exact ⟨i, by simpa +contextual⟩

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal P x
⊢ Q x

Tactic:
obtain ⟨y, hyx, hy⟩ := h h'.prop
    rwa [((h'.le_of_le (hPQ hy)) hyx).antisymm hyx]

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

Goal state before:
pp: s : Set ℕ
h : s.Nonempty
⊢ sInf s ∈ s

Tactic:
rw [Nat.sInf_def h]

Goal state after:
s : Set ℕ
h : s.Nonempty
⊢ Nat.find h ∈ s
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    a ≤ x ∧ x ≤ b

Tactic:
cases a <;> cases b

Goal state after:
case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ ⊤

case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ ↑a✝

case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝ ≤ x ∧ x ≤ ⊤

case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝¹ ≤ x ∧ x ≤ ↑a✝
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    a ≤ x ∧ x < b

Tactic:
cases a <;> cases b

Goal state after:
case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < ⊤

case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < ↑a✝

case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝ ≤ x ∧ x < ⊤

case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝¹ ≤ x ∧ x < ↑a✝
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    a < x ∧ x ≤ b

Tactic:
cases a <;> cases b

Goal state after:
case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ ⊤

case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ ↑a✝

case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝ < x ∧ x ≤ ⊤

case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝¹ < x ∧ x ≤ ↑a✝
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    a < x ∧ x < b

Tactic:
cases a <;> cases b

Goal state after:
case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < ⊤

case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < ↑a✝

case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝ < x ∧ x < ⊤

case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝¹ < x ∧ x < ↑a✝
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s) → ∃ x, ∀ (n : ℕ), x n ∈ s

Tactic:
rintro ⟨⟨f, hf⟩⟩

Goal state after:
case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
⊢ ∃ x, ∀ (n : ℕ), x n ∈ s
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ s * ↑(closure s) = ↑(closure s)

Tactic:
rw [← smul_eq_mul, ← Set.iUnion_smul_set]
  have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s :=
    smul_coe_set <| subset_closure ha
  simp +contextual [h, hs]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹ = Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹}

Tactic:
Set.inv_singleton

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹} = Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
⊢ ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H

Tactic:
intro n hn g

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ g * n * g⁻¹ ∈ H
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ ∀ (a : ↑x * ↑y = 1) (a' : ↑x' * ↑y' = 1), a ≍ a' → (fun hyx ↦ f x y ⋯ ⋯) ≍ fun hyx ↦ f x' y' ⋯ ⋯

Tactic:
· rintro Hxy Hxy' -
    refine Function.hfunext ?_ ?_
    · rw [c.eq.2 hx, c.eq.2 hy]
    · rintro Hyx Hyx' -
      exact heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
⊢ (fun g ↦ ⇑g ∘ of) ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) f) = f

Tactic:
by ext; simp [of, Lift.aux]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
g : FreeGroup α →* β
⊢ (fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) ((fun g ↦ ⇑g ∘ of) g) = g

Tactic:
by ext; simp [of, Lift.aux]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ (⇑prod ∘ ⇑(map f)) x = prod ((map f) x)

Tactic:
Function.comp_apply

Goal state after:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ prod ((map f) x) = prod ((map f) x)
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s t : Set G
⊢ mk '' s = mk '' t ↔ ↑N * s = ↑N * t

Tactic:
simp_rw [← preimage_image_coe]

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s t : Set G
⊢ mk '' s = mk '' t ↔ mk ⁻¹' mk '' s = mk ⁻¹' mk '' t
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Unique ι
s : Finset ι
f : ι → M
h : s.Nonempty
⊢ ∏ x ∈ s, f x = f default

Tactic:
h.eq_singleton_default,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Unique ι
s : Finset ι
f : ι → M
h : s.Nonempty
⊢ ∏ x ∈ {default}, f x = f default
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
⊢ (∏ i, f ↑i) * ∏ i, f ↑i = ∏ i, f i

Tactic:
classical
    let s := { x | p x }.toFinset
    rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
    · exact Finset.prod_mul_prod_compl _ _
    · simp [s]
    · simp [s]

Goal state after: