mathlib-initiative/mathlib-tactics huggingface dataset:
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₁
⊢ f' (f x) ∈ s₁

Tactic:
]

Goal state after:
α : 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₁
⊢ f' (f x) ∈ s₁
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₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
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₁
⊢ x ∈ s

Tactic:
]

Goal state after:
α : 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₁
⊢ x ∈ s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ -a = -a

Tactic:
]

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

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

Tactic:
]

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
⊢ s = s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
x : α
hx : x ∈ s
heq : f x = y
⊢ f x = f x

Tactic:
]

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

Goal state before:
pp: motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ cast ?m.44 zero =
    match 0 with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

pp: motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = (fun x ↦ motive x) (b + 0)

Tactic:
]

Goal state after:
motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ cast ?m.44 zero =
    match 0 with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = (fun x ↦ motive x) (b + 0)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ y ∈ s

Tactic:
]

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ y ∈ s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ Classical.choose h ∈ s ∧ f (Classical.choose h) = b

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ Classical.choose h ∈ s ∧ f (Classical.choose h) = b
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ¬∃ a, a ∈ s ∧ f a = b
⊢ Classical.choice inst✝ = Classical.choice inst✝

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' f '' s
x : α
hx' : x ∈ s
hx : invFunOn f s (f x) ∈ s
⊢ invFunOn f s (f x) = invFunOn f s (f x)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f x' = f x'

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ invFunOn f s y = invFunOn f s y

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ y ∈ t

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ y ∈ t
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
⊢ base = base

Tactic:
]

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
⊢ succ n hmn
      (Int.inductionOn' (motive := fun x ↦ (hmn : m ≤ x) → motive x hmn) n m (fun x ↦ base)
        (fun k hle ih x ↦ succ k hle (ih hle)) (fun x x_1 x_2 x_3 ↦ ⋯.elim) hmn) =
    succ n hmn (Int.leInduction base succ n hmn)

Tactic:
]

Goal state after:
m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
⊢ succ n hmn
      (Int.inductionOn' (motive := fun x ↦ (hmn : m ≤ x) → motive x hmn) n m (fun x ↦ base)
        (fun k hle ih x ↦ succ k hle (ih hle)) (fun x x_1 x_2 x_3 ↦ ⋯.elim) hmn) =
    succ n hmn (Int.leInduction base succ n hmn)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : 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)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
]

Goal state after:
α : 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)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ f x * g x * f y * g y = f x * g x * f y * g y

Tactic:
]

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

Goal state before:
pp: F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
⊢ base = base

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ f x * g x * f y * g y = f x * g x * f y * g y

Tactic:
]

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ pred n hnm
      (Int.inductionOn' (motive := fun x ↦ (hnm : x ≤ m) → motive x hnm) n m (fun x ↦ base) (fun x x_1 x_2 x_3 ↦ ⋯.elim)
        (fun k hle ih x ↦ pred k hle (ih hle)) hnm) =
    pred n hnm (Int.leInductionDown base pred n hnm)

Tactic:
]

Goal state after:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ pred n hnm
      (Int.inductionOn' (motive := fun x ↦ (hnm : x ≤ m) → motive x hnm) n m (fun x ↦ base) (fun x x_1 x_2 x_3 ↦ ⋯.elim)
        (fun k hle ih x ↦ pred k hle (ih hle)) hnm) =
    pred n hnm (Int.leInductionDown base pred n hnm)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2
α : 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)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'

Tactic:
]

Goal state after:
case refine_2
α : 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)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a ^ n = 1

Tactic:
]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a ^ n = 1

Tactic:
]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a = a⁻¹ ↔ a = a⁻¹

Tactic:
]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a = 1 ↔ a = 1

Tactic:
]

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

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((↑m + 1 - 1) / (↑n + 1) + 1)

Tactic:
]

Goal state after:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((↑m + 1 - 1) / (↑n + 1) + 1)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -(↑m / (↑n + 1) + 1)

Tactic:
]

Goal state after:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -(↑m / (↑n + 1) + 1)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d

Tactic:
]

Goal state after:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b d : ℤ
hb : b ≠ 0
k : ℤ
h : a = k * d
⊢ a = k * d

Tactic:
]

Goal state after:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : a = k * d
⊢ a = k * d
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

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)
⊢ Disjoint s r

Tactic:
]

Goal state after:
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

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)
⊢ Disjoint s r
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ↑(m - n.succ) = ↑(m - n.succ)

Tactic:
]

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

Goal state before:
pp: a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ 0 < c - b ↔ 0 < c - b

Tactic:
]

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 : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' f '' s

Tactic:
]

Goal state after:
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 : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' f '' s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b c : ℤ
⊢ a.gcd ↑(c.gcd b) = a.gcd ↑(c.gcd b)

Tactic:
]

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

Goal state before:
pp: case refine_4
α : 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)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ f '' s₁ ∩ t'

Tactic:
]

Goal state after:
case refine_4
α : 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)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ f '' s₁ ∩ t'
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ a ∈ s ↔ a ∈ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' f '' s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)
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 (f '' univ) (f '' univ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)
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
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = fb (f y)
⊢ x = y

Tactic:
]

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 : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = fb (f y)
⊢ x = y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), e a ∈ t ↔ a ∈ s
b : β
hb : b ∈ t
⊢ b ∈ t

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), e a ∈ t ↔ a ∈ s
b : β
hb : b ∈ t
⊢ b ∈ t
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ n = a ^ n

Tactic:
]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ n = a ^ n

Tactic:
]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ m

Tactic:
]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n * a * (b * b ^ n) = a ^ n * a * (b * b ^ n)

Tactic:
]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ a * a ^ n * (b * b ^ n) = a * a ^ n * (b * b ^ n)

Tactic:
]

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsLeftCancelMul M
a b : M
⊢ a * b = a ↔ a * b = a

Tactic:
]

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsRightCancelMul M
a b : M
⊢ a * b = b ↔ a * b = b

Tactic:
]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * y⁻¹ = x * y⁻¹

Tactic:
]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
a b : G
⊢ a * b⁻¹ = a * b⁻¹

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : b * a = 1
⊢ a⁻¹ = a⁻¹

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ a⁻¹ = a⁻¹

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a / b = 1
⊢ a / b = 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a / b = 1
⊢ a / b = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = a ^ ↑(n + 1)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = a ^ ↑(n + 1)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
]

Goal state after:
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 * (f y * f z) = f x * (f y * f z)

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
⊢ b = b

Tactic:
]

Goal state after:
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✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = a ^ ↑(m * n)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = a ^ ↑(m * 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✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ n * f x = f x ^ n * f x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ * unop x✝ ^ x✝¹ = unop x✝ * unop x✝ ^ x✝¹

Tactic:
]

Goal state after:
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₁✝ ℕ
M₁ : Type u_3
inst✝¹ : Inv M₁
inst✝ : InvolutiveInv M₂
f : M₁ → M₂
hf : Injective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ f x = f x

Tactic:
]

Goal state after:
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✝ : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ ↑(m * n.succ) = a ^ ↑(m * (n + 1))

Tactic:
]

Goal state after:
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✝ : DivInvMonoid 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₁
⊢ f x * (f y)⁻¹ = f x * (f y)⁻¹

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ ↑(m.succ * n) = a ^ ↑((m + 1) * n)

Tactic:
]

Goal state after:
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✝ : DivInvMonoid 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 : M₁
⊢ 1 = 1

Tactic:
]

Goal state after: