mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case h₁
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun i ↦ f ⟨i, ⋯⟩) ⊆ range f

Tactic:
rintro - ⟨i, rfl⟩

Goal state after:
case h₁
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : ι
⊢ (fun i ↦ f ⟨i, ⋯⟩) i ∈ range f
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case h₂
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ range f ⊆ range fun i ↦ f ⟨i, ⋯⟩

Tactic:
rintro - ⟨i, rfl⟩

Goal state after:
case h₂
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : Subtype p
⊢ f i ∈ range fun i ↦ f ⟨i, ⋯⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i < a → ∀ x ∈ s, f x < a

Tactic:
intro h x hx
    refine h.trans_le' (le_csSup ?_ ?_)
    · classical
      refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove
      intro
      simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind
    · simp only [mem_range]
      refine ⟨x, ?_⟩
      simp [hx]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: case refine_1
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i ≤ ⨆ t, ⨆ i ∈ t, s i

pp: case refine_2
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ t, ⨆ i ∈ t, s i ≤ ⨆ i, s i

Tactic:
· exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl

Goal state after:
case refine_2
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ t, ⨆ i ∈ t, s i ≤ ⨆ i, s i
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b

Tactic:
by
  refine ⟨fun h2 => h.eq_or_eq h2.1 h2.2, ?_⟩; rintro (rfl | rfl)
  exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) ≠ ∅ ↔ ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅

case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ ≠ ∅ ↔ ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) = ∅ ↔
    ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ #(if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) =
    if h : a.fst = b.fst then #(f (h ▸ a.snd) b.snd) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ #(map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd)) = #(f (h ▸ a.snd) b.snd)

case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ #∅ = 0
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ∈ Ici (sInf s) ∧ k ∉ Ici (sInf s)

pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = ?m.40 + 1

Tactic:
H,

Goal state after:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ∈ Ici (k + 1) ∧ k ∉ Ici (k + 1)

s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = ?m.40 + 1
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
h : c ≤ a
⊢ image (fun x ↦ x - c) (Ico a b) = Ico (a - c) (b - c)

Tactic:
by
  ext x
  simp_rw [mem_image, mem_Ico]
  refine ⟨?_, fun h ↦ ⟨x + c, by lia⟩⟩
  rintro ⟨x, hx, rfl⟩
  lia

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

Goal state before:
pp: n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}

Tactic:
convert! sInf_add h₁

Goal state after:
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
x✝ : ℕ
⊢ x✝ = x✝ + n - n
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
⊢ Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r r)

Tactic:
exact ⟨f⟩

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
⊢ ¬WellFounded r

Tactic:
rw [wellFounded_iff_isEmpty, not_isEmpty_iff]
  exact ⟨f⟩

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.Infinite
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
Set.Infinite,

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
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.WellFoundedOn r ↔ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
have f : RelEmbedding (Subrel r (· ∈ s)) fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s :=
    ⟨⟨(↑), Subtype.coe_injective⟩, by simp⟩

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
⊢ s.WellFoundedOn r ↔ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ WellQuasiOrdered r ↔ WellQuasiOrdered s

Tactic:
apply (Equiv.arrowCongr (.refl ℕ) f).forall_congr
  congr! with g a b
  simp [f.map_rel_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Preorder α
p : α → Prop
inst✝⁵ : DecidablePred p
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : Preorder M
inst✝³ : Preorder N
inst✝² : EquivLike F M N
inst✝¹ : OrderIsoClass F M N
f : F
inst✝ : LocallyFiniteOrder N
⊢ ∀ (a b x : M), x ∈ map { toFun := EquivLike.inv f, inj' := ⋯ } (finsetIcc (f a) (f b)) ↔ a ≤ x ∧ x ≤ b

Tactic:
simp [finset_mem_Icc, EquivLike.inv_apply_eq]

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 α
x y : Quotient G α
h : x.orbit = y.orbit
⊢ x = y

Tactic:
orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq',

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : MulAction.orbit G (Quotient.out x) = MulAction.orbit G (Quotient.out y)
⊢ x = y
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : M
⊢ 1 * (x✝¹ * x✝) = 1 * x✝¹ * x✝

Tactic:
rw [one_mul, one_mul]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : True ∧ map (↑(MulAut.conj g)) K = K
⊢ H ⊔ map (↑(MulAut.conj g)) K = H ⊔ K

Tactic:
hg.2

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
⊢ ∑ a ∈ s, {a} = s.val

Tactic:
simp only [sum_eq_multiset_sum, Multiset.sum_map_singleton]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
⊢ (∏ x ∈ s, if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
h : p
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x

case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
h : ¬p
⊢ ∏ x ∈ s, g x = ∏ x ∈ s, g x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
⊢ (∏ x ∈ s, if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : p
⊢ ∏ x ∈ s, f h x = ∏ x ∈ s, f h x

case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : ¬p
⊢ ∏ x ∈ s, g h x = ∏ x ∈ s, g h x
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Setoid α
⊢ s = ⊤ ↔ ∀ (x y : α), s x y

Tactic:
_root_.eq_top_iff,

Goal state after:
α : Type u_1
s : Setoid α
⊢ ⊤ ≤ s ↔ ∀ (x y : α), s x y
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ Quotient.lift f H ⟦x⟧ = g ⟦x⟧

Tactic:
Quotient.lift_mk f H,

Goal state after:
case mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ f x = g ⟦x⟧
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : r x y
⊢ s (Quotient.mk' x) (Quotient.mk' y)

Tactic:
Quotient.eq'.2 h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : r x y
⊢ s (Quotient.mk' y) (Quotient.mk' y)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ d : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
w x y z : M
h1 : (Setoid.comap f c.toSetoid) w x
h2 : (Setoid.comap f c.toSetoid) y z
⊢ c (f (w * y)) (f (x * z))

Tactic:
H,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ d : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
w x y z : M
h1 : (Setoid.comap f c.toSetoid) w x
h2 : (Setoid.comap f c.toSetoid) y z
⊢ c (f w * f y) (f (x * z))
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
a b : M
h1 : c.toSetoid a b
p q : M
h2 : c.toSetoid p q
⊢ (c.mapOfSurjective (⇑f) h hf) (f a * f p) (f b * f q)

Tactic:
exact ⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩

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

Goal state before:
pp: case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)

Tactic:
rw [nil_append, nil_append, cons.sizeOf_spec, cons.sizeOf_spec]
      lia

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

Goal state before:
pp: α : Type u
x : FreeGroup α
⊢ (map _root_.id) x = x

Tactic:
rcases x with ⟨L⟩

Goal state after:
case mk
α : Type u
x : FreeGroup α
L : List (α × Bool)
⊢ (map _root_.id) (Quot.mk Red.Step L) = Quot.mk Red.Step L
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
⊢ (map g) ((map f) x) = (map (g ∘ f)) x

Tactic:
rcases x with ⟨L⟩

Goal state after:
case mk
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
L : List (α × Bool)
⊢ (map g) ((map f) (Quot.mk Red.Step L)) = (map (g ∘ f)) (Quot.mk Red.Step L)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case h
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.LeftInverse ⇑(map (Function.invFun f)) ⇑(map f)

Tactic:
simp [Function.LeftInverse, map.comp, Function.invFun_comp hf]

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [ha h₁, hb h₂, mul_one]
    exact
      _root_.trans
        (prod_congr rfl fun c hc =>
          h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, ne_of_mem_of_not_mem hc h₂⟩)
        prod_const_one

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : g b ≠ 1
H : g b = 1
⊢ False

Tactic:
rw [H] at h₂; simp at h₂

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : Monoid M
⊢ (∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ) → FG M

Tactic:
intro ⟨α, _, φ, hφ⟩

Goal state after:
case mpr
M : Type u_1
inst✝ : Monoid M
α : Type
w✝ : Finite α
φ : FreeMonoid α →* M
hφ : Function.Surjective ⇑φ
⊢ FG M
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 →* H
hφ : Surjective ⇑φ
HN : N = φ.ker
⊢ Injective ⇑(lift N φ ⋯)

Tactic:
by rw [← MonoidHom.ker_eq_bot_iff, ker_lift, ← HN, QuotientGroup.map_mk'_self]

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

Goal state before:
pp: case H
ι : 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 ∈ s, f x = 1

Tactic:
| H s ih =>

Goal state after:
case H
ι : 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 ∈ s, f x = 1
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
G : Type u_3
inst✝ : Group G
S : Set G
hS : S.Finite
φ : FreeGroup ↑S →* G
hφ : Function.Surjective ⇑φ
n : ℕ
e : ↑S ≃ Fin n
⊢ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
exact ⟨Fin n, inferInstance, φ.comp (FreeGroup.freeGroupCongr e).symm,
      hφ.comp (FreeGroup.freeGroupCongr e).symm.surjective⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
intro ⟨α, _, φ, hφ⟩

Goal state after:
case mpr
G : Type u_3
inst✝ : Group G
α : Type
w✝ : Finite α
φ : FreeGroup α →* G
hφ : Function.Surjective ⇑φ
⊢ FG G
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n✝ n : ℕ
a✝ : n < n✝
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)

Goal state after:
M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n✝ n : ℕ
a✝ : n < n✝
h₁ : f n ≤ f (n + 1)
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅p, q⁆ ∈ ⊥ ↔ q * p = p * q

Tactic:
mem_bot,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅p, q⁆ = 1 ↔ q * p = p * q
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer ↑H₂

Tactic:
rw [eq_bot_iff, commutator_le]
  refine forall_congr' fun p =>
    forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => ?_
  rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Function.Surjective ⇑(QuotientGroup.mk' N)

Tactic:
exact QuotientGroup.mk'_surjective N

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)
⊢ g (f.sec 1).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec 1).2)⁻¹ = 1

Tactic:
rw [mul_inv_left, mul_one]

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)
⊢ g (f.sec 1).1 = g ↑(f.sec 1).2
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
⊢ StrictMono ⇑f ↔ ∀ (a : α), 0 < a → 0 < f a

Tactic:
refine ⟨fun h a => ?_, fun h a b hl => ?_⟩

Goal state after:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : StrictMono ⇑f
a : α
⊢ 0 < a → 0 < f a

case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 < a → 0 < f a
a b : α
hl : a < b
⊢ f a < f b
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by rw [← comp_apply, h, comp_apply]

Goal state after:
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀o γ
f₁ f₂ : α →*₀o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by rw [← comp_apply, h, comp_apply]

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

Goal state before:
pp: case h.right
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := ⋯
u₀ : ↥S := ⋯
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ ↑s₄ * ↑s₃ * (↑u₀ * ↑s₁) = ↑s₄ * r₃ * (↑u * ↑s₁)

Tactic:
rw [← mul_assoc (b := (u₀ : R)), mul_assoc (c := (u₀ : R)), h₃]
    simp only [mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
z : N
H : z = f.mk' x y
⊢ z * f ↑y = f x

Tactic:
H,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
z : N
H : z = f.mk' x y
⊢ f.mk' x y * f ↑y = f x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a : M
b c : ↥S
⊢ a * (↑b * ↑c) = a * ↑c * ↑b

Tactic:
mul_comm (b : M),

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a : M
b c : ↥S
⊢ a * (↑c * ↑b) = a * ↑c * ↑b