mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
  refine fun hx ↦ closure_induction (by simp) (by simp) ?_ hx
  rintro x y _ _ ⟨i, hi⟩ ⟨j, hj⟩
  obtain ⟨k, hik, hjk⟩ := hS i j
  exact ⟨k, mul_mem (hik hi) (hjk hj)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LE β
x y : α × β
⊢ toLex y ≤ toLex x ↔ y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 ≤ x.2

Tactic:
by
  rw [eq_comm, toLex_le_toLex]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : M), (∃ i, a ∈ S i) → ∀ (b : M), (∃ i, b ∈ S i) → a * b = b * a

Tactic:
forall_exists_index

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : M) (x : ι), a ∈ S x → ∀ (b : M) (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
⊢ ∀ (x : Option α), ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) x = f x

Tactic:
rintro (_ | _) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)

Tactic:
obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ toLex (a₁, b₁) < toLex (a₁, b₂)

case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).1 < (a₂, b₂).1
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (n : N) (a : α), x' • n • a = n • x' • a
y : N
z : α
⊢ x • x' • y • z = y • x • x' • z

Tactic:
hx',

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (n : N) (a : α), x' • n • a = n • x' • a
y : N
z : α
⊢ x • y • x' • z = y • x • x' • z
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: ⊢ ofNat (ℕ × ℕ) = unpair

Tactic:
funext

Goal state after:
x✝ : ℕ
⊢ ofNat (ℕ × ℕ) x✝ = unpair x✝
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
⊢ (some z).getD d = y

Tactic:
have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩

Goal state after:
case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 ↦ x1 ≤ x2
⊢ (some z).getD d = y
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ l'.revzip = List.map (fun x ↦ (x, ↑l - x)) l'

Tactic:
have :
    Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) => p = (s, ↑l - s)) (revzip l')
      ((revzip l').map Prod.fst) := by
    rw [forall₂_map_right_iff, forall₂_same]
    rintro ⟨s, t⟩ h
    dsimp
    rw [← H h, add_tsub_cancel_left]
  rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]
  simpa using this

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

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
⊢ r i j

Tactic:
rcases hd m n with ⟨p, mp, np⟩

Goal state after:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
p : κ
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s a✝ : Finset α
⊢ a✝ ∈ powersetCard (#s) s ↔ a✝ ∈ {s}

Tactic:
rw [mem_powersetCard, mem_singleton]

Goal state after:
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s ↔ a✝ = s
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

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

Tactic:
simp only [hp, ciSup_unique]

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ ⨆ i, f ⟨i, ⋯⟩ = iSup f
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
rw [← iSup_univ (f := g), ← iSup_univ (f := fun i ↦ f (g i))]
  exact map_finite_biSup finite_univ f g

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

Goal state before:
pp: α : Type u
ι : Sort v
κ : ι → Sort w
inst✝¹ : Order.Frame α
inst✝ : Finite ι
f : (a : ι) → κ a → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
suffices ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : Π a, κ a → α),
      ⨅ a, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a, f a (g a) by
    simpa [← Equiv.plift.symm.iInf_comp, ← Equiv.plift.symm.iSup_comp,
        ← (Equiv.plift.piCongr fun a => @Equiv.plift (κ a.down)).symm.iSup_comp] using!
      this (κ := fun a => PLift (κ a.down)) fun (a : PLift ι) b => f a.down b.down
  intro ι κ _ f
  induction ι using Finite.induction_empty_option with
  | of_equiv e h => simp [← e.iInf_comp, ← e.piCongrLeft κ |>.iSup_comp, h]
  | h_empty => simp [iInf_of_empty, iSup_const]
  | h_option h =>
    simp only [iInf_option, h, ← (Equiv.piOptionEquivProd (β := κ)).symm.iSup_comp,
      Equiv.piOptionEquivProd_symm_apply, iSup_prod, ← inf_iSup_eq, ← iSup_inf_eq]

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

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

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)
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
· rw [iSup_of_empty', cbiSup_eq_of_forall_not fun i h ↦ isEmptyElim (⟨i, h⟩ : Subtype p)]

Goal state after:
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)
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case inl
α : Type u_5
inst✝ : CompleteLinearOrder α
a : α
hne : a ≠ ⊥
hfin : ∅.Finite
hmem : a ∉ ∅
⊢ sSup ∅ ≠ a

Tactic:
simp [eq_comm, hne]

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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

Tactic:
exact ((ciSup_pos hj).trans_le (le_ciSup bdd ⟨j, hj⟩)).trans gt.le

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
wf : WellFoundedLT α
a : α
h : ¬IsMax a
⊢ ∃ a', a ⋖ a'

Tactic:
rw [not_isMax_iff] at h

Goal state after:
α : Type u_1
inst✝ : Preorder α
wf : WellFoundedLT α
a : α
h : ∃ b, a < b
⊢ ∃ a', a ⋖ a'
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : x ∈ sigmaLift f a b
⊢ x ∈ sigmaLift g a b

Tactic:
rw [mem_sigmaLift] at hx ⊢

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
h : x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ x ∈ f '' {x | Minimal P x}

Tactic:
obtain ⟨y, hy, rfl⟩ := (mem_ofPred_eq ▸ h).prop

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
y : α
hy : P y
h : f y ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ f y ∈ f '' {x | Minimal P x}
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
ht : t ⊆ range ⇑f
⊢ Minimal (fun x ↦ x ∈ t) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Tactic:
← f.minimal_apply_mem_inter_range_iff,

Goal state after:
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
ht : t ⊆ range ⇑f
⊢ Minimal (fun x ↦ x ∈ t) (f x) ↔ Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x)
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iic b ↔ x ≤ b

Tactic:
Iic,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ (Finset.Iic b).val ↔ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ max a b + 1 - min a b = (↑b - ↑a).natAbs + 1

Tactic:
rw [← Int.natCast_inj, Int.ofNat_sub]

Goal state after:
a b : ℕ
⊢ ↑(max a b + 1) - ↑(min a b) = ↑((↑b - ↑a).natAbs + 1)

a b : ℕ
⊢ min a b ≤ max a b + 1
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ ↑a ∈ insertTop s ↔ a ∈ s

Tactic:
by
  simp [insertTop]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ⊤ ∈ insertTop s

Tactic:
by
  simp [insertTop]

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

Goal state before:
pp: n a : ℕ
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = range a

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
n : ℕ
⊢ image (fun x ↦ x % 0) (Ico n (n + 0)) = range 0

case inr
n a : ℕ
ha : a ≠ 0
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = range a
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
mn : m < m.succ + x
⊢ r (f (g m)) (f (g (m.succ + x)))

Tactic:
induction x with
    | zero => apply hr
    | succ x ih =>
      apply IsTrans.trans _ _ _ _ (hr _)
      exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))

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

Goal state before:
pp: case inr.mpr.inr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
· refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
    · lia
    · lia
    · rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

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

Goal state before:
pp: P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ P n

Tactic:
apply Nat.cauchy_induction h _ hs (k * ·) fun x hl hP => ⟨_, hm x hl hP⟩
  intro _ hl _
  convert! (Nat.mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk
  rw [one_mul]

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

Goal state before:
pp: P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ P n

Tactic:
by
  apply Nat.cauchy_induction h _ hs (k * ·) fun x hl hP => ⟨_, hm x hl hP⟩
  intro _ hl _
  convert! (Nat.mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk
  rw [one_mul]

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ico a b

Tactic:
by
  rw [← coe_subset, coe_Ioo, coe_Ico]
  exact Set.Ioo_subset_Ico_self

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Icc a b ⊆ Ici a

Tactic:
simpa [← coe_subset] using Set.Icc_subset_Ici_self

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
H K : Submonoid M
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
by rw [closure_eq, closure_eq]

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
not_lt

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ [[a, b]] = Icc b a

Tactic:
by
  rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]

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

Goal state before:
pp: case e'_2
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⟧
⊢ b ∈ orbit ⟦a⟧

Tactic:
orbitRel.Quotient.mem_orbit,

Goal state after:
case e'_2
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⟧
⊢ Quotient.mk'' b = ⟦a⟧
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ Set.univ = ⋃ x, x.orbit

Tactic:
ext x
  simp only [Set.mem_univ, Set.mem_iUnion, true_iff]
  exact ⟨Quotient.mk'' x, by simp⟩

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:
apply hf1.2 _ _ (g.lt_iff_lt.2 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
⊢ List.SublistForall₂ r (f (g (m - g 0))) (f (g n'))
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
by rw [closure_eq, closure_eq]

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

Goal state before:
pp: case inv_mem
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g g' : G
hg' : g' ∈ s
x : X
hx : x ∈ t
⊢ g'⁻¹ • x ∈ t

Tactic:
exact hst g'⁻¹ (hs g' hg') x hx

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

Goal state before:
pp: case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i * ?convert_8.m ^ #(univ.erase i) = x i

pp: case convert_8.m
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ M i

pp: case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = ?convert_8.m

Tactic:
one_pow,

Goal state after:
case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i * 1 = x i

case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∏ i, f i = ∏ i, g i

Tactic:
rw [← prod_subset s.toFinset.subset_univ (by simpa), prod_subtype (p := (· ∈ s)) _ (by simp)]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∏ a, f ↑a = ∏ i, g i

ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ Fintype { x // x ∈ s }
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ closure (⋃ x ∈ ↑Finset.univ, ↑(Finset.image (⇑(MonoidHom.mulSingle M x)) (s x))) = Submonoid.pi Set.univ P

Tactic:
Finset.coe_univ,

Goal state after:
ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ closure (⋃ x ∈ Set.univ, ↑(Finset.image (⇑(MonoidHom.mulSingle M x)) (s x))) = Submonoid.pi Set.univ P
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
h : (Submonoid.map e P).FG
⊢ P.FG

Tactic:
by
  obtain ⟨s, hs⟩ := h
  use s.preimage e he.injOn
  apply Submonoid.map_injective_of_injective he
  rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]
  congr
  rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs,
      MonoidHom.mrange_eq_map e]
  exact Submonoid.monotone_map le_top

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

Goal state before:
pp: case succ
M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
k : ℕ
hk : (∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1) → ∏ k ∈ range k, f k = s k
step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1
⊢ ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1

Tactic:
exact fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr.refine_2
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ Submonoid.closure ↑S ≤ (closure ↑S).toSubmonoid

Tactic:
Submonoid.closure_le

Goal state after:
case mpr.refine_2
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(closure ↑S).toSubmonoid
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ FG G ↔ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
by
  constructor
  · rw [fg_iff_exists_freeGroup_hom_surjective]
    intro ⟨S, hS, φ, hφ⟩
    obtain ⟨n, ⟨e⟩⟩ := hS.exists_equiv_fin S
    exact ⟨Fin n, inferInstance, φ.comp (FreeGroup.freeGroupCongr e).symm,
      hφ.comp (FreeGroup.freeGroupCongr e).symm.surjective⟩
  · intro ⟨α, _, φ, hφ⟩
    exact Group.fg_of_surjective hφ

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst✝¹ : G'.Normal
inst✝ : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
x : H ⧸ H'
⊢ (map G' H' ↑e ⋯) ((map H' G' ↑e.symm ⋯) x) = x

Tactic:
by
      rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le)
        (he ▸ G'.le_comap_map (e : G →* H))]
      simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
        MulEquiv.coe_monoidHom_refl, map_id_apply]

Goal state after:
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
ι : Type u_5
inst✝² : Finite ι
G : ι → Type u_6
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), Group.FG (G i)
⊢ ⊤.FG

Tactic:
by
    rw [← Subgroup.pi_top Set.univ]
    exact .pi fun i => Group.FG.out

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s.erase a, f a) * f a * b₂ = (f a * ∏ a ∈ s.erase a, f a) * b₂

Tactic:
mul_comm _ (f a)

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₂ = (f a * ∏ a ∈ s.erase a, f a) * b₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
G : Type u_3
s : Finset ι
a : ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
ha : a ∉ s
f : ι → G
⊢ (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x

Tactic:
by simp [ha]

Goal state after: