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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * (n + 1)) = (a ^ m) ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * n) = (a ^ n) ^ m

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ (a ^ m) ^ n = (a ^ n) ^ m

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
reg : IsLeftRegular a
eq : a * b = 1
⊢ (fun x ↦ a * x) (b * a) = (fun x ↦ a * x) 1

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
reg : IsRightRegular a
eq : b * a = 1
⊢ (fun x ↦ x * a) (a * b) = (fun x ↦ x * a) 1

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
⊢ y * x = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
⊢ y * x = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ (n + 1))⁻¹

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -((n + 1) • a)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
x : G
⊢ x⁻¹ = 1 / x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a b c : G
⊢ a * b / c = a * (b / c)

Tactic:
by

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

Goal state before:
pp: ι : Sort u_3
α : ι → Type u_1
β : ι → Type u_2
f f' : (i : ι) → α i
g g' : (i : ι) → β i
⊢ Function.prod f g = Function.prod f' g' ↔ f = f' ∧ g = g'

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 1 = a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 2 = a * a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
⊢ (f a == f b) = (a == b)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
⊢ a / a = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a⁻¹ * (a * b) = b

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a * (a⁻¹ * b) = b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a * b / b = a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a / b * b = a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b a : G
⊢ a⁻¹⁻¹ = a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b x✝¹ x✝ : G
⊢ x✝¹ * x✝ = 1 → x✝¹⁻¹ = x✝

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ a * x) b = (fun x ↦ a * x) c
⊢ b = c

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ b = c

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * (b * a) = b

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a * (b * a⁻¹) = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
⊢ ∃ x, f x ≠ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x : α
⊢ ∃ y, y ≠ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
x : α
⊢ ∃ y, y ≠ x

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
⊢ Nontrivial β

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ Subsingleton α → ∀ (x y : α), x = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ¬Nontrivial α ↔ Subsingleton α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ¬Subsingleton α ↔ Nontrivial α

Tactic:
rw [← not_nontrivial_iff_subsingleton, Classical.not_not]

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

Goal state before:
pp: α : Type u_1
⊢ ¬Subsingleton α ↔ Nontrivial α

Tactic:
by

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

Goal state before:
pp: α : Type u_3
⊢ Subsingleton α ∨ Nontrivial α

Tactic:
by

Goal state after:
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
⊢ x' ≠ y'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
⊢ Nontrivial α

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
⊢ (a = b) = (b = a)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ (a ↔ b) = (b ↔ a)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ : p x
y : α
property✝ : p y
⊢ ⟨x, property✝¹⟩ = ⟨y, property✝⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u_2
γ : Sort u_3
f : α → γ
g : β → γ
x : α
y : β
h₁ : f ≍ g
h₂ : x ≍ y
⊢ f x = g y

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α₁ α₂ : Sort u
β₁ : α₁ → Sort v
β₂ : α₂ → Sort v
f₁ : (a : α₁) → β₁ a
f₂ : (a : α₂) → β₂ a
a₁ : α₁
a₂ : α₂
hargs : a₁ ≍ a₂
ht : ∀ (t₁ : α₁) (t₂ : α₂), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂
hf : α₁ = α₂ → β₁ ≍ β₂ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₂

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
b c : α
h : ∀ {a : α}, a = b ↔ a = c
⊢ b = c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
b c : α
h : b = c
a : α
⊢ a = b ↔ a = c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a✝ b : α
h : a✝ = b
a : α
⊢ a✝ = a ↔ b = a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: ⊢ Xor True = Not

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: ⊢ Xor False = id

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a b = Xor b a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a : Prop
⊢ Xor a a = False

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor (¬a) b ↔ (a ↔ b)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a ¬b ↔ (a ↔ b)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor (¬a) ¬b ↔ Xor a b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
h : Xor a b
⊢ a ∨ b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
p : Prop
⊢ p ∧ a = b ↔ p ∧ b = a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
p : Prop
⊢ a = b ∧ p ↔ b = a ∧ p

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q : Prop
⊢ ¬Xor P Q ↔ (P ↔ Q)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a b ↔ (a ↔ ¬b)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a b ↔ (¬a ↔ b)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β γ : Sort u_1
e : α = β
a : α
c : γ
⊢ cast e a ≍ c ↔ a ≍ c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β γ : Sort u_1
e : β = γ
a : α
b : β
⊢ a ≍ cast e b ↔ a ≍ b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
a : α
b : β
e : β = α
⊢ a = cast e b → a ≍ b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
a : α
b : β
⊢ (∃ h, a = cast h b) → a ≍ b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: A : Prop
B : A → Prop
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ∃ a, ¬P a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ∀ (a : α), ¬P a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
β : α → Sort u_3
⊢ (∀ (a : α) (a : β a), True) ↔ True

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
β : α → Sort u_3
γ : (a : α) → β a → Sort u_4
⊢ (∀ (a : α) (b : β a) (a : γ a b), True) ↔ True

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a : α
p : α → Prop
⊢ (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: ι₁ : Sort u_3
ι₂ : Sort u_4
κ₁ : ι₁ → Sort u_5
κ₂ : ι₂ → Sort u_6
p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop
⊢ (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
q : Prop
p : α → Prop
inst✝ : Decidable q
⊢ (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : h₁
⊢ p True

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : ¬h₁
⊢ p False

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
⊢ p h

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Subsingleton ι
P : ι → ι → Prop
⊢ (∀ (i j : ι), P i j) ↔ ∀ (i : ι), P i i

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop
⊢ Decidable p

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
p : α → Prop
⊢ DecidablePred p

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
p : α → α → Prop
⊢ DecidableRel p

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α✝ : Sort u_1
α : Sort u_2
⊢ DecidableEq α

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Nonempty α
q : Prop
p : α → Prop
⊢ (∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Nonempty α
p : α → Prop
q : Prop
⊢ (∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
r p q : α → Prop
⊢ (∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c

Tactic:
by
  by_cases P <;> simp [*, exists_prop_of_true, exists_prop_of_false]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b c : α
⊢ ((∃ h, a = c) ∨ ∃ h, b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a : α
B : ¬P → α
⊢ dite P (fun x ↦ a) B ≠ a ↔ ∃ h, a ≠ B h

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
b : α
A : P → α
⊢ (dite P A fun x ↦ b) ≠ b ↔ ∃ h, A h ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ (∃ h, a ≠ b) ↔ ¬P ∧ a ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ (∃ h, a ≠ b) ↔ P ∧ a ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
⊢ dite P f g a = if h : P then f h a else g h a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
x y : α
z : β
⊢ f (if P then x else y) z = if P then f x z else f y z

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
A : P → α
inst✝ : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
⊢ (if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
by

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

Goal state before:
pp: α : Sort u
β : Sort v
h : Nonempty α
inst✝ : IsEmpty β
⊢ IsEmpty (α → β)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
h : ∀ (x y : α), (x == y) = (x == y)
⊢ inst1 = inst2

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
⊢ inst1 = inst2

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a ↦ p a) a
he : ∀ (y : α), (fun a ↦ p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ ⟨b, hb⟩ = default

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
p : α → Prop
h : p default
x : α
⊢ p x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ { default := x, uniq := h } = { default := y, uniq := uniq✝ }

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u
inst✝¹ : Subsingleton α
inst✝ : Nonempty α
⊢ Nonempty (Unique α)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α ∧ Nonempty α

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f i ≍ Function.const α (f default) x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α✝ : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst✝ : Unique ι
x : α default
i : ι
⊢ α i

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.Bijective f

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
y : α
x✝ : { x // x = y }
x : α
hx : x = y
⊢ ⟨x, hx⟩ = ⟨y, ⋯⟩

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
y : α
x✝ : { x // y = x }
x : α
hx : y = x
⊢ ⟨x, hx⟩ = ⟨y, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
⊢ f x = g y ↔ f = g

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
⊢ ¬Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : Nontrivial α
b : β
⊢ ¬Injective fun x ↦ b

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : α
h : f x = f y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (fun x ↦ if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) x₁ = (fun x ↦ if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) x₂
⊢ x₁ = x₂

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
⊢ (Injective fun g ↦ g ∘ f) ↔ Surjective f

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! y, p y
y : β
hpy : (fun y ↦ p y) y
hy : ∀ (y_1 : β), (fun y ↦ p y) y_1 → y_1 = y
x : α
hx : f x = y
⊢ (fun x ↦ p (f x)) x

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! x, p (f x)
x : α
hpx : (fun x ↦ p (f x)) x
hx : ∀ (y : α), (fun x ↦ p (f x)) y → y = x
y : β
hy : (fun y ↦ p y) y
z : α
hz : f z = y
⊢ (fun x ↦ p (f x)) z

Tactic:
by

Goal state after: