mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Abelianization.Defs

Goal state before:
pp: case mk
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
x✝ : Abelianization H
a : H
⊢ (Abelianization.map e.toMonoidHom)
      ((Abelianization.map e.symm.toMonoidHom) (Quot.mk (⇑(QuotientGroup.leftRel (commutator H))) a)) =
    Quot.mk (⇑(QuotientGroup.leftRel (commutator H))) a

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
⊢ ∀ x ∈ ⊤, ∀ (y : M), x * y ∈ ⊤ → y ∈ ⊤

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ι → M
e : ι ≃ κ
⊢ (map e.toEmbedding s).prod (f ∘ ⇑e.symm) = s.prod f

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : κ → M
e : ι ≃ κ
⊢ s.prod (f ∘ ⇑e) = (map e.toEmbedding s).prod f

Tactic:
simp

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

Goal state before:
pp: case base
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 / f 0 = 1

Tactic:
simp

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

Goal state before:
pp: case step
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f (k + 1) / f 0 = f k / f 0 * (f (k + 1) / f k)

Tactic:
simp

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

Goal state before:
pp: case step
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f 0 / f (k + 1) = f 0 / f k * (f k / f (k + 1))

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
⊢ #s = ∑ x ∈ s, 1

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s : Finset ι
t : ι → Finset M
this : DecidableEq ι
⊢ #(∅.biUnion t) ≤ ∑ a ∈ ∅, #(t a)

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Injective e
f : ι → M
g : κ → M
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ Set.MapsTo e ↑univ ↑univ

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : ι → M
j : κ
⊢ ∀ (x : ι), x ∈ {i | g i = j} ↔ g x = j

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : κ → M
j : κ
⊢ ∀ (x : ι), x ∈ {i | g i = j} ↔ g x = j

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : Prop → M
⊢ ∏ p, f p = f True * f False

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
x✝ : [].Nodup
⊢ [].toFinset.prod f = (map f []).prod

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_4
α : Type u_5
inst✝ : CommMonoid M
m : Multiset ι
f : ι → α → M
⊢ (map (fun i ↦ ∏ a ∈ ∅, f i a) m).prod = ∏ a ∈ ∅, (map (fun i ↦ f i a) m).prod

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
⊢ Prod.mk <$> x <*> y = (fun b a ↦ (a, b)) <$> y <*> x

Tactic:
induction x using FreeAbelianGroup.induction_on' with

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
by
  rw [map_comp]
  rfl

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

Goal state before:
pp: case empty
M : Type u_4
inst✝ : CommMonoid M
⊢ IsUnit (Multiset.prod 0) ↔ ∀ a ∈ 0, IsUnit a

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : Fintype ι
inst✝ : CommMonoid M
f : ι → M
⊢ IsUnit (∏ a, f a) ↔ ∀ (a : ι), IsUnit (f a)

Tactic:
simp

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
x✝ : X × ↥S
⊢ 1 • x✝.fst = 1 • x✝.fst ∧ ↑1 * ↑x✝.snd = 1 * ↑x✝.snd

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : of s * y1 = y1 * of s
ih2 : of s * y2 = y2 * of s
⊢ of s * (y1 + y2) = (y1 + y2) * of s

Tactic:
rw [mul_add, add_mul, ih1, ih2]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
z : FreeAbelianGroup T
⊢ (fun n ↦ n • of default) ((lift fun x ↦ 1) (of default)) = of default →
    (fun n ↦ n • of default) ((lift fun x ↦ 1) (-of default)) = -of default

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
a : GrothendieckGroup M
⊢ a⁻¹ * a = 1

Tactic:
cases a using ind

Goal state after:
case H
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
y✝ : M × ↥⊤
⊢ (mk y✝.1 y✝.2)⁻¹ * mk y✝.1 y✝.2 = 1
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : M →* G
x✝ : M
⊢ ((fun f ↦ f.comp of) ((fun f ↦ (monoidOf ⊤).lift ⋯) f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : GrothendieckGroup M →* G
x✝ : Localization ⊤
⊢ ((fun f ↦ (monoidOf ⊤).lift ⋯) ((fun f ↦ f.comp of) f)) x✝ = f x✝

Tactic:
simp

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
s₁ : ↥S
r₂ : X
t₂ : R
s₂ : ↥S
ht₂ : t₂ * ↑s₂ ∈ S
⊢ 1 * ↑s₁ ∈ S

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : Mul γ
inst✝ : Mul δ
f g : α ≃*o β
⊢ ∀ {a b : α}, (MulEquiv.refl α).toFun a ≤ (MulEquiv.refl α).toFun b ↔ a ≤ b

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : Mul γ
inst✝ : Mul δ
f✝ g✝ f : α ≃*o β
g : β ≃*o γ
⊢ ∀ {a b : α}, ((↑f).trans ↑g).toFun a ≤ ((↑f).trans ↑g).toFun b ↔ a ≤ b

Tactic:
simp

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
r₂ : X
s₂ : ↥S
⊢ 1 * ↑s₂ ∈ S

Tactic:
simp

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

Goal state before:
pp: case c
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
r₂ : X
s₂ : ↥S
⊢ P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (1 • r₂) ⟨1 * ↑s₂, ⋯⟩ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ r₂ s₂

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x✝ : ↥S
⊢ ↑1 * (↑(↑x✝, x✝).2 * 1.1) = ↑1 * (↑1.2 * (↑x✝, x✝).1)

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)

Tactic:
by
  simp only [r_eq_r' S, r', Con.rel_mk]

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

Goal state before:
pp: case zero.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ 0 ≤ 0

Tactic:
simp

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

Goal state before:
pp: case 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 : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
⊢ ∃ a, (f.lift hg) a = v

Tactic:
obtain ⟨x, hx⟩ := H v

Goal state after:
case 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 : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
x : M × ↥S
hx : v * g ↑x.2 = g x.1
⊢ ∃ a, (f.lift hg) a = v
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case zero.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ 0 ≤ ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ ↑a✝ ≤ 0

Tactic:
simp

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

Goal state before:
pp: case coe.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝¹ a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝¹ ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
simp

Goal state after:
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
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : WithZero G ≃*o WithZero H
a b : G
⊢ (MulEquiv.withZero.symm ↑e).toFun a ≤ (MulEquiv.withZero.symm ↑e).toFun b ↔ a ≤ b

Tactic:
simp

Goal state after:
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
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : G ≃*o H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ }) x✝))
      a✝ =
    x✝ a✝

Tactic:
simp

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

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      0 =
    x✝ 0

Tactic:
simp

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

Goal state before:
pp: case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      ↑a✝ =
    x✝ ↑a✝

Tactic:
simp

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

Goal state before:
pp: case zero.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ 0 ≤ 0

Tactic:
simp

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

Goal state before:
pp: case zero.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ 0 ≤ ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ ↑a✝ ≤ 0

Tactic:
simp

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

Goal state before:
pp: case coe.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝¹ a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝¹ ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
simp

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
y : OreLocalization S R
x : OreLocalization S X
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
⊢ smul'' r₁ s x = smul'' (r₂ • r₁) ⟨r₂ * ↑s, hs⟩ x

Tactic:
cases x with | _ x s₂
     =>  _ 

Goal state after:
case c
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
⊢ smul'' r₁ s (x /ₒ s₂) = smul'' (r₂ • r₁) ⟨r₂ * ↑s, hs⟩ (x /ₒ 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 : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑z = f ↑y * 1

Tactic:
← mul_inv_left hf y (f z) 1,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑z * ↑((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = 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
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f x₁ * f x₂ = f x₁ * f x₂ * (f ↑y₁ * ↑⋯.unit⁻¹ * (f ↑y₂ * ↑⋯.unit⁻¹))

Tactic:
simp

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
r : R
hr : r ∈ S
⊢ ⟨r, hr⟩ • 1 = 1 • r

Tactic:
simp

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
r : R
hr : r ∈ S
⊢ ↑⟨r, hr⟩ * ↑1 = 1 * ↑⟨r, hr⟩

Tactic:
simp

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_2
inst✝ : MulAction R X
r : X
s : ↥S
⊢ ↑s * 1 = 1 * ↑s

Tactic:
simp

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
r : R
s : ↥S
⊢ ↑1 * r = r * ↑1

Tactic:
simp

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
k : S.LocalizationMap P
x : M
⊢ (f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k)) x = k x

Tactic:
simp

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
k : N ≃* P
x : N
⊢ (f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k)) x = k x

Tactic:
simp

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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * f.toMonoidHom (k w) = f.toMonoidHom x.1

Tactic:
hw

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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * f.toMonoidHom ↑x.2 = f.toMonoidHom x.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
f : S.LocalizationMap N
x : M
⊢ (mulEquivOfQuotient f) ((monoidOf S) x) = f x

Tactic:
simp

Goal state after:
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:
by
    cases f; cases g; congr
    exact DFunLike.coe_injective h

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
s s' : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
simp

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_2
inst✝ : MulAction R X
r : X
s t : ↥S
⊢ ↑s * 1 = 1 * ↑s

Tactic:
simp

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
r : R
s t : ↥S
⊢ ↑s * 1 = 1 * ↑s

Tactic:
simp

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_2
inst✝ : MulAction R X
r : X
s t : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
simp

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
r : R
s t : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
simp

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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s t : ↥S
⊢ ↑1 * (r₁ * ↑s) = r₁ * ↑s

Tactic:
simp

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
r₁ r₂ : R
s t : ↥S
⊢ ↑1 * (r₁ * ↑s) = r₁ * ↑s

Tactic:
simp

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_2
inst✝ : MulAction R X
p : R
r : X
s : ↥S
⊢ ↑1 * p = p * ↑1

Tactic:
simp

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
p r : R
s : ↥S
⊢ ↑1 * p = p * ↑1

Tactic:
simp

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
P : Type u_3
inst✝ : CommMonoid P
x✝ y✝ : M
⊢ (∃ c, ↑c * (↑(y✝, 1).2 * (x✝, 1).1) = ↑c * (↑(x✝, 1).2 * (y✝, 1).1)) ↔ ∃ c, ↑c * x✝ = ↑c * y✝

Tactic:
simp

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
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
⊢ ↑(fS 1)⁻¹ * f 1 = 1

Tactic:
simp

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

Goal state before:
pp: case mk.mk.zero
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
hn : 0 ≠ 0
hab : c * (↑b.2 ^ 0 * a.1 ^ 0) = c * (↑a.2 ^ 0 * b.1 ^ 0)
⊢ (fun a ↦ a ^ 0) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ 0) (c * (↑a.2 * b.1))

Tactic:
simp

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
x✝ : S
⊢ (e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom) x✝ = (NonUnitalRingHom.id S) x✝

Tactic:
simp

Goal state after: