mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁ a₂ x✝ : WithBot α
h₁ : WithBot.recBotCoe True p ⊥
h₂ : WithBot.recBotCoe True p x✝
⊢ WithBot.recBotCoe True p (⊥ ⊔ x✝)

Tactic:
| =>

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁ a₂ x✝ : WithBot α
h₁ : WithBot.recBotCoe True p ⊥
h₂ : WithBot.recBotCoe True p x✝
⊢ WithBot.recBotCoe True p (⊥ ⊔ x✝)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁✝ a₂ : WithBot α
a₁ : α
h₁ : WithBot.recBotCoe True p ↑a₁
h₂ : WithBot.recBotCoe True p ⊥
⊢ WithBot.recBotCoe True p (↑a₁ ⊔ ⊥)

Tactic:
| =>

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁✝ a₂ : WithBot α
a₁ : α
h₁ : WithBot.recBotCoe True p ↑a₁
h₂ : WithBot.recBotCoe True p ⊥
⊢ WithBot.recBotCoe True p (↑a₁ ⊔ ⊥)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁✝ a₂✝ : WithBot α
a₁ a₂ : α
h₁ : WithBot.recBotCoe True p ↑a₁
h₂ : WithBot.recBotCoe True p ↑a₂
⊢ WithBot.recBotCoe True p (↑a₁ ⊔ ↑a₂)

Tactic:
| =>

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁✝ a₂✝ : WithBot α
a₁ a₂ : α
h₁ : WithBot.recBotCoe True p ↑a₁
h₂ : WithBot.recBotCoe True p ↑a₂
⊢ WithBot.recBotCoe True p (↑a₁ ⊔ ↑a₂)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
⊢ (⋃ i, ⋃ (h : i ∈ s), t i h).Finite

Tactic:
have := hs.to_subtype
  rw [biUnion_eq_iUnion]
  apply finite_iUnion fun i : s => ht i.1 i.2

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
⊢ ∀ (n : ℕ), f n ∈ s

Tactic:
rintro (_ | _) <;> exact (h _).choose_spec.1

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

Goal state before:
pp: n : ℕ
⊢ Icc 0 (n + 1 - 1) = Icc 0 n

Tactic:
Nat.add_sub_cancel_right

Goal state after:
n : ℕ
⊢ Icc 0 n = Icc 0 n
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)}
x✝ : ℕ
⊢ x✝ = x✝ + n - n

Tactic:
Nat.add_sub_cancel_right

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

Goal state before:
pp: case refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ p (m + n - n)

Tactic:
Nat.add_sub_cancel_right

Goal state after:
case refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ p m
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedGT α ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

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

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
h : WellFoundedGT α
a : ℕ →o α
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ WellFoundedGT α
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
a : (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x2 < x1
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬a.swap.toRelHom.toOrderHom n < a.swap.toRelHom.toOrderHom m
⊢ False

Tactic:
exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)

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

Goal state before:
pp: a b : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a)) (Ico 0 b)

Tactic:
convert! (Ico_union_Ico_eq_Ico a.zero_le (a.le_add_right b)).symm

Goal state after:
a b : ℕ
⊢ image (⇑(addLeftEmbedding a)) (Ico 0 b) = Ico a (a + b)
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:
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.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ #(Ioi a) = #(Ioi a) + 1 - 1

Tactic:
Nat.add_sub_cancel_right

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ #(Ioi a) = #(Ioi a)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ #(Iio a) = #(Iio a) + 1 - 1

Tactic:
Nat.add_sub_cancel_right

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ #(Iio a) = #(Iio a)
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 : α
a b : ↑(orbit G x)
⊢ a ∈ orbit (↥H) b ↔ ↑a ∈ orbit ↥H ↑b

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases h with ⟨g, rfl⟩
    exact MulAction.mem_orbit _ g
  · 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.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ ∃ k, ∀ (m : ℕ), k < m → f m ∉ s

Tactic:
by
  have := hs.bddAbove_preimage hf
  contrapose! this
  simpa [not_bddAbove_iff, and_comm]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case succ
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
ih : ↑(fs m) m = ↑(fs (m + k)) m
⊢ ↑(fs m) m = ↑(fs (m + (k + 1))) m

Tactic:
rw [ih, (minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
        (Nat.lt_succ_iff.2 (Nat.add_le_add_left k.zero_le m))]
      rfl

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

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ ∈ carrier (Quot.mk (⇑(IsConj.setoid G)) g)

Tactic:
mem_carrier_iff_mk_eq

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ ConjClasses.mk (h * g * h⁻¹) = Quot.mk (⇑(IsConj.setoid G)) g
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'
hmn : List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail) (f (g (n' + g 0 - g 0))).tail
hn : ¬g 0 + n' < g 0
⊢ False

Tactic:
Nat.add_sub_cancel_right

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'
hmn : List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail) (f (g n')).tail
hn : ¬g 0 + n' < g 0
⊢ False
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 ι
e : ι ↪ κ
⊢ (map e s).prod = fun f ↦ ∏ x ∈ s, f (e x)

Tactic:
funext f

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
e : ι ↪ κ
f : κ → M
⊢ (map e s).prod f = ∏ x ∈ s, f (e x)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

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

Tactic:
g

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

Goal state before:
pp: case cons
α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∉ s
IH : s.noncommProd f ⋯ = s.prod f
⊢ (cons a s ha).noncommProd f ⋯ = (cons a s ha).prod f

Tactic:
| cons a s ha IH =>

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
⊢ (∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x) → x ∈ closure s

Tactic:
by
    rintro ⟨n, t, hts, -, rfl⟩; exact prod_mem _ fun x hx ↦ pow_mem (subset_closure <| hts hx) _

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

Goal state before:
pp: α : Type u
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
by injections; subst_vars; simp

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

Goal state before:
pp: α : Type u
x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [(x3, b3)] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = [(x3, b3)] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([(x3, b3)] ++ x✝⁴) L₅

Tactic:
by injections; subst_vars; simp

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
h : a ∉ s
⊢ (cons a s h).prod = fun f ↦ f a * ∏ x ∈ s, f x

Tactic:
funext f

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝ : CommMonoid M
h : a ∉ s
f : ι → M
⊢ (cons a s h).prod f = f a * ∏ x ∈ s, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
h : a ∉ s
⊢ (insert a s).prod = fun f ↦ f a * ∏ x ∈ s, f x

Tactic:
funext f

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
h : a ∉ s
f : ι → M
⊢ (insert a s).prod f = f a * ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [(x3, b3)] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [(x3, b3)] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([(x3, b3)] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
by injections; subst_vars; simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
a : ι
⊢ {a}.prod = fun f ↦ f a

Tactic:
funext f

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
a : ι
f : ι → M
⊢ {a}.prod f = f a
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
d : Con c.Quotient
x y : c.Quotient
⊢ ((fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯) ((fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩) d)) x y ↔ d x y

Tactic:
by
      refine ⟨?_, Con.induction_on₂ x y fun w z h => ⟨w, z, h, rfl, rfl⟩⟩
      rintro ⟨a, b, H, rfl, rfl⟩
      exact H

Goal state after:
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:
by
  induction step
  simp [IsReduced] at h

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ ⦃a b : List (α × Bool)⦄, Red.Step a b → Red.Step (invRev a) (invRev b)

Tactic:
intro a b h

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
h : Red.Step a b
⊢ Red.Step (invRev a) (invRev b)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case of
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : α
⊢ (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) (of x)) = of x

Tactic:
simp [Unique.default_eq x]

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

Goal state before:
pp: case inv_of
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : α
hx : (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) (of x)) = of x
⊢ (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) (of x)⁻¹) = (of x)⁻¹

Tactic:
simp [Unique.default_eq x]

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

Goal state before:
pp: case of
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : α
⊢ (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) (FreeAddGroup.of x)) =
    FreeAddGroup.of x

Tactic:
simp [Unique.default_eq x]

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

Goal state before:
pp: case neg_of
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : α
hx :
  (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) (FreeAddGroup.of x)) =
    FreeAddGroup.of x
⊢ (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) (-FreeAddGroup.of x)) =
    -FreeAddGroup.of x

Tactic:
simp [Unique.default_eq x]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
ι : Sort u_3
inst✝ : Finite ι
P : ι → Submonoid M
hP : ∀ (i : ι), (P i).FG
⊢ (_root_.iSup P).FG

Tactic:
simpa [iSup_plift_down] using biSup Set.finite_univ (P ∘ PLift.down) fun i _ => hP i.down

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Monoid M
S : Set M
hS : S.Finite
φ : FreeMonoid ↑S →* M
hφ : Function.Surjective ⇑φ
⊢ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
obtain ⟨n, ⟨e⟩⟩ := hS.exists_equiv_fin S

Goal state after:
case mp
M : Type u_1
inst✝ : Monoid M
S : Set M
hS : S.Finite
φ : FreeMonoid ↑S →* M
hφ : Function.Surjective ⇑φ
n : ℕ
e : ↑S ≃ Fin n
⊢ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
ι : Sort u_5
inst✝ : Finite ι
P : ι → Subgroup G
hP : ∀ (i : ι), (P i).FG
⊢ (_root_.iSup P).FG

Tactic:
simpa [iSup_plift_down] using biSup Set.finite_univ (P ∘ PLift.down) fun i _ => hP i.down

Goal state after:
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 ⇑φ
⊢ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
obtain ⟨n, ⟨e⟩⟩ := hS.exists_equiv_fin S

Goal state after:
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 ⇑φ
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
R : Setoid ι
inst✝ : DecidableRel ⇑R
⊢ ∏ x ∈ s, f x = ∏ xbar ∈ image (Quotient.mk R) s, ∏ y ∈ s with ⟦y⟧ = xbar, f y

Tactic:
by
  refine (Finset.prod_image' f fun x _hx => ?_).symm
  rfl

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
F : FreeAbelianGroup α →+* R
⊢ ↑{ toFun := ⇑(lift ⇑((↑F).comp ofMulHom)), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } = ↑F

Tactic:
rw [← lift.apply_symm_apply (↑F : FreeAbelianGroup α →+ R)]

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
F : FreeAbelianGroup α →+* R
⊢ ↑{ toFun := ⇑(lift ⇑((↑F).comp ofMulHom)), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } =
    lift (lift.symm ↑F)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ of s * of t = of t * of s

Tactic:
dsimp only [(· * ·), Mul.mul]

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (Mul.mul x₁ x₂)) (of s)) (of t) =
    (lift fun x₂ ↦ (lift fun x₁ ↦ of (Mul.mul x₁ x₂)) (of t)) (of s)
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:
mul_inv_left,

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 * 1
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
P : Type u_3
inst✝ : CommMonoid P
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d
x : Localization S
y z : M × ↥S
h : (OreLocalization.oreEqv S M) y z
⊢ ⋯ ▸ f y.1 y.2 = f z.1 z.2

Tactic:
cases y; cases z; exact H (r_iff_oreEqv_r.mpr h)

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ (r S) (1, 1) (↑a, a)

Tactic:
exact one_rel a

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ j (l (k.sec ((f.map hy k) z)).1) *
      ↑((IsUnit.liftRight ((j.toMonoidHom.comp l).domRestrict T) ⋯) (k.sec ((f.map hy k) z)).2)⁻¹ =
    j (l (g (f.sec z).1)) * ↑((IsUnit.liftRight ((j.toMonoidHom.comp (l.comp g)).domRestrict S) ⋯) (f.sec z).2)⁻¹

Tactic:
mul_inv_left,

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ j (l (k.sec ((f.map hy k) z)).1) =
    (j.toMonoidHom.comp l) ↑(k.sec ((f.map hy k) z)).2 *
      (j (l (g (f.sec z).1)) * ↑((IsUnit.liftRight ((j.toMonoidHom.comp (l.comp g)).domRestrict S) ⋯) (f.sec z).2)⁻¹)
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 : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
w z : N
⊢ w * ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z ↔ w = f ↑y * z

Tactic:
rw [mul_comm]
  exact Units.inv_mul_eq_iff_eq_mul (IsUnit.liftRight (f.domRestrict S) h y)

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
z : N
⊢ z * f ↑(f.sec z).2 * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) (f.sec z).2)⁻¹ = z

Tactic:
mul_inv_left,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z : N
⊢ z * f ↑(f.sec z).2 = f.toMonoidHom ↑(f.sec z).2 * z
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
⊢ f x * f ↑y * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y)⁻¹ = f x

Tactic:
mul_inv_left,

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
⊢ f x * f ↑y = f.toMonoidHom ↑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
y : ↥S
⊢ f ↑y * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y)⁻¹ = 1

Tactic:
mul_inv_left,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
y : ↥S
⊢ f ↑y = f.toMonoidHom ↑y * 1
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x : R
⊢ -f x = 1 ↔ -x = 1

Tactic:
← map_neg,

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x : R
⊢ f (-x) = 1 ↔ -x = 1
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
c : WithTop α
b : α
hbc : ↑b < ⊤
⊢ (fun x ↦ ↑a * x) ↑b < (fun x ↦ ↑a * x) ⊤

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
c : WithTop α
b : α
hbc : ↑b < ⊤
⊢ (fun x ↦ ↑a * x) ↑b < (fun x ↦ ↑a * x) ⊤