mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case refine_2.inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ update f i x j ∈ t j

Tactic:
rw [update_of_ne h]

Goal state after:
case refine_2.inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ f j ∈ t j
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : One M
inst✝ : One N
toFun✝¹ : M → N
map_one'✝¹ : toFun✝¹ 1 = 1
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun = { toFun := toFun✝, map_one' := map_one'✝ }.toFun
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹ } = { toFun := toFun✝, map_one' := map_one'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Mul M
inst✝ : Mul N
toFun✝¹ : M → N
map_mul'✝¹ : ∀ (x y : M), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun = { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } = { toFun := toFun✝, map_mul' := map_mul'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : MulOne M
inst✝ : MulOne N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } = { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }

Tactic:
congr

Goal state after:
case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : MulOne M
inst✝ : MulOne N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ toOneHom✝¹ = toOneHom✝
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
toEquiv✝¹ : M ≃ N
map_mul'✝¹ : ∀ (x y : M), toEquiv✝¹.toFun (x * y) = toEquiv✝¹.toFun x * toEquiv✝¹.toFun y
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), toEquiv✝.toFun (x * y) = toEquiv✝.toFun x * toEquiv✝.toFun y
h₁ : { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ }.toFun = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.toFun
h₂ : { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ }.invFun = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.invFun
⊢ { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }

Tactic:
congr

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
toEquiv✝¹ : M ≃ N
map_mul'✝¹ : ∀ (x y : M), toEquiv✝¹.toFun (x * y) = toEquiv✝¹.toFun x * toEquiv✝¹.toFun y
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), toEquiv✝.toFun (x * y) = toEquiv✝.toFun x * toEquiv✝.toFun y
h₁ : { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ }.toFun = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.toFun
h₂ : { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ }.invFun = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.invFun
⊢ toEquiv✝¹ = toEquiv✝
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (range f) (range f)

Tactic:
by
  rw [← image_univ]
  exact h.bijOn_image ha.bijOn_univ hf.injOn

Goal state after:
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ f ⁻¹' s → fa x = fa x₂ → x = x₂

Tactic:
y

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
⊢ y ∈ f ⁻¹' s → fa x = fa y → x = y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (Subtype.val ∘ ⇑f) (g a) = (g.extendDomain f) ((Subtype.val ∘ ⇑f) a)

Tactic:
Function.comp_apply,

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ ↑(f (g a)) = (g.extendDomain f) ↑(f a)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) b) = (Subtype.val ∘ ⇑f) (g b)

Tactic:
Function.comp_apply,

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (g.extendDomain f) ↑(f b) = ↑(f (g b))
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
Function.comp_apply,

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ↑(f a)) = ↑(f a)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
Function.comp_apply,

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ↑(f a)) = ↑(f a)
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
⊢ f (x * y * z) = f (x * (y * z))

Tactic:
rw [mul, mul, mul, mul, mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ a⁻¹ ^ n = a ^ (-n)

Tactic:
inv_zpow,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ (a ^ n)⁻¹ = a ^ (-n)
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
h : x * y = 1
⊢ f x * ?m.113 = 1

Tactic:
by rw [← mul, h, one]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / c / (b / c) = a / b

Tactic:
by
  rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-↑(n + 1)) = (a ^ (n + 1))⁻¹

Tactic:
exact zpow_negSucc _ _

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
by
  rw [Int.sub_eq_add_neg, zpow_add, zpow_neg]

Goal state after:
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v, inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
congr

Goal state after:
case e_inv
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ i₁ = i₂
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = ↑h.unit * ↑h.unit⁻¹

Tactic:
congr

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

Goal state before:
pp: M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ n * f) = (c f)^[n + 1]

Tactic:
iterate_succ,

Goal state after:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ n * f) = (c f)^[n] ∘ c f
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
β : α → Type u_8
x : (a : α) → Perm (β a)
⊢ ∀ ⦃a₂ : (a : α) → Perm (β a)⦄, (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) a₂ → x = a₂

Tactic:
y

Goal state after:
α : Type u_7
β : α → Type u_8
x y : (a : α) → Perm (β a)
⊢ (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y → x = y
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x : Perm (Subtype p)
⊢ ∀ ⦃a₂ : Perm (Subtype p)⦄, ofSubtype x = ofSubtype a₂ → x = a₂

Tactic:
y

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
⊢ ofSubtype x = ofSubtype y → x = y
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
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
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
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a * a⁻¹ = a

Tactic:
· rw [mul_assoc, mul_inv_cancel₀ h, mul_one]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
split_ifs with h
  · rw [h, zpow_zero]
  · rw [zero_zpow _ h]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • x + r • -y = r • x + -(r • y)

Tactic:
smul_neg

Goal state after:
M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • x + -(r • y) = r • x + -(r • y)
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
hn : m ≤ n
⊢ ge n ⋯
      (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
    ge n hn fun k x ↦ Int.strongRec lt ge k

Tactic:
congr

Goal state after:
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
hn : m ≤ n
⊢ (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
    fun k x ↦ Int.strongRec lt ge k
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: a : ℤ
h : 1 < a.natAbs
x✝ : ℕ
⊢ (natAbs ∘ fun x ↦ a ^ x) x✝ = a.natAbs ^ x✝

Tactic:
Function.comp_apply,

Goal state after:
a : ℤ
h : 1 < a.natAbs
x✝ : ℕ
⊢ (a ^ x✝).natAbs = a.natAbs ^ x✝
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m.sqrt < n ↔ m < n * n

Tactic:
simp only [← not_le, le_sqrt]

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
h : 1 < n
⊢ n < n * n

Tactic:
by have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h); grind

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

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : toMulHom✝¹.toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), toMulHom✝¹.toFun (x + y) = toMulHom✝¹.toFun x + toMulHom✝¹.toFun y
toMulHom✝ : α →ₙ* β
map_zero'✝ : toMulHom✝.toFun 0 = 0
map_add'✝ : ∀ (x y : α), toMulHom✝.toFun (x + y) = toMulHom✝.toFun x + toMulHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }

Tactic:
congr

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : toMulHom✝¹.toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), toMulHom✝¹.toFun (x + y) = toMulHom✝¹.toFun x + toMulHom✝¹.toFun y
toMulHom✝ : α →ₙ* β
map_zero'✝ : toMulHom✝.toFun 0 = 0
map_add'✝ : ∀ (x y : α), toMulHom✝.toFun (x + y) = toMulHom✝.toFun x + toMulHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ toMulHom✝¹ = toMulHom✝
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : (↑toMonoidHom✝¹).toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), (↑toMonoidHom✝¹).toFun (x + y) = (↑toMonoidHom✝¹).toFun x + (↑toMonoidHom✝¹).toFun y
toMonoidHom✝ : α →* β
map_zero'✝ : (↑toMonoidHom✝).toFun 0 = 0
map_add'✝ : ∀ (x y : α), (↑toMonoidHom✝).toFun (x + y) = (↑toMonoidHom✝).toFun x + (↑toMonoidHom✝).toFun y
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }

Tactic:
congr

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : (↑toMonoidHom✝¹).toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), (↑toMonoidHom✝¹).toFun (x + y) = (↑toMonoidHom✝¹).toFun x + (↑toMonoidHom✝¹).toFun y
toMonoidHom✝ : α →* β
map_zero'✝ : (↑toMonoidHom✝).toFun 0 = 0
map_add'✝ : ∀ (x y : α), (↑toMonoidHom✝).toFun (x + y) = (↑toMonoidHom✝).toFun x + (↑toMonoidHom✝).toFun y
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ ^ (n + 1) = (r ^ (n + 1))⁻¹ʳ

Tactic:
rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
      Ring.inverse_pow r n]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ ↑⋯.unit⁻¹ = ↑u⁻¹

Tactic:
IsUnit.unit_of_val_units

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ ↑u⁻¹ = ↑u⁻¹
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : Ring R
a : R
n : ℕ
⊢ (-1) ^ n * a = 0 ↔ a = 0

Tactic:
rcases neg_one_pow_eq_or R n with h | h <;> simp [h]

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

Goal state before:
pp: α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2 * n + 1] = f

Tactic:
iterate_succ,

Goal state after:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2 * n] ∘ f = f
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inr
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ -1 = if Even n then 1 else -1

Tactic:
if_neg (by simpa using h)

Goal state after:
case inr
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ -1 = -1
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h✝ : a ≤ b
c : α
h : a < b
⊢ a * c ≤ b * c

Tactic:
· simpa [mul_comm] using (hmul _ _ _ h).le

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
h : a < 1
⊢ a * a < 1

Tactic:
exact mul_lt_one' h h

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : ZeroLEOneClass M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < a ^ 0

Tactic:
rw [pow_zero]

Goal state after:
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : ZeroLEOneClass M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < 1
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: case mk.mk
α : Sort u
β : Sort v
toFun✝¹ : α → β
inj'✝¹ : Injective toFun✝¹
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝¹, inj' := inj'✝¹ }.toFun = { toFun := toFun✝, inj' := inj'✝ }.toFun
⊢ { toFun := toFun✝¹, inj' := inj'✝¹ } = { toFun := toFun✝, inj' := inj'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
x : α
⊢ ∀ ⦃a₂ : α⦄,
    (fun a' ↦ if a' = a then b else if f a' = b then f a else f a') x =
        (fun a' ↦ if a' = a then b else if f a' = b then f a else f a') a₂ →
      x = a₂

Tactic:
y

Goal state after:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
x y : α
⊢ (fun a' ↦ if a' = a then b else if f a' = b then f a else f a') x =
      (fun a' ↦ if a' = a then b else if f a' = b then f a else f a') y →
    x = y
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x : { x // p x ∨ q x }
⊢ ∀ ⦃a₂ : { x // p x ∨ q x }⦄,
    (fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) x =
        (fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) a₂ →
      x = a₂

Tactic:
y

Goal state after:
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
⊢ (fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) x =
      (fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) y →
    x = y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
toFun✝¹ : α → β
map_rel'✝¹ : ∀ {a b : α}, r a b → s (toFun✝¹ a) (toFun✝¹ b)
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)
h :
  (fun o ↦ o.toFun) { toFun := toFun✝¹, map_rel' := map_rel'✝¹ } =
    (fun o ↦ o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ }
⊢ { toFun := toFun✝¹, map_rel' := map_rel'✝¹ } = { toFun := toFun✝, map_rel' := map_rel'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x : α
⊢ ∀ ⦃a₂ : α⦄, f x = f a₂ → x = a₂

Tactic:
y

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
⊢ f x = f y → x = y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
toFun✝¹ : α → β
inj'✝¹ : Injective toFun✝¹
map_rel_iff'✝¹ :
  ∀ {a b : α}, s ({ toFun := toFun✝¹, inj' := inj'✝¹ } a) ({ toFun := toFun✝¹, inj' := inj'✝¹ } b) ↔ r a b
toFun✝ : α → β
inj'✝ : Injective toFun✝
map_rel_iff'✝ : ∀ {a b : α}, s ({ toFun := toFun✝, inj' := inj'✝ } a) ({ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a b
h :
  (fun x ↦ x.toFun) { toFun := toFun✝¹, inj' := inj'✝¹, map_rel_iff' := map_rel_iff'✝¹ } =
    (fun x ↦ x.toFun) { toFun := toFun✝, inj' := inj'✝, map_rel_iff' := map_rel_iff'✝ }
⊢ { toFun := toFun✝¹, inj' := inj'✝¹, map_rel_iff' := map_rel_iff'✝¹ } =
    { toFun := toFun✝, inj' := inj'✝, map_rel_iff' := map_rel_iff'✝ }

Tactic:
congr

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

Goal state before:
pp: case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
⊢ Acc (Quotient.lift₂ r H) ⟦x✝⟧

Tactic:
| intro _ _ IH =>

Goal state after:
case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
⊢ Acc (Quotient.lift₂ r H) ⟦x✝⟧