mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Commutator.Basic

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

Tactic:
y

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
⊢ y ∈ H₂ → ∀ h ∈ ↑H₃, ⁅h, ⁅x, y⁆⁆ = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥

Tactic:
Subgroup.commutator_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), ⁅⊤, centralizer ↑(commutator G)⁆⁆ = ⊥
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ N

Tactic:
apply hGN

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ _root_.commutator G
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 : GrothendieckGroup M
⊢ ↑((IsUnit.liftRight (f.domRestrict ⊤) ⋯) ((monoidOf ⊤).sec x).2) = f ↑((monoidOf ⊤).sec x).2

Tactic:
congr

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✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g : α →*o β
toFun✝¹ : α → β
map_one'✝¹ : toFun✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun x * { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun y
monotone'✝¹ : Monotone (↑{ toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun
toFun✝ : α → β
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_one' := map_one'✝ }.toFun x * { toFun := toFun✝, map_one' := map_one'✝ }.toFun y
monotone'✝ : Monotone (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidHom).toFun)
      { toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, monotone' := monotone'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun)
      { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ }
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, monotone' := monotone'✝¹ } =
    { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
g₁ g₂ : β →*o γ
f : α →*o β
hf : Surjective ⇑f
x✝ : g₁ = g₂
⊢ g₁.comp f = g₂.comp f

Tactic:
congr

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 β
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : RightInverse invFun✝¹ toFun✝¹
map_mul'✝¹ :
  ∀ (x y : α),
    { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun x *
        { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun y
map_le_map_iff'✝¹ :
  ∀ {a b : α},
    { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹,
              map_mul' := map_mul'✝¹ }.toFun
          a ≤
        { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹,
              map_mul' := map_mul'✝¹ }.toFun
          b ↔
      a ≤ b
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x * y) =
      { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x *
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
map_le_map_iff'✝ :
  ∀ {a b : α},
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝ }.toFun
          a ≤
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝,
              map_mul' := map_mul'✝ }.toFun
          b ↔
      a ≤ b
h₁ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
        map_le_map_iff' := map_le_map_iff'✝¹ }.toFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_le_map_iff' := map_le_map_iff'✝ }.toFun
h₂ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
        map_le_map_iff' := map_le_map_iff'✝¹ }.invFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_le_map_iff' := map_le_map_iff'✝ }.invFun
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹, map_mul' := map_mul'✝¹,
      map_le_map_iff' := map_le_map_iff'✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
      map_le_map_iff' := map_le_map_iff'✝ }

Tactic:
congr

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 : M
v : P
y : ↥S
⊢ (f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y * v

Tactic:
by
  rw [f.lift_mk' hg]; exact mul_inv_left hg _ _ _

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g : α ≃*o β
f₁ f₂ : β ≃*o γ
hg : Surjective ⇑g
x✝ : f₁ = f₂
⊢ g.trans f₁ = g.trans f₂

Tactic:
congr

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
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g : α →*₀o β
toFun✝¹ : α → β
map_zero'✝¹ : toFun✝¹ 0 = 0
map_one'✝¹ : { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun x * { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun y
monotone'✝¹ :
  Monotone (↑{ toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun x * { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun y
monotone'✝ :
  Monotone (↑{ toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidWithZeroHom).toFun)
      { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹,
        monotone' := monotone'✝¹ } =
    (fun f ↦ (↑f.toMonoidWithZeroHom).toFun)
      { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝,
        monotone' := monotone'✝ }
⊢ { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹,
      monotone' := monotone'✝¹ } =
    { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g₁ g₂ : β →*₀o γ
f : α →*₀o β
hf : Surjective ⇑f
x✝ : g₁ = g₂
⊢ g₁.comp f = g₂.comp f

Tactic:
congr

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

Goal state before:
pp: case 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 : M
⊢ ∀ (y : M), f x = f y ↔ g x = g y

Tactic:
y

Goal state after:
case 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
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

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

Tactic:
OreLocalization.oreDiv_smul_oreDiv

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ OreLocalization.oreNum (c • 1) b • a /ₒ (OreLocalization.oreDenom (c • 1) b * 1) = c • a /ₒ b
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 : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝¹ : M × ↥S
h✝¹ : z * f ↑w✝¹.2 = f w✝¹.1
w✝ : M × ↥S
h✝ : w * f ↑w✝.2 = f w✝.1
⊢ z = w

Tactic:
rw [← f.mk'_sec z, ← f.mk'_sec w]

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 : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝¹ : M × ↥S
h✝¹ : z * f ↑w✝¹.2 = f w✝¹.1
w✝ : M × ↥S
h✝ : w * f ↑w✝.2 = f w✝.1
⊢ f.mk' (f.sec z).1 (f.sec z).2 = f.mk' (f.sec w).1 (f.sec w).2
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) * j (l (g ↑(f.sec z).2)) = j (l ↑(k.sec ((f.map hy k) z)).2) * j (l (g (f.sec z).1))

Tactic:
← map_mul j,

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 * l (g ↑(f.sec z).2)) = j (l ↑(k.sec ((f.map hy k) z)).2) * j (l (g (f.sec z).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
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 * l (g ↑(f.sec z).2)) = j (l ↑(k.sec ((f.map hy k) z)).2) * j (l (g (f.sec z).1))

Tactic:
← map_mul j,

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 * l (g ↑(f.sec z).2)) = j (l ↑(k.sec ((f.map hy k) z)).2 * l (g (f.sec z).1))
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:
by
    cases x with | _ x s₂
    change OreLocalization.smul' r₁ s x s₂ = OreLocalization.smul' (r₂ * r₁) ⟨_, hs⟩ x s₂
    rcases oreCondition r₁ s₂ with ⟨r₁', s₁', h₁⟩
    rw [smul'_char _ _ _ _ _ _ h₁]
    rcases oreCondition (r₂ * r₁) s₂ with ⟨r₂', s₂', h₂⟩
    rw [smul'_char _ _ _ _ _ _ h₂]
    rcases oreCondition (s₂' * r₂) (s₁') with ⟨r₃', s₃', h₃⟩
    have : s₃' * r₂' * s₂ = r₃' * r₁' * s₂ := by
      rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, mul_assoc]
    rcases ore_right_cancel _ _ _ this with ⟨s₄', h₄⟩
    have : (s₄' * r₃') * (s₁' * s) ∈ S := by
      rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc, mul_assoc]
      exact mul_mem (s₄' * s₃' * s₂').2 hs
    rw [OreLocalization.expand' (r₂' • x) _ (s₄' * s₃'), OreLocalization.expand _ _ _ this]
    simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_smul, mul_assoc, h₄]
    congr 1
    ext; simp only [Submonoid.coe_mul, ← mul_assoc]
    rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc]

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.comp k.toMonoidHom) ↑(v, ⟨w, ⋯⟩).2 = (f.toMonoidHom.comp k.toMonoidHom) (v, ⟨w, ⋯⟩).1

Tactic:
simp_rw [MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, hv, 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.Algebra.Order.Hom.Ring

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

Tactic:
congr

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
toRingHom✝¹ : α →+* β
monotone'✝¹ : Monotone (↑↑toRingHom✝¹).toFun
toRingHom✝ : α →+* β
monotone'✝ : Monotone (↑↑toRingHom✝).toFun
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝¹, monotone' := monotone'✝¹ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, monotone' := monotone'✝ }
⊢ toRingHom✝¹ = toRingHom✝
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✝⁸ : Mul α
inst✝⁷ : Add α
inst✝⁶ : LE α
inst✝⁵ : Mul β
inst✝⁴ : Add β
inst✝³ : LE β
inst✝² : Mul γ
inst✝¹ : Add γ
inst✝ : LE γ
e : α ≃+*o β
⊢ ∀ {a b : β}, e.symm.toFun a ≤ e.symm.toFun b ↔ a ≤ b

Tactic:
by simp [← e.map_le_map_iff']

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝⁵ : Mul R
inst✝⁴ : Add R
inst✝³ : Mul S
inst✝² : Add S
inst✝¹ : Preorder R
inst✝ : Preorder S
e : R ≃+*o S
x : R
y : S
⊢ e.symm y < x ↔ y < e x

Tactic:
simpa using! e.toOrderIso.symm_apply_lt

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

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

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
a b : WithTop α
inst✝ : NoZeroDivisors α
⊢ NoZeroDivisors (WithTop α)

Tactic:
by
  refine ⟨fun h₁ => Decidable.byContradiction fun h₂ => ?_⟩
  rw [mul_def, if_neg h₂] at h₁
  rcases Option.mem_map₂_iff.1 h₁ with ⟨a, b, (rfl : _ = _), (rfl : _ = _), hab⟩
  exact h₂ ((eq_zero_or_eq_zero_of_mul_eq_zero hab).imp (congr_arg some) (congr_arg some))

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

Tactic:
numeratorHom_apply,

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = ↑(fS s)⁻¹ * φ (r /ₒ 1)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * φ (numeratorHom ↑s * (r /ₒ s)) = ↑(fS s)⁻¹ * φ (r /ₒ 1)

Tactic:
numeratorHom_apply,

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * φ (↑s /ₒ 1 * (r /ₒ s)) = ↑(fS s)⁻¹ * φ (r /ₒ 1)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₂ /ₒ s₂ * (r₁ /ₒ s₁)

Tactic:
rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
· rw [hb.succ_eq, or_iff_right_of_imp le_of_eq]

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s

Tactic:
simpa [Order.succ_eq_add_one] using monotoneOn_of_le_succ hs (f := f)

Goal state after:
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ (Function.invFun g ∘ f) a = b

Tactic:
Function.comp_apply,

Goal state after:
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ Function.invFun g (f a) = b
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
x✝ : ι
⊢ (↑s).piecewise f g x✝ = s.piecewise f g x✝

Tactic:
congr

Goal state after: