mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : 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
f g : M →ₙ* N
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
g h : ι → M
⊢ ⇑f ∘ (g * h) = ⇑f ∘ g * ⇑f ∘ h

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ t' g, t ⊆ t' ∧ Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
y : β
hy : y ∈ t
t' : Set β
g : ↑s → ↑t'
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : ↑s), f ↑x = ↑(g x)
x : ↑s
hx : g x = ⟨y, ⋯⟩
⊢ f ↑x = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ SurjOn f ∅ t ↔ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝¹ : Subsingleton β
inst✝ : Nonempty β
⊢ SurjOn f s univ ↔ s.Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
⊢ s.Nonempty ∨ t = ∅

Tactic:
by

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

Goal state before:
pp: ι : 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
f g : M →* N
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ SurjOn f₂ s t

Tactic:
by

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOne M
inst✝² : MulOne N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ f a * f b = 1

Tactic:
by

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

Goal state before:
pp: 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 M N
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulEquivClass F M N
e : F
⊢ e 1 * e (EquivLike.inv e 1) = e (EquivLike.inv e 1)

Tactic:
by

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

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MulHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
a b : G
⊢ f (a / b) = f a / f b

Tactic:
by

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✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MulHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
⊢ ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
⊢ SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂)

Tactic:
by

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

Goal state before:
pp: 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
f g : M ≃* N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ SurjOn id s s

Tactic:
by

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 : ι → G
⊢ ⇑f ∘ g⁻¹ = (⇑f ∘ g)⁻¹

Tactic:
by

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

Goal state before:
pp: 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 α β
ι : Type u_9
M : ι → Type u_10
inst✝ : (i : ι) → Mul (M i)
i j : ι
h : i = j
x✝¹ x✝ : M i
⊢ (Equiv.cast ⋯).toFun (x✝¹ * x✝) = (Equiv.cast ⋯).toFun x✝¹ * (Equiv.cast ⋯).toFun x✝

Tactic:
by

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

Goal state before:
pp: 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
a b : G
⊢ f (a * b⁻¹) = f a * (f b)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
⊢ SurjOn g t p

Tactic:
by

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

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

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

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
e : M ≃* N
f : N →* P
⊢ (fun f ↦ f.comp ↑e.symm) (f.comp ↑e) = f

Tactic:
by

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
e : M ≃* N
f : P →* M
⊢ (↑e.symm).comp ((↑e).comp f) = f

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ SurjOn (g ∘ f) s (g '' t)

Tactic:
by

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

Goal state before:
pp: 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
a : G
⊢ f (a ^ 0) = f a ^ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
⊢ SurjOn (g ∘ f) (f ⁻¹' s) t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ SurjOn f univ univ ↔ Surjective f

Tactic:
by

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

Goal state before:
pp: 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
a : G
n : ℕ
⊢ f (a ^ (n + 1)) = f a ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
⊢ EqOn g₁ g₂ t

Tactic:
by

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

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ f (a ^ ↑n) = f a ^ ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : BijOn f s ∅
⊢ s = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ s = ∅ → BijOn f s ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
h : BijOn f ∅ t
⊢ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ t = ∅ → BijOn f ∅ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
b : β
⊢ BijOn f {a} {b} ↔ f a = b

Tactic:
by

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

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ f (a ^ Int.negSucc n) = f a ^ Int.negSucc n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
⊢ SurjOn f (f ⁻¹' t) t

Tactic:
by

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✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
b : β
hb : b ∈ t
⊢ p b

Tactic:
by

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 : ι → G
n : ℤ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
⊢ (∃ b, b ∈ t ∧ p b) → ∃ a, a ∈ s ∧ p (f a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
⊢ (∃ a, a ∈ s ∧ p (f a)) → ∃ b, b ∈ t ∧ p b

Tactic:
by

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : IsMulTorsionFree N
f : M →* N
hf : Injective ⇑f
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
⊢ (fun a ↦ a ^ n) (f x) = (fun a ↦ a ^ n) (f y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
p : Set γ
f : α → β
g : β → γ
hf : InjOn f s
⊢ BijOn (g ∘ f) s p ↔ BijOn g (f '' s) p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
⊢ p₂ (f a) = g (p₁ a)

Tactic:
by

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

Goal state before:
pp: ι : 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✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝⁴ : MulOne M
inst✝³ : MulOne N
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
f : F
hf : Injective ⇑f
inst✝ : IsDedekindFiniteMonoid N
a✝ b✝ : M
eq : a✝ * b✝ = 1
⊢ f (b✝ * a✝) = f 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hbij : BijOn f s t
hinj : InjOn g (p₁ '' s)
⊢ BijOn g (p₁ '' s) (p₂ '' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f univ univ ↔ Bijective f

Tactic:
by

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

Goal state before:
pp: ι : 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✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : LeftCancelMonoid N
f : M →ₙ* N
⊢ f 1 * 1 = f 1 * f 1

Tactic:
by

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

Goal state before:
pp: ι : 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✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : LeftCancelMonoid N
f : M →ₙ* N
⊢ f 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
⊢ BijOn f (s ∩ f ⁻¹' r) r

Tactic:
by

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

Goal state before:
pp: ι : 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✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : RightCancelMonoid N
f : M →ₙ* N
⊢ 1 * f 1 = f 1 * f 1

Tactic:
by

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

Goal state before:
pp: ι : 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✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : RightCancelMonoid N
f : M →ₙ* N
⊢ f 1 = 1

Tactic:
by

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

Goal state before:
pp: ι : 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
inst✝ : One P
hnp : OneHom N P
hmn : OneHom M N
⊢ hnp (hmn 1) = 1

Tactic:
by

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

Goal state before:
pp: ι : 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
inst✝ : Mul P
hnp : N →ₙ* P
hmn : M →ₙ* N
x y : M
⊢ hnp (hmn (x * y)) = hnp (hmn x) * hnp (hmn y)

Tactic:
by

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

Goal state before:
pp: ι : 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
inst✝ : MulOne P
hnp : N →* P
hmn : M →* N
⊢ hnp (hmn 1) = 1

Tactic:
by

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

Goal state before:
pp: ι : 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
inst✝ : MulOne P
hnp : N →* P
hmn : M →* N
⊢ ∀ (x y : M), hnp (hmn (x * y)) = hnp (hmn x) * hnp (hmn y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ MapsTo f s t

Tactic:
by

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✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ SurjOn f s t

Tactic:
by

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:
by

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✝² : MulOne M
inst✝¹ : MulOne N
inst✝ : MulOne 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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ x ∈ insert a s

Tactic:
by

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

Goal state before:
pp: ι : 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
f : OneHom M N
g : N → M
h₁ : LeftInverse g ⇑f
⊢ g 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ a ∈ insert a s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬f x = f a

Tactic:
h.injOn.eq_iff (by simp [hx]) (by simp)

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬x = a
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : 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
f : M →ₙ* N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x y : N
⊢ g (x * y) = g (f (g x) * f (g y))

Tactic:
by

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

Goal state before:
pp: ι : 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
f : M →ₙ* N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x y : N
⊢ g (f (g x) * f (g y)) = g (f (g x * g y))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
⊢ BijOn f s t

Tactic:
by

Goal state after:
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 * b = b * a

Tactic:
by

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

Goal state before:
pp: ι : 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
n : ℕ
f : Monoid.End M
⊢ (⇑f)^[n] = ⇑(npowRec n f)

Tactic:
by

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✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
⊢ f.comp 1 = 1

Tactic:
by

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✝² : MulOne M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
⊢ f.comp 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : DivisionMonoid β
f : α →* β
g h : α
⊢ f (g * h⁻¹) = f g * (f h)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ BijOn f (insert a s) (insert (f a) t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ BijOn f (s \ {a}) (t \ {f a})

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
⊢ f' y ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ x ∈ s₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f' (f x) ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ (-a.succ).succ = -a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ -a.pred = (-a).succ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ (-a.pred).pred = -a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ ↑(n - 1) = ↑n - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ a < a.succ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ a.pred < a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case ofNat
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i : ℕ
⊢ motive (ofNat i)

Tactic:
induction i with
    | zero => exact zero
    | succ i ih => exact succ _ ih

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' '' f '' s = s

Tactic:
by

Goal state after: