mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : LocallyFiniteOrder α
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    h₁

Tactic:
obtain ⟨h₁_finset_Icc, h₁_finset_Ico, h₁_finset_Ioc, h₁_finset_Ioo,
      h₁_finset_mem_Icc, h₁_finset_mem_Ico, h₁_finset_mem_Ioc, h₁_finset_mem_Ioo⟩ := h₁

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (Icc (f a) (f b)).preimage ⇑f ⋯ ↔ a ≤ x ∧ x ≤ b

Tactic:
by rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ = a ∨ a < a✝ ↔ a < a✝ ∨ a = a✝

Tactic:
or_comm,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ = a ∨ a < a✝ ↔ a = a✝ ∨ a < a✝
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • x • y = x • g • y

Tactic:
Submonoid.smul_def,

Goal state after:
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • ↑x • y = ↑x • g • y
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc b a

Tactic:
inf_eq_right.2 h,

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ Icc b (a ⊔ b) = Icc b a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s✝ : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : a ∉ s
hs : (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r
⊢ ((cons a s ha).sup f).WellFoundedOn r ↔ ∀ i ∈ cons a s ha, (f i).WellFoundedOn r

Tactic:
by simp [-sup_set_eq_biUnion, hs]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
s✝ : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : a ∉ s
hs : (s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r
⊢ ((cons a s ha).sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ cons a s ha, (f i).PartiallyWellOrderedOn r

Tactic:
by simp [-sup_set_eq_biUnion, hs]

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 : α
⊢ ∃ i, x ∈ i.orbit

Tactic:
exact ⟨Quotient.mk'' x, by simp⟩

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

Goal state before:
pp: M✝ : Type u_1
inst✝² : MulOneClass M✝
M : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
c : ↥(center M)
r : M
v : α
this : ∀ (g : M), g * ↑c = ↑c * g
⊢ c • r • v = r • c • v

Tactic:
Submonoid.smul_def,

Goal state after:
M✝ : Type u_1
inst✝² : MulOneClass M✝
M : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
c : ↥(center M)
r : M
v : α
this : ∀ (g : M), g * ↑c = ↑c * g
⊢ ↑c • r • v = r • ↑c • v
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
x : M
⊢ op x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M

Tactic:
simp_rw [Set.mem_center_iff, isMulCentral_iff, MulOpposite.forall, ← op_mul, op_inj]

Goal state after:
M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : M), Commute (op x) (op a)) ∧
      (∀ (a a_1 : M), a_1 * a * x = a_1 * (a * x)) ∧ ∀ (a a_1 : M), x * (a_1 * a) = x * a_1 * a) ↔
    (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ (↑l).noncommProd comm = l.prod

Tactic:
by
  rw [noncommProd]
  simp only [noncommFold_coe]
  induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.prod_cons, List.foldr, hl]
    intro x hx y hy
    exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)

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

Goal state before:
pp: case mul_left
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x✝ : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
x : G
hx : x ∈ s ∪ s⁻¹
y : G
hy : y ∈ Submonoid.closure (s ∪ s⁻¹)
ih : p y ⋯
⊢ p (x * y) ⋯

Tactic:
| mul_left x hx y hy ih =>

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
this : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x
⊢ a * (l.erase a).prod = l.prod

Tactic:
List.prod_erase_of_comm h this

Goal state after:
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
this : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x
⊢ l.prod = l.prod
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
l : List ι
⊢ ∑ x ∈ l.toFinset with p x, count x l = countP (fun b ↦ decide (p b)) l

Tactic:
simp [Finset.sum, sum_map_count_dedup_filter_eq_countP p l]

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
inst✝ : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
⊢ count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x)

Tactic:
by
  dsimp only [Finset.sum]
  rw [count_sum]

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

Goal state before:
pp: case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (g y)

pp: case hbc.hab
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)

pp: case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)

Tactic:
· exact (comm_gf hy hx h.symm).symm

Goal state after:
case hbc.hab
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)

case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)
Module: Mathlib.Data.Setoid.Basic

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

Tactic:
simp only [Pi.top_apply, Prop.top_eq_true, forall_true_left]

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

Goal state before:
pp: α : Type u_1
S : Set (Setoid α)
⊢ sSup S = EqvGen.setoid fun x y ↦ ∃ r ∈ S, r x y

Tactic:
by
  rw [eqvGen_eq]
  apply congr_arg sInf
  simp only [upperBounds, le_def, and_imp, exists_imp]
  ext
  exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩

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

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

Tactic:
coe_map_of_ker_le _ _ hf

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
⊢ ((Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) on f) ≤ ⇑r
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
h : (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ c.toSetoid x y

Tactic:
exact h c hS

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
c : Con M
p : c.Quotientˣ → Prop
u : c.Quotientˣ
H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }
⊢ p u

Tactic:
rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩
  exact H x y (c.eq.1 h₁) (c.eq.1 h₂)

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

Goal state before:
pp: β : Type v
inst✝ : Group β
s : Set β
⊢ Subgroup.closure s = (lift Subtype.val).range

Tactic:
FreeGroup.range_lift_eq_closure,

Goal state after:
β : Type v
inst✝ : Group β
s : Set β
⊢ Subgroup.closure s = Subgroup.closure (Set.range Subtype.val)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u_1
⊢ (lift of).range = ⊤

Tactic:
lift_of_eq_id

Goal state after:
α : Type u_1
⊢ (MonoidHom.id (FreeGroup α)).range = ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
n : ℕ
hn : N ≤ n
⊢ ∏ k ∈ range n, u k = ∏ k ∈ range N, u k

Tactic:
obtain ⟨m, rfl : n = N + m⟩ := Nat.exists_eq_add_of_le hn
  clear hn
  induction m with
  | zero => simp
  | succ m hm => simp [← add_assoc, prod_range_succ, hm, hu]

Goal state after:
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)
hP : ∀ (i : ι), (P i).FG
⊢ (Submonoid.pi Set.univ P).FG

Tactic:
have := Fintype.ofFinite ι
  choose s hs using hP
  refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩
  simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure ↑Finset.univ = ⊤

Tactic:
rw [Finset.coe_univ]; exact Submonoid.closure_univ

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
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.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ : R
s : ↥⊥
⊢ ↑s * x✝ = x✝ * ↑s

Tactic:
by
    rcases s with ⟨s, hs⟩
    rw [Submonoid.mem_bot] at hs
    simp [hs]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₂ ↦ of (1 * x₂)) x1 = x1
ih2 : (lift fun x₂ ↦ of (1 * x₂)) x2 = x2
⊢ (lift fun x₂ ↦ of (1 * x₂)) (x1 + x2) = x1 + x2

Tactic:
rw [map_add, ih1, ih2]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₁ ↦ of (x₁ * 1)) x1 = x1
ih2 : (lift fun x₁ ↦ of (x₁ * 1)) x2 = x2
⊢ (lift fun x₁ ↦ of (x₁ * 1)) (x1 + x2) = x1 + x2

Tactic:
rw [map_add, ih1, ih2]

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)
x y : M
h : f x = f y
⊢ g x = g y

Tactic:
by
  obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h
  rw [← one_mul (g x), ← IsUnit.liftRight_inv_mul (g.domRestrict S) hg c]
  change _ * g c * _ = _
  rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]

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

Tactic:
mul_inv_right hg,

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)
x y : N
⊢ g (f.sec (x * y)).1 * g ↑(f.sec y).2 =
    g ↑(f.sec (x * y)).2 * (g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹) * g (f.sec y).1
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

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

Tactic:
rw [f.lift_mk' hg]

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)
x : M
v : P
y : ↥S
⊢ g x * ↑((IsUnit.liftRight (g.domRestrict S) hg) y)⁻¹ = v ↔ g x = g ↑y * v
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : Group α
inst✝ : Preorder α
a b : (WithZero α)ˣ
⊢ WithZero.unitsWithZeroEquiv.toFun a ≤ WithZero.unitsWithZeroEquiv.toFun b ↔ a ≤ b

Tactic:
by simp [WithZero.unitsWithZeroEquiv]

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

Goal state before:
pp: case mp.mp
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
⊢ f x = f y → g x = g y

Tactic:
exact f.eq_of_eq hg

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

Tactic:
rw [← sec_spec, mul_inv_left, mul_comm]

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
⊢ f ↑(f.sec z).2 * z = f.toMonoidHom ↑(f.sec z).2 * z
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = ↑(fS sa) * (↑(fS s₁) * ↑(fS s₁)⁻¹ * f r₁ * (↑(fS s₂)⁻¹ * f r₂))

Tactic:
Units.mul_inv,

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = ↑(fS sa) * (1 * f r₁ * (↑(fS s₂)⁻¹ * f r₂))
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.coe
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hy : y ≠ 0
x : R
hx : ↑x ≠ 0
⊢ map (⇑f) (↑x * y) = map ⇑f ↑x * map (⇑f) y

Tactic:
| coe x =>

Goal state after:
case inr.inr.coe
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hy : y ≠ 0
x : R
hx : ↑x ≠ 0
⊢ map (⇑f) (↑x * y) = map ⇑f ↑x * map (⇑f) y
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) ≤ y (n + 1)

Tactic:
refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))
    · exact fun k hk => hx _ (hk.trans n.lt_succ_self)
    · exact fun k hk => hy _ (hk.trans n.lt_succ_self)

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ * ↑x < ↑a✝ * ↑x

Tactic:
bot_mul x0.ne.symm,

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ < ↑a✝ * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑a✝ * ↑x ≤ ⊥ * ↑x
⊢ ↑a✝ ≤ ⊥

Tactic:
bot_mul x0.ne.symm,

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑a✝ * ↑x ≤ ⊥
⊢ ↑a✝ ≤ ⊥
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case coe
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
x : α
⊢ IsSuccPrelimit ↑x ↔ ↑x = ⊤ ∨ ∃ y, ↑x = ↑y ∧ IsSuccPrelimit y

Tactic:
| coe x =>

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
x : α
⊢ IsSuccLimit ↑x ↔ ↑x = ⊤ ∨ ∃ y, ↑x = ↑y ∧ IsSuccLimit y

Tactic:
| coe x =>

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
x : α
⊢ IsPredPrelimit ↑x ↔ ↑x = ⊤ ∨ ∃ y, ↑x = ↑y ∧ IsPredLimit y

Tactic:
| coe x =>

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
by
  rw [← Ici_inter_Iio, Ici_succ_of_not_isMax ha, Ioi_inter_Iio]

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsSuccLimit b
⊢ (if h : IsMin b then isMin b h else isSuccLimit b ⋯) = isSuccLimit b hb

Tactic:
dif_neg hb.not_isMin

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsSuccLimit b
⊢ isSuccLimit b ⋯ = isSuccLimit b hb
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccPrelimit b
⊢ ⋯.fix
      (fun a IH ↦
        if h : IsSuccPrelimit a then isSuccPrelimit a h IH
        else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
      b =
    isSuccPrelimit b hb fun x x_1 ↦ prelimitRecOn x succ isSuccPrelimit

Tactic:
WellFounded.fix_eq,

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccPrelimit b
⊢ (if h : IsSuccPrelimit b then
      isSuccPrelimit b h fun y x ↦
        ⋯.fix
          (fun a IH ↦
            if h : IsSuccPrelimit a then isSuccPrelimit a h IH
            else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
          y
    else
      cast ⋯
        (succ (Classical.choose ⋯) ⋯
          ((fun y x ↦
              ⋯.fix
                (fun a IH ↦
                  if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                  else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
                y)
            (Classical.choose ⋯) ⋯))) =
    isSuccPrelimit b hb fun x x_1 ↦ prelimitRecOn x succ isSuccPrelimit