mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

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

Tactic:
smul_set_univ

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:
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.Algebra.Group.Subgroup.Basic

Goal state before:
pp: M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
H : Subgroup G
⊢ Subgroup.map H.subtype (I.inertia ↥H) = I.inertia G ⊓ H

Tactic:
rw [← AddSubgroup.subgroupOf_inertia, Subgroup.subgroupOf_map_subtype]

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
k : ℕ
⊢ (x ^ n) ^ k = 1

Tactic:
hx,

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
k : ℕ
⊢ 1 ^ k = 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
⊢ l[i] ≤ maximum_of_length_pos h

Tactic:
apply le_maximum_of_length_pos_of_mem

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
⊢ l[i] ∈ l
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeInf β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ ⊤ ⊓ ⊤ = ⊤

Tactic:
inf_top_eq

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeInf β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ ⊤ = ⊤
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: case empty
α : Type u_2
inst✝ : LinearOrder α
⊢ ∀ {a : α}, ∅.max = ↑a → a ∈ ∅

Tactic:
intro _ H

Goal state after:
case empty
α : Type u_2
inst✝ : LinearOrder α
a✝ : α
H : ∅.max = ↑a✝
⊢ a✝ ∈ ∅
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α), ⟦a⟧ ∈ powersetCardAux n l ↔ ⟦a⟧ ≤ ↑l ∧ card ⟦a⟧ = n

Tactic:
by
    simp only [quot_mk_to_coe, powersetCardAux_eq_map_coe, List.mem_map, mem_sublistsLen,
      coe_eq_coe, coe_le, Subperm, coe_card]
    exact fun l₁ =>
      ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩,
       fun ⟨⟨l₂, p, s⟩, e⟩ => ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
⊢ (Disjoint on f) a b

Tactic:
obtain hcd | hcd := eq_or_ne (g c) (g d)

Goal state after:
case inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c = g d
⊢ (Disjoint on f) a b

case inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c ≠ g d
⊢ (Disjoint on f) a b
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
refine (hs hi.1 hj.1 hij).mono ?_ ?_
    · convert! le_iSup₂ (α := α) i' hi.2; rfl
    · convert! le_iSup₂ (α := α) j' hj.2; rfl

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ u

Tactic:
rw [← insert_erase hx, powersetCard_succ_insert (notMem_erase _ _)]

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ (u.erase x) ∪ image (insert x) (powersetCard n (u.erase x))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : LinearOrder α
s : Finset ι
f : ι → α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup f) = s.sup (g ∘ f)

Tactic:
rw [← Finset.sup'_eq_sup H, ← Finset.sup'_eq_sup H]

Goal state after:
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : LinearOrder α
s : Finset ι
f : ι → α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : LinearOrder α
s : Finset ι
f : ι → α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup f) = s.sup (g ∘ f)

Tactic:
by
  rw [← Finset.sup'_eq_sup H, ← Finset.sup'_eq_sup H]
  exact Finset.apply_sup'_eq_sup'_comp H g (fun x y ↦ Monotone.map_sup mono_g x y)

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ (⋃ a, ↑(f a)).Finite

Tactic:
rw [← biUnion_range]

Goal state after:
α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ (⋃ x ∈ range f, ↑x).Finite
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
f : ι → α
⊢ univ.inf' ⋯ f = ⨅ i, f i

Tactic:
simp [inf'_eq_csInf_image, iInf]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
c : α
ha : a < c
hb : c < b
⊢ False

Tactic:
exact hab.2 ha hb

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ a ⩿ b ↔ a ⋖ b ∨ a = b

Tactic:
rw [le_antisymm_iff, wcovBy_iff_covBy_or_le_and_le]

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

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ iInf f = 0

Tactic:
by
  rw [iInf_of_isEmpty, sInf_empty]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | x ≠ b} ↔ a ≤ x ∧ x < b

Tactic:
by rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_and_ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
a b x : α
⊢ x ∈ h₀_finset_Ioc a b ↔ x ∈ h₁_finset_Ioc a b

Tactic:
rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → n ∉ bad := by
        by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g 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)
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
have := Fintype.ofFinite ι
  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) }
  suffices ∀ (s : Finset ι) (f : ℕ → ∀ i, α i),
    ∃ g : ℕ ↪o ℕ, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i, i ∈ s → r i ((f ∘ g) a i) ((f ∘ g) b i) by
    rw [wellQuasiOrdered_iff_exists_monotone_subseq]
    intro f
    simpa only [Finset.mem_univ, true_imp_iff] using! this Finset.univ f
  refine Finset.cons_induction ?_ ?_
  · intro f
    exists RelEmbedding.refl (· ≤ ·)
    simp only [IsEmpty.forall_iff, imp_true_iff, Finset.notMem_empty]
  · intro i s hi ih f
    obtain ⟨g, hg⟩ := (hr i).exists_monotone_subseq (f · i)
    obtain ⟨g', hg'⟩ := ih (f ∘ g)
    refine ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 ?_⟩
    exact ⟨hg _ _ (OrderHomClass.mono g' hab), hg' hab⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_1.inr.inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
a✝ : (f ∘ ⇑g) m ≠ (f ∘ ⇑g) n
hf : (f ∘ ⇑g) m ≤ (f ∘ ⇑g) n
h : n < m
⊢ False

Tactic:
exact h2 _ _ h (lt_of_le_not_ge hf (hc _ _ (g.strictMono h)))

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)

Tactic:
obtain ⟨m, n, hlt, hmn⟩ := hs g hgs

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
m n : ℕ
hlt : m < n
hmn : r (g m) (g n)
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Tactic:
by
  obtain (rfl | hs) := s.eq_empty_or_nonempty
  · simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self]
  exact ⟨fun h ↦ ⟨⟨h.toFinset.inf' ((Finite.toFinset_nonempty h).mpr hs) id,
    fun x hx ↦ Finset.inf'_le id ((Finite.mem_toFinset h).mpr hx)⟩,
    ⟨h.toFinset.sup' ((Finite.toFinset_nonempty h).mpr hs) id, fun x hx ↦ Finset.le_sup' id
    ((Finite.mem_toFinset h).mpr hx)⟩⟩,
    fun ⟨h₀, h₁⟩ ↦ BddBelow.finite_of_bddAbove h₀ h₁⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
⊢ ∃ m n, m < n ∧ (fun x1 x2 ↦ x1 ≤ x2) (f m) (f n)

Tactic:
· contrapose! hc
    refine ⟨Set.range (f ∘ g), ?_, ?_⟩
    · rintro _ ⟨m, rfl⟩ _ ⟨n, rfl⟩ _ hf
      obtain h | rfl | h := lt_trichotomy m n
      · exact hc _ _ (g.strictMono h) hf
      · contradiction
      · exact h2 _ _ h (lt_of_le_not_ge hf (hc _ _ (g.strictMono h)))
    · refine Set.infinite_range_of_injective fun m n (hf : f (g m) = f (g n)) ↦ ?_
      obtain h | rfl | h := lt_trichotomy m n <;>
        (first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl)

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

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : ↑a ∈ orbit ↥H ↑b
⊢ a ∈ orbit (↥H) b

Tactic:
· rcases h with ⟨g, h⟩
    dsimp at h
    rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h
    subst h
    exact MulAction.mem_orbit _ g

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

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
h : ↑a ∈ MulAction.orbit ↥H ↑b
⊢ a ∈ MulAction.orbit (↥H) b

pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
h : a ∈ MulAction.orbit (↥H) b
⊢ ↑a ∈ MulAction.orbit ↥H ↑b

Tactic:
· rcases h with ⟨g, h⟩
    dsimp at h
    rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h
    subst h
    exact MulAction.mem_orbit _ g

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
h : a ∈ MulAction.orbit (↥H) b
⊢ ↑a ∈ MulAction.orbit ↥H ↑b
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
⊢ ⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧

Tactic:
by
  simp_rw [← @Quotient.mk''_eq_mk, Quotient.eq'']
  exact orbitRel.Quotient.mem_subgroup_orbit_iff.symm

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 α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ a ∈ MulAction.orbit ↥H ⟦a⟧.out

Tactic:
← orbitRel_apply,

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
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ (orbitRel ↥H ↑x.orbit) a ⟦a⟧.out
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:
← smul_eq_mul,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ s • ↑(closure s) = ↑(closure s)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient (ker (Quot.mapRight h))
y : Quot ⇑r
w : α
⊢ (fun x ↦ x.liftOn' (fun w ↦ Quotient.mk'' (Quotient.mk'' w)) ⋯)
      ((fun x ↦ x.liftOn' (fun w ↦ Quotient.liftOn' w Quotient.mk'' ⋯) ⋯) (Quotient.mk'' (Quotient.mk'' w))) =
    Quotient.mk'' (Quotient.mk'' w)

Tactic:
by change ⟦_⟧ = _; rfl

Goal state after:
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient s
y : α
⊢ (fun x ↦ x.liftOn' (fun w ↦ Quotient.liftOn' w Quotient.mk'' ⋯) ⋯)
      ((fun x ↦ x.liftOn' (fun w ↦ Quotient.mk'' (Quotient.mk'' w)) ⋯) (Quotient.mk'' y)) =
    Quotient.mk'' y

Tactic:
by change ⟦_⟧ = _; rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Tactic:
by_cases a ∈ s

Goal state after:
case pos
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
h✝ : a ∈ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

case neg
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
h✝ : a ∉ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
x : c.Quotient
⊢ (c.lift (f.comp c.mk') ⋯) x = f x

Tactic:
rcases x with ⟨⟩

Goal state after:
case mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
x : c.Quotient
a✝ : M
⊢ (c.lift (f.comp c.mk') ⋯) (Quot.mk (⇑c.toSetoid) a✝) = f (Quot.mk (⇑c.toSetoid) a✝)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : IsReduced L₁
step : Red.Step L₁ L₂
⊢ False

Tactic:
induction step
  simp [IsReduced] at h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ {a} ⊆ s

Tactic:
intro _ H

Goal state after:
case refine_1
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
x✝ : ι
H : x✝ ∈ {a}
⊢ x✝ ∈ s
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ (lift N φ HN).ker = Subgroup.map (mk' N) φ.ker

Tactic:
← congrArg MonoidHom.ker (lift_comp_mk' N φ HN),

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ (lift N φ HN).ker = Subgroup.map (mk' N) ((lift N φ HN).comp (mk' N)).ker
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure ↑Finset.univ = ⊤

Tactic:
by rw [Finset.coe_univ]; exact Subgroup.closure_univ

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h₃ : ∀ (a : ι) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}
⊢ x ∉ s \ {x, g x hx} ∧ insert x (s \ {x, g x hx}) ⊆ s

Tactic:
simp [insert_subset_iff, hx]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : κ → M
⊢ ∏ j, ∏ _i, f j = ∏ i, f (g i)

Tactic:
← Finset.prod_fiberwise' _ g f

Goal state after:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : κ → M
⊢ ∏ j, ∏ _i, f j = ∏ j, ∏ i with g i = j, f j
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
z x y : FreeAbelianGroup T
hx : (lift fun x ↦ 1) x • of default = x
hy : (lift fun x ↦ 1) y • of default = y
⊢ (lift fun x ↦ 1) x • of default + (lift fun x ↦ 1) y • of default = x + y

Tactic:
hx,

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
z x y : FreeAbelianGroup T
hx : (lift fun x ↦ 1) x • of default = x
hy : (lift fun x ↦ 1) y • of default = y
⊢ x + (lift fun x ↦ 1) y • of default = x + y
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:

Tactic:
(t' : R) * (r₁ * r * r₂)
      = t' * r₁ * r * r₂ := by simp [← mul_assoc]
    _ = r₁' * t * r * r₂ := by rw [hr₁]
    _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
    _ = r₁' * (t * r') * r₂ := by rw [h]
    _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
    _ = t' * r₁ * r' * r₂ := by rw [hr₁]
    _ = t' * (r₁ * r' * r₂) := by simp [← mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
w v : P
⊢ w * (f.lift hg) z = v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v

Tactic:
lift_apply,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
w v : P
⊢ w * (g (f.sec z).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹) = v ↔
    g (f.sec z).1 * w = g ↑(f.sec z).2 * v
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ (f.lift hg) z * g ↑(f.sec z).2 = g (f.sec z).1

Tactic:
lift_apply,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ g (f.sec z).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹ * g ↑(f.sec z).2 = g (f.sec z).1
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x✝ : M
⊢ ((f.lift hg).comp f.toMonoidHom) x✝ = g x✝

Tactic:
exact f.lift_eq hg _

Goal state after: