mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ Nontrivial α

Tactic:
have : x' ≠ y' := by
    refine fun H ↦ h ?_
    rw [← hx', ← hy', H]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
this : x' ≠ y'
⊢ Nontrivial α
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
⊢ Pi.map f (update g i a) = update (Pi.map f g) i (f i a)

Tactic:
ext j

Goal state after:
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
⊢ Pi.map f (update g i a) j = update (Pi.map f g) i (f i a) j
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.refl
α : Type u_1
r : α → α → Prop
a b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
hea : ReflTransGen r e b
⊢ Join (ReflTransGen r) e c

Tactic:
exact ⟨b, hea, hcb⟩

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
⊢ (Equiv.cast ⋯) x = ((Equiv.cast h).trans (Equiv.cast h2)) x

Tactic:
subst h h2; rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑(f.trans g) = ⇑(Equiv.refl α) ↔ f = g.symm

Tactic:
coe_trans,

Goal state after:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑g ∘ ⇑f = ⇑(Equiv.refl α) ↔ f = g.symm
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ r • x * (r • x) ^ n = r ^ (n + 1) • x ^ (n + 1)

Tactic:
smul_pow _ _ n,

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ r • x * r ^ n • x ^ n = r ^ (n + 1) • x ^ (n + 1)
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: case ofNat
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
a✝ : ℕ
⊢ (g • a) ^ Int.ofNat a✝ = g ^ Int.ofNat a✝ • a ^ Int.ofNat a✝

Tactic:
simp [smul_pow, smul_inv]

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

Goal state before:
pp: case negSucc
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
a✝ : ℕ
⊢ (g • a) ^ Int.negSucc a✝ = g ^ Int.negSucc a✝ • a ^ Int.negSucc a✝

Tactic:
simp [smul_pow, smul_inv]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
exact Or.inl (.left _ _ hij)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a ≤ const β b ↔ a ≤ b

Tactic:
simp [Pi.le_def]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ x✝¹ ⊓ x✝ = if x✝¹ ≤ x✝ then x✝¹ else x✝

Tactic:
by simp_rw [← hf.eq_iff, ← le, apply_ite f, ← min_def, min]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ a ⊓ b ≤ c

Tactic:
by rw [inf_comm]; exact sdiff_le_iff

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α✝
a✝ b✝ : α✝
α : Type u_2
inst✝ : CoheytingAlgebra α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ a ⊓ b ≤ c

Tactic:
by rw [inf_comm]; exact sdiff_le_iff

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
⊢ ⊥ ≤ a

Tactic:
rw [← le, map_bot]
    exact bot_le

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : Compl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ ⊥ ≤ a

Tactic:
rw [← le, map_bot]
    exact bot_le

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
s : Set α
⊢ insert a (s \ {b}) = insert a s \ {b}

Tactic:
← union_singleton,

Goal state after:
α : Type u_1
a b : α
hab : a ≠ b
s : Set α
⊢ s \ {b} ∪ {a} = (s ∪ {a}) \ {b}
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)), ∃ a, Sigma.map f₁ f₂ a = ⟨f₁ x, b⟩

Tactic:
exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩

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

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)

Tactic:
sdiff_inf,

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = (a ⊓ b) \ a ⊔ (a ⊓ b) \ c
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
f : α → β
⊢ (f ⁻¹' s).Nonempty ↔ (s ∩ range f).Nonempty

Tactic:
simp [Set.Nonempty]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ p ⁻¹' {True} = {a | p a}

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ p ⁻¹' {False} = {a | ¬p a}

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ ∅ = f '' s ↔ s = ∅

Tactic:
by
  rw [eq_comm, image_eq_empty]

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

Goal state before:
pp: α : Type u_1
⊢ image id = id

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ f ⁻¹' g ⁻¹' s = s

Tactic:
by rw [← preimage_comp, h.comp_eq_id, preimage_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ InjOn f (insert a s) ↔ InjOn f s ∧ ¬f a ∈ f '' s

Tactic:
← union_singleton,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ InjOn f (s ∪ {a}) ↔ InjOn f s ∧ ¬f a ∈ f '' s
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
⊢ ⇑f ∘ g⁻¹ = (⇑f ∘ g)⁻¹

Tactic:
by ext; simp

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
⊢ (↑e).comp ↑e.symm = MonoidHom.id N

Tactic:
by ext; simp

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
⊢ (↑e.symm).comp ↑e = MonoidHom.id M

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
⊢ ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
by ext; simp

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
← MulHom.comp_apply,

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₁) x = g (f₂ x)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : IsMulCommutative M
a b : N
a' : M
ha' : f a' = a
b' : M
hb' : f b' = b
⊢ a * b = b * a

Tactic:
simp [← ha', ← hb', ← map_mul, mul_comm']

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y

Tactic:
refine fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_
      rw [← h.image_eq]
      exact ⟨x, hxs, hxy⟩

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ (fun x ↦ a * x)^[0] = fun x ↦ a ^ 0 * x

Tactic:
by ext; simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ (fun x ↦ x * a)^[0] = fun x ↦ x * a ^ 0

Tactic:
by ext; simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
k : ℕ
⊢ (fun x ↦ x ^ k)^[0] = fun x ↦ x ^ k ^ 0

Tactic:
by ext; simp

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a ↦ a / b

Tactic:
simp only [div_eq_mul_inv]
  exact fun a a' h ↦ mul_left_injective b⁻¹ h

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

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

Tactic:
← zpow_sub_one,

Goal state after:
case pred
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ (m + -↑n - 1)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']
  simp only [mul_comm, eq_comm]

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

Goal state before:
pp: α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a⁻¹ * a = 1

Tactic:
change ↑(h a).unit⁻¹ * a = 1

Goal state after:
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑⋯.unit⁻¹ * a = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a⁻¹ * a = 1

Tactic:
change ↑(h a).unit⁻¹ * a = 1

Goal state after:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑⋯.unit⁻¹ * a = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
⊢ a * ↑u = 1 ↔ a = ↑u⁻¹

Tactic:
← mul_inv_eq_one,

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
⊢ a * ↑u = 1 ↔ a * ↑u⁻¹⁻¹ = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a = ↑d⁻¹ * (c * ↑b) ↔ a * ↑d = c * ↑b

Tactic:
Units.eq_inv_mul_iff_mul_eq,

Goal state after:
α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ ↑d * a = c * ↑b ↔ a * ↑d = c * ↑b
Module: Mathlib.Algebra.Group.Equiv.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N✝ : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P✝ : Type u_12
Q✝ : Type u_13
G : Type u_14
H : Type u_15
inst✝² : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
⊢ (fun k m ↦ g.symm (k (f m))) ((fun h n ↦ g (h (f.symm n))) h) = h

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N✝ : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P✝ : Type u_12
Q✝ : Type u_13
G : Type u_14
H : Type u_15
inst✝² : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
⊢ (fun h n ↦ g (h (f.symm n))) ((fun k m ↦ g.symm (k (f m))) k) = k

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N✝ : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P✝ : Type u_12
Q✝ : Type u_13
G : Type u_14
H : Type u_15
inst✝² : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
⊢ (fun n ↦ g ((h * k) (f.symm n))) = (fun n ↦ g (h (f.symm n))) * fun n ↦ g (k (f.symm n))

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : M₁ ≃* M₂
f : M₁ →* N
⊢ (fun f ↦ f.comp e.toMonoidHom) ((fun f ↦ f.comp e.symm.toMonoidHom) f) = f

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : M₁ ≃* M₂
f : M₂ →* N
⊢ (fun f ↦ f.comp e.symm.toMonoidHom) ((fun f ↦ f.comp e.toMonoidHom) f) = f

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₁
⊢ e.symm.toMonoidHom.comp (e.toMonoidHom.comp f) = f

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₂
⊢ e.toMonoidHom.comp (e.symm.toMonoidHom.comp f) = f

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : CommMonoid N
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
e : M₁ ≃* M₂
f g : M₁ →* N
⊢ e.monoidHomCongrLeftEquiv.toFun (f * g) = e.monoidHomCongrLeftEquiv.toFun f * e.monoidHomCongrLeftEquiv.toFun g

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : CommMonoid N
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
e : N₁ ≃* N₂
f g : M →* N₁
⊢ e.monoidHomCongrRightEquiv.toFun (f * g) = e.monoidHomCongrRightEquiv.toFun f * e.monoidHomCongrRightEquiv.toFun g

Tactic:
by ext; simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)

Tactic:
by rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
⊢ { toFun := fun h ↦ 1 * h * 1⁻¹, invFun := fun h ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } = 1

Tactic:
by ext; simp

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y ↦ x * y) y = (fun y ↦ x * y) y'
⊢ y = y'

Tactic:
simpa only [← mul_assoc, inv_mul_cancel₀ h, one_mul] using congr_arg (fun y => x⁻¹ * y) w

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

Goal state before:
pp: case pos
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
hb : b = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

pp: case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
hb : ¬b = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
· simp [hb]

Goal state after:
case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
hb : ¬b = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))

Tactic:
h1,

Goal state after:
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑(1 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: m n : ℤ
⊢ (m % n).gcd n = m.gcd n

Tactic:
by
  conv_rhs => rw [← m.emod_add_mul_ediv n, gcd_add_mul_left_left]

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

Goal state before:
pp: n : ℕ
⊢ n < n.sqrt.succ ^ 2

Tactic:
by simpa [Nat.pow_two] using lt_succ_sqrt n

Goal state after:
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
n : ℕ
⊢ f n + f 1 = ↑(n + 1)

Tactic:
h1,

Goal state after:
A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
n : ℕ
⊢ f n + 1 = ↑(n + 1)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
⊢ x⁻¹ʳ * y = z

Tactic:
h1,

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
⊢ x⁻¹ʳ * (x * z) = z
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * z⁻¹ʳ
⊢ x * z = y

Tactic:
h1,

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * z⁻¹ʳ
⊢ y * z⁻¹ʳ * z = y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a / b * b = a

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a * b / b = a

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ (a * if h0 : a = 0 then 0 else ↑⋯.unit⁻¹) = 1

Tactic:
change (a * if h0 : a = 0 then 0 else ↑((h a).resolve_right h0).unit⁻¹) = 1
      rw [dif_neg h0, Units.mul_inv_eq_iff_eq_mul, one_mul, IsUnit.unit_spec]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
⊢ ↑0 = 0

Tactic:
← natCast,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
⊢ f ↑0 = 0