mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) l.sublists) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) l.sublists)

Tactic:
induction sublists l <;> simp [*]

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

Goal state before:
pp: case slnil
α : Type u
l₁ l₂ : List α
⊢ [].sublists' <+ [].sublists'

Tactic:
exact .refl _

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

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

Tactic:
sup_empty,

Goal state after:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ ⊥ = ∅.sup f ⊔ ∅.sup g
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ ⊥ = ∅.sup f ⊔ ∅.sup g

Tactic:
sup_empty,

Goal state after:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ ⊥ = ⊥ ⊔ ∅.sup g
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ ⊥ = ⊥ ⊔ ∅.sup g

Tactic:
sup_empty,

Goal state after:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ ⊥ = ⊥ ⊔ ⊥
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ (∅.sup fun b ↦ f b \ a) = ∅.sup f \ a

Tactic:
sup_empty,

Goal state after:
case empty
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ ⊥ = ∅.sup f \ a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ ⊥ = ∅.sup f \ a

Tactic:
sup_empty,

Goal state after:
case empty
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ ⊥ = ⊥ \ a
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #(insertNone s) = #s + 1

Tactic:
by simp [insertNone]

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

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
⊢ (∅.sup fun b ↦ a \ f b) = a \ ∅.inf f

Tactic:
sup_empty,

Goal state after:
case empty
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
⊢ ⊥ = a \ ∅.inf f
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

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

Tactic:
· intro H
    have := hs.ciInf_mem_image _ h
    simp only [mem_image] at this
    obtain ⟨_, hmem, hx⟩ := this
    rw [← hx]
    exact H _ hmem

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t : Finset ι
⊢ ⨆ x ∈ s ∪ t, f x = max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x)

Tactic:
suffices ∀ st : Finset ι, BddAbove <| .range fun x ↦ ⨆ (_ : x ∈ st), f x by
    simp [ciSup_or', ciSup_sup_eq, this]
  refine fun st ↦ ⟨st.sup f, fun a ⟨i, ha⟩ ↦ ha ▸ ?_⟩
  by_cases h : i ∈ st <;>
    simp [h, le_sup]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Multiset ι
f : ι → α
h : s ≠ 0
⊢ ∃ x ∈ s, sSup ∅ ≤ f x

Tactic:
by simpa using exists_mem_of_ne_zero h

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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
rw [ciSup_of_not_bddAbove hf, ciSup_of_not_bddAbove <| mt bbdAbove_range_left_of_sup hf]

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
⊢ sSup ∅ ≤ max (sSup ∅) (⨆ x, g x)
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (s.sigma t).sup f = s.sup fun i ↦ (t i).sup fun b ↦ f ⟨i, b⟩

Tactic:
by
  simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]
  exact
    ⟨fun i a hi ha => (le_sup hi).trans' <| le_sup (f := fun a => f ⟨i, a⟩) ha, fun i hi a ha =>
      le_sup <| mem_sigma.2 ⟨hi, ha⟩⟩

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [Icc, ← Finset.mem_def, Finset.mem_Icc]

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Finset.Ioc a b = ∅ ↔ ¬a < b

Tactic:
Finset.Ioc_eq_empty_iff

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ ¬a < b ↔ ¬a < b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: b : ℕ
⊢ #(Iic b) = b + 1

Tactic:
by rw [Iic_eq_Icc, card_Icc, Nat.bot_eq_zero, Nat.sub_zero]

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_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
a b : α
⊢ b ∈ h₀_finset_Ici a ↔ b ∈ h₁_finset_Ici a

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

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : 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
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))

Tactic:
refine ⟨n + n' - n - m, by lia, ?_⟩

Goal state after:
α : 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
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ r (f (n + m)) (f (n + n' - n - m + m))
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

Goal state after:
case 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
⊢ ∃ s, IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Infinite
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s)⁻¹ ≤ closure s⁻¹

Tactic:
rw [inv_le, closure_le, coe_inv, ← Set.inv_subset]
    exact subset_closure

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 α
g : G
x : Quotient G α
⊢ Set.MapsTo (fun x ↦ g • x) x.orbit x.orbit

Tactic:
rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']
  exact mapsTo_smul_orbit g x.out

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∈ center G
b : G
⊢ b * a * b⁻¹ ∈ center G

Tactic:
by simpa [mem_center_iff.mp ha b]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
⊢ (S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer

Tactic:
ext
  simp only [mem_prod, mem_centralizer_iff, Prod.forall, Prod.mul_def]
  grind [Set.Nonempty]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Mˣ
ha : ↑a ∈ center M
⊢ ↑a⁻¹ ∈ center M

Tactic:
rw [Semigroup.mem_center_iff] at *

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : Mˣ
ha : ∀ (g : M), g * ↑a = ↑a * g
⊢ ∀ (g : M), g * ↑a⁻¹ = ↑a⁻¹ * g
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Invertible a
ha : a ∈ center M
⊢ ⅟a ∈ center M

Tactic:
rw [Semigroup.mem_center_iff] at *

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Invertible a
ha : ∀ (g : M), g * a = a * g
⊢ ∀ (g : M), g * ⅟a = ⅟a * g
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
⊢ (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)

Tactic:
refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)

case refine_2
G : Type u_2
inst✝ : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
⊢ ∏ x ∈ s, f x = ∏ x ∈ t, g x

Tactic:
refine prod_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) h

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2
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 : ι
⊢ (insert i (univ.erase i)).noncommProd (fun j ↦ Pi.mulSingle j (x j) i) ⋯ = x i

Tactic:
rw [noncommProd_insert_of_notMem _ _ _ _ (notMem_erase _ _),
      noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one]
    · simp only [Pi.mulSingle_eq_same]
    · simpa using fun _ a ↦ Pi.mulSingle_eq_of_ne (a ·.symm) _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝ : β
⊢ (r.map f) i✝ i✝

Tactic:
exact .refl _

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

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

Tactic:
by rw [← toSetoid_bot, toSetoid_inj]

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

Goal state before:
pp: 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'
⊢ (fun hxy hyx ↦ f x y ⋯ ⋯) ≍ fun hxy hyx ↦ f x' y' ⋯ ⋯

Tactic:
refine Function.hfunext ?_ ?_

Goal state after:
case refine_1
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'
⊢ (↑x * ↑y = 1) = (↑x' * ↑y' = 1)

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' ⋯ ⋯
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'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ (fun hyx ↦ f x y ⋯ ⋯) ≍ fun hyx ↦ f x' y' ⋯ ⋯

Tactic:
refine Function.hfunext ?_ ?_

Goal state after:
case refine_2.refine_1
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'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ (↑y * ↑x = 1) = (↑y' * ↑x' = 1)

case refine_2.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'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1), a ≍ a' → f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), a * 1 = a

Tactic:
by rintro ⟨L⟩; simp [one_eq_mk]

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

Goal state before:
pp: case pos
ι : 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₁, one_mul]
    apply prod_eq_single_of_mem b h₂
    exact fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
⊢ FG M

Tactic:
cases nonempty_fintype M

Goal state after:
case intro
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
val✝ : Fintype M
⊢ FG M
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
⊢ f x = b

Tactic:
by_cases hc0 : #s = 0

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : #s = 0
⊢ f x = b

case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : ¬#s = 0
⊢ f x = b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f x = 1

Tactic:
rw [h]
      rw [h] at hx
      rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),
        prod_singleton] at hp
      exact hp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ (MulAut.conj g₁) g₂ = ⁅g₁, g₂⁆ * g₂

Tactic:
by
  simp [commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
    simp [mul_assoc]

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

Goal state before:
pp: case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inl G G') H₁, map (MonoidHom.inl G G') H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
apply commutator_mono <;>
          simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

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

Goal state before:
pp: case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inr G G') K₁, map (MonoidHom.inr G G') K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
apply commutator_mono <;>
          simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
⊢ liftExpand (P r₁ s₁) ⋯ = liftExpand (P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩) ⋯

Tactic:
ext x; cases x with | _ r₂ s₂
    rw [liftExpand_of, liftExpand_of, hP r₁ t₁ s₁ ht₁ r₂ 1 s₂ (by simp)]; simp

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ (c • 1) • a /ₒ (b * 1) = c • a /ₒ b

Tactic:
rw [smul_assoc, one_smul, mul_one]

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 g : S.LocalizationMap N
⊢ f.toMonoidHom = g.toMonoidHom → f = g

Tactic:
cases f

Goal state after:
case mk
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
g : S.LocalizationMap N
toMulHom✝ : M →ₙ* N
isLocalizationMap✝ : S.IsLocalizationMap toMulHom✝.toFun
⊢ { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ }.toMonoidHom = g.toMonoidHom →
    { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ } = g
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp.mpr
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)
H : Injective ⇑(f.lift hg)
x y : M
h : g x = g y
⊢ f x = f y

Tactic:
rw [← f.lift_eq hg, ← f.lift_eq hg] at h

Goal state after:
case mp.mpr
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)
H : Injective ⇑(f.lift hg)
x y : M
h : (f.lift hg) (f x) = (f.lift hg) (f y)
⊢ f x = f y
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f g : α →+*o β
h : (fun f ↦ (↑↑f.toRingHom).toFun) f = (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
g : α →+*o β
toRingHom✝ : α →+* β
monotone'✝ : Monotone (↑↑toRingHom✝).toFun
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, monotone' := monotone'✝ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ { toRingHom := toRingHom✝, monotone' := monotone'✝ } = g
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
⊢ 1 /ₒ 1 = 1

Tactic:
by with_unfolding_all rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
f : R ≃+* S
toEquiv✝ : R ≃ S
map_mul'✝ : ∀ (x y : R), toEquiv✝.toFun (x * y) = toEquiv✝.toFun x * toEquiv✝.toFun y
map_add'✝ : ∀ (x y : R), toEquiv✝.toFun (x + y) = toEquiv✝.toFun x + toEquiv✝.toFun y
h₁ : { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun = f.toFun
h₂ : { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }.invFun = f.invFun
⊢ { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ } = f

Tactic:
cases f

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
toEquiv✝¹ : R ≃ S
map_mul'✝¹ : ∀ (x y : R), toEquiv✝¹.toFun (x * y) = toEquiv✝¹.toFun x * toEquiv✝¹.toFun y
map_add'✝¹ : ∀ (x y : R), toEquiv✝¹.toFun (x + y) = toEquiv✝¹.toFun x + toEquiv✝¹.toFun y
toEquiv✝ : R ≃ S
map_mul'✝ : ∀ (x y : R), toEquiv✝.toFun (x * y) = toEquiv✝.toFun x * toEquiv✝.toFun y
map_add'✝ : ∀ (x y : R), toEquiv✝.toFun (x + y) = toEquiv✝.toFun x + toEquiv✝.toFun y
h₁ :
  { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toFun =
    { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun
h₂ :
  { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.invFun =
    { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }.invFun
⊢ { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
a b : WithTop α
inst✝ : NoZeroDivisors α
a✝ b✝ : WithTop α
h₁ : map₂ (fun x1 x2 ↦ x1 * x2) a✝ b✝ = 0
h₂ : ¬(a✝ = 0 ∨ b✝ = 0)
⊢ False

Tactic:
rcases Option.mem_map₂_iff.1 h₁ with ⟨a, b, (rfl : _ = _), (rfl : _ = _), hab⟩

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
a✝ b✝ : WithTop α
inst✝ : NoZeroDivisors α
a b : α
hab : a * b = 0
h₁ : map₂ (fun x1 x2 ↦ x1 * x2) (Option.some a) (Option.some b) = 0
h₂ : ¬(Option.some a = 0 ∨ Option.some b = 0)
⊢ False