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

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

Tactic:
ciSup_eq_ite

Goal state after:
case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this✝ : Nonempty ι
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i ↦ ⨆ (h : p i), f ⟨i, h⟩) i
⊢ BddAbove (range fun i ↦ if h : p i then f ⟨i, h⟩ else sSup ∅)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case empty
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Nonempty α
I : Set β
S : β → Set α
⊢ BddAbove (⋃ i ∈ ∅, S i) ↔ ∀ i ∈ ∅, BddAbove (S i)

Tactic:
simp only [biUnion_empty, bddAbove_empty, forall_mem_empty]

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

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

Tactic:
ciSup_eq_ite

Goal state after:
case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
i : ι
⊢ (if h : p i then f ⟨i, h⟩ else sSup ∅) ≤ iSup f
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i, ↑i ≤ sInf ∅

Tactic:
convert! h
    rw [← sInf_range, Subtype.range_coe]

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

Goal state before:
pp: case mp
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ⨅ i, f i = n → (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i

Tactic:
rintro rfl
    exact ⟨ciInf_mem f, ciInf_le (OrderBot.bddBelow ..)⟩

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

Goal state before:
pp: case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ x ∈
    if h : ⟨x.1, a⟩.fst = ⟨x.1, b⟩.fst then map (Embedding.sigmaMk ⟨x.1, b⟩.fst) (f (h ▸ ⟨x.1, a⟩.snd) ⟨x.1, b⟩.snd)
    else ∅

Tactic:
dif_pos rfl,

Goal state after:
case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ x ∈ map (Embedding.sigmaMk ⟨x.1, b⟩.fst) (f (⋯ ▸ ⟨x.1, a⟩.snd) ⟨x.1, b⟩.snd)
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
g : β → α
s : Finset α
hgf : LeftInvOn g f ↑s
ginj : InjOn g (g ⁻¹' ↑s)
⊢ image f s = s.preimage g ginj

Tactic:
simp only [SetLike.ext'_iff, coe_preimage, coe_image]
  rw [Set.image_eq_preimage_of_leftInvOn_injOn hgf ginj]

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)
i : ι
a : α i
b : β i
x : γ i
⊢ (⟨i, x⟩ ∈
      if h : ⟨i, a⟩.fst = ⟨i, b⟩.fst then map (Embedding.sigmaMk ⟨i, b⟩.fst) (f (h ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd) else ∅) ↔
    x ∈ f a b

Tactic:
dif_pos rfl,

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ ⟨i, x⟩ ∈ map (Embedding.sigmaMk ⟨i, b⟩.fst) (f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd) ↔ x ∈ f a b
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
x : α
inst✝ : LE α
⊢ Minimal (fun x ↦ True) x ↔ IsMin x

Tactic:
by
  simp [IsMin, Minimal]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
inst✝ : LE α
x : Subtype Q
⊢ Minimal (fun x ↦ P ↑x) x ↔ Minimal (P ⊓ Q) ↑x

Tactic:
by
  obtain ⟨x, hx⟩ := x
  simp only [Minimal, Subtype.forall, Subtype.mk_le_mk, Pi.inf_apply, inf_Prop_eq]
  tauto

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

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

Tactic:
suffices h₁ : n ≤ sInf {m | p (m - n)} by
    convert! sInf_add h₁
    simp_rw [Nat.add_sub_cancel_right]

Goal state after:
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ n ≤ sInf {m | p (m - n)}
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (range fun x ↦ f ↑x).WellFoundedOn r ↔ s.WellFoundedOn (r on f)

Tactic:
exact wellFoundedOn_range

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

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

Tactic:
simpa [← coe_subset] using Set.Ico_subset_Iio_self

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ioo a b) = Ioo ↑a ↑b

Tactic:
rw [subtype_Ioo_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Ioo] at hx
  exact hp hx.1.le hx.2.le a.prop b.prop

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c

Tactic:
rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
⊢ Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
refine ⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ ConjClasses.mk g ∈ (noncenter G)ᶜ

case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : ConjClasses.mk x = ConjClasses.mk y
⊢ x = y

case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : 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)
n : ℕ
x : α
hx : x ∈ if n < g 0 then f n else (f (g (n - g 0))).tail
⊢ x ∈ s

Tactic:
split_ifs at hx with hn
    exacts [hf1.1 _ _ hx, hf1.1 _ _ (List.tail_subset _ hx)]

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

Goal state before:
pp: case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ : N
⊢ Commute (e x) a✝

Tactic:
apply e.symm.injective

Goal state after:
case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
a✝ : N
⊢ e.symm (e x * a✝) = e.symm (a✝ * e x)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
b✝ c✝ : N
⊢ e x * (b✝ * c✝) = e x * b✝ * c✝

Tactic:
apply e.symm.injective

Goal state after:
case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
b✝ c✝ : N
⊢ e.symm (e x * (b✝ * c✝)) = e.symm (e x * b✝ * c✝)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ b✝ : N
⊢ a✝ * b✝ * e x = a✝ * (b✝ * e x)

Tactic:
apply e.symm.injective

Goal state after:
case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
a✝ b✝ : N
⊢ e.symm (a✝ * b✝ * e x) = e.symm (a✝ * (b✝ * e x))
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
⊢ z₁ * z₂ ∈ center M

Tactic:
by
  simp only [commute_iff_eq, mem_center_iff, isMulCentral_iff] at *
  grind

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {↑x}))ˣ
⊢ ConjAct.toConjAct ((Units.map (Submonoid.centralizer {↑x}).subtype) u) ∈ MulAction.stabilizer (ConjAct Mˣ) x

Tactic:
change _ • _ = _
      simp only [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, mul_inv_eq_iff_eq_mul]
      exact Units.ext <| (u.1.2 x <| Set.mem_singleton _).symm

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

Goal state before:
pp: case refine_2.refine_1
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {g}
⊢ h * g * h⁻¹ ∈ {g}

pp: case refine_2.refine_2
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {h * g * h⁻¹}
⊢ g ∈ {h * g * h⁻¹}

Tactic:
· exact (eq_mul_inv_of_mul_eq <| hh g rfl).symm

Goal state after:
case refine_2.refine_2
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {h * g * h⁻¹}
⊢ g ∈ {h * g * h⁻¹}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: 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) ⋯
h : x ∈ Submonoid.closure (s ∪ s⁻¹)
⊢ p x ⋯

Tactic:
induction h using Submonoid.closure_induction_left with

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

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * hd * tl.prod = hd * (a * tl.prod)

pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute

Tactic:
← mul_assoc

Goal state after:
case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * hd * tl.prod = hd * a * tl.prod

case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x

Tactic:
induction hx using closure_induction'' with

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ x ∈ ↑H * ↑N

Tactic:
induction hx using closure_induction'' with

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ (Commute on g) x y

Tactic:
by
        dsimp only [Function.onFun]
        rw [← h₂ _ hx, ← h₂ _ hy]
        subst h₁
        exact comm hx hy h

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ ∀ x ∈ Multiset.map f s.val, x = m

Tactic:
· simpa using h

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

Goal state before:
pp: α : Type u_1
s : Setoid α
a b : α
⊢ Quotient.mk' a = Quotient.mk' b ↔ ⊤ → s a b

Tactic:
Prop.top_eq_true,

Goal state after:
α : Type u_1
s : Setoid α
a b : α
⊢ Quotient.mk' a = Quotient.mk' b ↔ True → s a b
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mpr
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂

Tactic:
· rintro (⟨L, h, rfl⟩ | rfl)
    · exact Step.cons h
    · exact Step.cons_not

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

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

Tactic:
by
  calc
    ∏ x ∈ s, f x = ∏ x ∈ {a}, f x := by
      { refine (prod_subset ?_ ?_).symm
        · intro _ H
          rwa [mem_singleton.1 H]
        · simpa only [mem_singleton] }
    _ = f a := prod_singleton _ _

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

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

Tactic:
by
  rw [eq_div_iff_mul_eq', prod_erase_mul _ _ h]

Goal state after:
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:
by
  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.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
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * (↑u * ↑s') = r₃ * ↑u * ↑s'

Tactic:
← mul_assoc

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * ↑u * ↑s' = r₃ * ↑u * ↑s'
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_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ ↑s * ↑(t • r, ⟨t * ↑s, hst⟩).snd = ↑s * t * ↑(r, s).snd

Tactic:
← mul_assoc

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ ↑s * t * ↑s = ↑s * t * ↑(r, s).snd
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)
z : N
⊢ g (f.sec z).1 * (↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹ * (g.domRestrict S) (f.sec z).2) =
    g (f.sec z).1

Tactic:
IsUnit.liftRight_inv_mul,

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)
z : N
⊢ g (f.sec z).1 * 1 = g (f.sec z).1
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ ↑s₄' * (r₃' * ↑s₂') * ↑s = ↑s₄' * r₃' * ↑s₂' * ↑s

Tactic:
← mul_assoc

Goal state after:
case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ ↑s₄' * r₃' * ↑s₂' * ↑s = ↑s₄' * r₃' * ↑s₂' * ↑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
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
x : N
⊢ (k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x

Tactic:
by
  -- Porting note: need to specify `k` explicitly
  rw [← f.map_comp_map (k := k) hy j hl]
  simp only [MonoidHom.coe_comp, comp_apply]

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

Goal state before:
pp: case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑s₄' * ↑s₃' * (↑s₂' * r₂) * ↑s = ↑s₄' * ↑s₃' * ↑s₂' * r₂ * ↑s

Tactic:
← mul_assoc

Goal state after:
case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑s₄' * ↑s₃' * ↑s₂' * r₂ * ↑s = ↑s₄' * ↑s₃' * ↑s₂' * r₂ * ↑s
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ rc * (rb * ↑s₃) = rc * rb * ↑s₃

Tactic:
← mul_assoc

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ rc * rb * ↑s₃ = rc * rb * ↑s₃
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.mk' (x * ↑y) y = f x

Tactic:
← mul_mk'_one_eq_mk',

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 * ↑y) * f.mk' 1 y = f x
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
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * (↑(fS ⟨t * ↑s, ht⟩) * (↑(fS s)⁻¹ * f r))

Tactic:
← mul_assoc

Goal state after:
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)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * ↑(fS ⟨t * ↑s, ht⟩) * (↑(fS s)⁻¹ * f r)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤

Tactic:
simp [mul_eq_top_iff, *]

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

Goal state before:
pp: α : 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
x y : WithTop R
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
have : ∀ z, map f z = 0 ↔ z = 0 := fun z =>
        (Option.map_injective hf).eq_iff' f.toZeroHom.withTopMap.map_zero

Goal state after:
α : 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
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : 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
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
x : R
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
⊢ ↑(f x) ≠ 0

Tactic:
simpa [hf.eq_iff' (map_zero f)] using hx

Goal state after: