mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Init

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

Tactic:
by

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

Goal state before:
pp: a b✝ c d m n : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = motive (b + ↑0)

Tactic:
by

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

Goal state before:
pp: a b✝ c d m n✝ : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
n : ℕ
⊢ motive (b + ↑n + 1) = motive (b + ↑(n + 1))

Tactic:
by

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

Goal state before:
pp: a b✝ c d m n✝ : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
n : ℕ
⊢ motive (b + -[n+1] - 1) = motive (b + -[n + 1+1])

Tactic:
by

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

Goal state before:
pp: a b✝ c d m n✝ : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
n : ℕ
⊢ b + -[n+1] ≤ b

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' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
⊢ f (f' y) = y

Tactic:
by

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)
⊢ zero ≍
    match b - b with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

Tactic:
by

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ Int.inductionOn' (z + 1) b zero succ pred = succ z hz (Int.inductionOn' z b zero succ pred)

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b

Tactic:
rw [invFunOn, dif_pos h]
  exact Classical.choose_spec h

Goal state after:
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
⊢ invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b

Tactic:
by

Goal state after:
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
⊢ invFunOn f s b = Classical.choice inst✝

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
β : (a' : α) → a = a' → Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ = ⋯ ▸ f a' h

Tactic:
by

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
⊢ invFunOn f s (f x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
β : (a' : α) → a = a' → Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ ≍ f a' h

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
h : a ≍ a'
⊢ a = a'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α β : Sort u
a : α
b : β
h : a ≍ b
⊢ a = cast ⋯ b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α β : Sort u
a : α
b : β
h : a ≍ b
⊢ cast ⋯ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ InjOn (invFunOn f s) (f '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ invFunOn f s '' 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 α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) 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 : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ BijOn f (invFunOn f s '' t) t

Tactic:
by

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
⊢ Int.inductionOn' (z - 1) b zero succ pred = pred z hz (Int.inductionOn' z b zero succ pred)

Tactic:
by

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

Goal state before:
pp: a b c d m✝ n✝ m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n x✝³ : ℤ
x✝² : x✝³ ≤ m
x✝¹ : (hmn : m ≤ x✝³) → motive x✝³ hmn
x✝ : m ≤ x✝³ - 1
⊢ False

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 : α → β
⊢ SurjOn f s t ↔ ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
by

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) ⋯
⊢ Int.leInduction base succ m ⋯ = base

Tactic:
by

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

Goal state before:
pp: a b c d m✝ n✝ 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
⊢ m ≤ n + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
⊢ invMonoidHom.comp invMonoidHom = MonoidHom.id α

Tactic:
by

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✝¹ : One M
inst✝ : MulOneClass N
f g : OneHom M N
⊢ f 1 * g 1 = 1

Tactic:
by

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✝¹ : One M
inst✝ : InvOneClass N
f : OneHom M N
⊢ (f 1)⁻¹ = 1

Tactic:
by

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✝¹ : One M
inst✝ : DivisionMonoid N
f g : OneHom M N
⊢ f 1 / g 1 = 1

Tactic:
by

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
⊢ Int.leInduction base succ (n + 1) ⋯ = succ n hmn (Int.leInduction base succ n hmn)

Tactic:
by

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

Goal state before:
pp: a b c d m✝ n✝ m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
n : ℤ
hnm : n ≤ m
⊢ n - 1 ≤ m

Tactic:
by

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✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
by

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

Goal state before:
pp: a b c d m✝ n✝ m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n x✝³ : ℤ
x✝² : m ≤ x✝³
x✝¹ : (hnm : x✝³ ≤ m) → motive x✝³ hnm
x✝ : x✝³ + 1 ≤ m
⊢ False

Tactic:
by

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

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
by

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
⊢ f (x * y⁻¹) = 1

Tactic:
by

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✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f (x * y) = f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹

Tactic:
by

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) ⋯
⊢ Int.leInductionDown base pred m ⋯ = base

Tactic:
by

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✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹ = f x * f y

Tactic:
by

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

Goal state before:
pp: a b c d m✝ n✝ 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
⊢ n - 1 ≤ m

Tactic:
by

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✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
hf : ∀ (x y : G), f (x / y) = f x / f y
⊢ ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹

Tactic:
by

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
⊢ f 1 * g 1 = 1

Tactic:
by

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 * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
by

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✝² : MulOneClass N
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : M →* G
a b : M
⊢ (f (a * b))⁻¹ = (f a)⁻¹ * (f b)⁻¹

Tactic:
by

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
⊢ Int.leInductionDown base pred (n - 1) ⋯ = pred n hnm (Int.leInductionDown base pred n hnm)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
φ : G →* H
ψ : M →* G
⊢ φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹

Tactic:
by

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

Goal state before:
pp: a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
⊢ n ≥ m

Tactic:
by

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✝² : MulOneClass N
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f g : M →* G
a b : M
⊢ f (a * b) / g (a * b) = f a / g a * (f b / g b)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
g h : M →* G
⊢ f.comp (g / h) = f.comp g / f.comp h

Tactic:
by

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✝¹ : Group G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ ∀ (a b : G), a * b = b * a

Tactic:
by

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

Goal state before:
pp: a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝¹ : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
a✝ : l < _n + 1
hlm : ¬l < m
⊢ l ≥ m

Tactic:
by

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✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (a b : H), a * b = b * a

Tactic:
by

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

Goal state before:
pp: a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝¹ : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
a✝ : l < _n + 1
hlm : ¬l < m
k : ℤ
x✝ : k < l
⊢ k < _n

Tactic:
by

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

Goal state before:
pp: a b c d m n✝¹ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n✝ : ℤ
hnm : ¬n✝ < m
n : ℤ
x✝¹ : n ≤ m
hn : (k : ℤ) → k < n → motive k
l : ℤ
x✝ : l < n - 1
⊢ l < n

Tactic:
by

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
a : M
⊢ 2 ≠ 0

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℕ
x✝ : ↑(n + 1) ≠ 0
⊢ Injective fun a ↦ a ^ ↑(n + 1)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℕ
x✝ : Int.negSucc n ≠ 0
⊢ Injective fun a ↦ a ^ Int.negSucc n

Tactic:
by

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 = 1

Tactic:
by

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
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
by

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
ha : a ≠ 1
⊢ a ^ n = 1 ↔ n = 0

Tactic:
by

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

Goal state before:
pp: a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
⊢ motive n

Tactic:
by

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 = 1

Tactic:
by

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 = 1

Tactic:
by

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

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

Goal state before:
pp: a b c : ℤ
hbc : c ∣ b
⊢ a ∣ b / c ↔ c * a ∣ b

Tactic:
by

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

Goal state before:
pp: a b c d : ℤ
hb : b ≠ 0
hbc : b ∣ c
h : b * a = c * d
⊢ a = c / b * d

Tactic:
by

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

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign

Tactic:
by

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

Goal state before:
pp: i : ℤ
h : 0 < i
⊢ ↑(i.toNat - 1) = i - 1

Tactic:
by

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

Goal state before:
pp: m : ℤ
n : ℕ
hn : n ≠ 0
⊢ m.toNat < n ↔ m < ↑n

Tactic:
by

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

Goal state before:
pp: m : ℤ
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ (↑m).gcd -[n+1] = m.gcd (n + 1)

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ -[m+1].gcd ↑n = (m + 1).gcd n

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ -[m+1].gcd -[n+1] = (m + 1).gcd (n + 1)

Tactic:
by

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

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

Tactic:
gcd_assoc,

Goal state after:
a b c : ℤ
⊢ a.gcd ↑(b.gcd c) = (↑(a.gcd c)).gcd b
Module: Mathlib.Data.Int.Init

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

Tactic:
gcd_assoc,

Goal state after:
a b c : ℤ
⊢ a.gcd ↑(b.gcd c) = a.gcd ↑(c.gcd b)
Module: Mathlib.Data.Int.Init

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

Tactic:
by

Goal state after:
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'
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' 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 : α → β
t' : Set β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ SurjOn f univ 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 : α → β
t' : Set β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ ∃ s', s ⊆ s' ∧ BijOn f s' t'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
⊢ invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
⊢ invFun 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 : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
⊢ (range fun a ↦ x ⋯) ⊆ 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 : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
x✝ : α
⊢ (x✝ ∈ range fun a ↦ x ⋯) → ∀ ⦃x₂ : α⦄, (x₂ ∈ range fun a ↦ x ⋯) → f x✝ = f x₂ → x✝ = 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 : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
⊢ (f '' range fun a ↦ x ⋯) = 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 : α → β
hfs : SurjOn f s t
⊢ ∃ u, u ⊆ s ∧ InjOn f u ∧ f '' u = t

Tactic:
by

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
⊢ SurjOn fb (f '' s) (f '' t)

Tactic:
by

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
ha : Surjective fa
⊢ SurjOn fb (range f) (range f)

Tactic:
by

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

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

Tactic:
by

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
ha : Injective fa
hf : InjOn f (range fa)
⊢ InjOn fb (range f)

Tactic:
by

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
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (range f) (range f)

Tactic:
by

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 t : Set β
hb : MapsTo fb s t
x : α
hx : x ∈ f ⁻¹' s
⊢ fa x ∈ f ⁻¹' t

Tactic:
by

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)
⊢ InjOn fa (f ⁻¹' s)

Tactic:
by

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

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

Tactic:
by

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

Goal state after:
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
⊢ MapsTo (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)

Tactic:
by

Goal state after: