awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α_1 : Sort u_1
α : Type u_2
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
x : α
xs : List α
hx : ¬p x
this : Decidable (∃! x : α, x ∈ xs ∧ p x)
⊢ (∃! x : α, x ∈ xs ∧ p x) ↔ ∃! x_1 : α, x_1 ∈ x :: xs ∧ p x_1

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : α → Sort u_4
x : α
f : (x : α) → β x
⊢ eval (β := β) x f = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
y : β
⊢ (fun (x : α) ↦ y) = const α y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
⊢ Injective (α := β) (const α)

Tactic:
fun _ _ h ↦
  let ⟨x⟩ := ‹Nonempty α›
  congr_fun h x

Premises used: _private.0.Function.const_injective.match_1, Function.Injective, congr_fun, Eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
y₁ y₂ : β
⊢ const α y₁ = const α y₂ ↔ y₁ = y₂

Tactic:
⟨fun h ↦ const_injective h, fun h ↦ h ▸ rfl⟩

Premises used: Eq.rec, Function.const_injective, Iff.intro, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : β → β → γ
g : α → β
a b : α
⊢ (f on g) a b = f (g a) (g b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → α → γ
g : β → α
h : δ → β
⊢ (f on g on h) = (f on g ∘ h)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → α → γ
g : β → α
h : δ → β
⊢ (f on g ∘ h) = (f on g on h)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hinj : Injective f
inst : IsPartialOrder β r
⊢ IsPartialOrder α (r on f)

Tactic:
{ hinj.antisymm_onFun r with }

Premises used: IsPartialOrder.mk, Function.Injective.antisymm_onFun
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hinj : Injective f
inst : IsLinearOrder β r
⊢ IsLinearOrder α (r on f)

Tactic:
{ hinj.isPartialOrder_onFun r with }

Premises used: IsLinearOrder.mk, Function.Injective.isPartialOrder_onFun
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hinj : Injective f
inst : IsStrictTotalOrder β r
⊢ IsStrictTotalOrder α (r on f)

Tactic:
{ hinj.trichotomous_onFun r with }

Premises used: Function.Injective.trichotomous_onFun, IsStrictTotalOrder.mk
-- Module: Mathlib.Logic.Function.Basic
Goal:
α α' : Sort u
β : α → Sort v
β' : α' → Sort v
f : (a : α) → β a
f' : (a : α') → β' a
hα : α = α'
h : ∀ (a : α) (a' : α'), a ≍ a' → f a ≍ f' a'
subst : ∀ {β' : α → Sort v} {f' : (a : α) → β' a} (h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'), f ≍ f'
⊢ f ≍ f'

Tactic:
subst hα
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
⊢ ∀ (a : α), f a ≍ f' a

Tactic:
have : ∀ a, f a ≍ f' a := fun a ↦ h a a (HEq.refl a)
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : 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
h₁ : ∀ (a : α), β a = β' a
⊢ β = β'

Tactic:
funext a
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : 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
a : α
⊢ β a = β' a

Tactic:
type_eq_of_heq (this a)

Premises used: type_eq_of_heq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : 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
a : α
⊢ β a = β' a

Tactic:
exact type_eq_of_heq (this a)

Premises used: type_eq_of_heq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : 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:
have : β = β' := by funext a; exact type_eq_of_heq (this a)
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this_1 : ∀ (a : α), f a ≍ f' a
this : β = β'
subst : ∀ {f' : (a : α) → β a} (h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a') (this : ∀ (a : α), f a ≍ f' a), f ≍ f'
⊢ f ≍ f'

Tactic:
subst this
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
f f' : (a : α) → β a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
⊢ f ≍ f'

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : α → Sort u_4
f₁ f₂ : (a : α) → β a
⊢ f₁ ≠ f₂ ↔ ∃ (a : α), f₁ a ≠ f₂ a

Tactic:
funext_iff.not.trans not_forall

Premises used: funext_iff, Iff.not, Iff.trans, Classical.not_forall
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
⊢ f x = g y ↔ f = g

Tactic:
⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩

Premises used: funext, Iff.intro
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
refine_1 : ∀ (h : f x = g y) (z : α), f z = g z
refine_2 : ∀ (h : f = g), f x = g y
⊢ f x = g y ↔ f = g

Tactic:
refine ⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
refine_1 : ∀ (h : f z = g y), f z = g z
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (h : f z = g z), f z = g z
⊢ f z = g z

Tactic:
rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
h : f = g
refine_2 : g x = g y
refine_2₁ refine_2₂ : g y = g y
⊢ f x = g y

Tactic:
rw [h, Subsingleton.elim x y]

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
inst : LT α
⊢ Eq.{u_4 + 1} (α := (y x : α) → Prop) (swap (φ := fun (x1 x2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : α) ↦
    x1 > x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
inst : LE α
⊢ Eq.{u_4 + 1} (α := (y x : α) → Prop) (swap (φ := fun (x1 x2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x1 x2 : α) ↦
    x1 ≥ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
inst : LT α
⊢ Eq.{u_4 + 1} (α := (y x : α) → Prop) (swap (φ := fun (x1 x2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x1 > x2) fun (x1 x2 : α) ↦
    x1 < x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
inst : LE α
⊢ Eq.{u_4 + 1} (α := (y x : α) → Prop) (swap (φ := fun (x1 x2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x1 ≥ x2) fun (x1 x2 : α) ↦
    x1 ≤ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
⊢ Injective f

Tactic:
hf.1

Premises used: And.left
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
⊢ Surjective f

Tactic:
hf.2

Premises used: And.right
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
⊢ ¬Injective f ↔ ∃ (a : α), ∃ (b : α), f a = f b ∧ a ≠ b

Tactic:
simp only [Injective, not_forall, exists_prop]

Premises used: exists_prop, Function.Injective, Classical.not_forall
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Type u_5
inst : Nontrivial α
b : β
rw : ∃ (a : α), ∃ (b_1 : α), b = b ∧ a ≠ b_1
⊢ ¬Injective.{u_4 + 1, u_5 + 1} (β := β) fun (x : α) ↦ b

Tactic:
rw [not_injective_iff]

Premises used: Function.not_injective_iff
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Type u_5
inst : Nontrivial α
b : β
obtain : ∀ (a₁ a₂ : α) (h : a₁ ≠ a₂), ∃ (a : α), ∃ (b_1 : α), b = b ∧ a ≠ b_1
⊢ ∃ (a : α), ∃ (b_1 : α), b = b ∧ a ≠ b_1

Tactic:
obtain ⟨a₁, a₂, h⟩ := exists_pair_ne α

Premises used: exists_pair_ne
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Type u_5
inst : Nontrivial α
b : β
a₁ a₂ : α
h : a₁ ≠ a₂
⊢ ∃ (a : α), ∃ (b_1 : α), b = b ∧ a ≠ b_1

Tactic:
⟨a₁, a₂, rfl, h⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Type u_5
inst : Nontrivial α
b : β
a₁ a₂ : α
h : a₁ ≠ a₂
⊢ ∃ (a : α), ∃ (b_1 : α), b = b ∧ a ≠ b_1

Tactic:
exact ⟨a₁, a₂, rfl, h⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
⊢ Injective g

Tactic:
fun _ _ h ↦ I <| congr_arg f h

Premises used: congr_arg, Function.Injective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
g : γ → α
⊢ Injective (f ∘ g) ↔ Injective g

Tactic:
⟨Injective.of_comp, hf.comp⟩

Premises used: Function.Injective.comp, Iff.intro, Function.Injective.of_comp
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : 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
obtain : ∀ (x : γ) (h : f (g x) = f y), g x = y
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := hg x

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
y : α
x : γ
h : f (g x) = f y
obtain : ∀ (y : γ) (h : f (g x) = f (g y)), g x = g y
⊢ g x = y

Tactic:
obtain ⟨y, rfl⟩ := hg y

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : γ
h : f (g x) = f (g y)
⊢ g x = g y

Tactic:
congr_arg g (I h)

Premises used: congr_arg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : γ
h : f (g x) = f (g y)
⊢ g x = g y

Tactic:
exact congr_arg g (I h)

Premises used: congr_arg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
hf : Surjective f
hg : Surjective g
I : Injective (f ∘ g)
⊢ Bijective f ∧ Bijective g

Tactic:
⟨⟨I.of_comp_right hg, hf⟩, I.of_comp, hg⟩

Premises used: And.intro, Function.Injective.of_comp_right, Function.Injective.of_comp
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
hg : Bijective g
⊢ Injective (f ∘ g) ↔ Injective f

Tactic:
⟨fun I ↦ I.of_comp_right hg.2, fun h ↦ h.comp hg.injective⟩

Premises used: Function.Bijective.injective, And.right, Function.Injective.comp, Iff.intro, Function.Injective.of_comp_right
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_4
α : ι → Sort u_5
β : ι → Sort u_6
f : (i : ι) → α i → β i
hf : ∀ (i : ι), Injective (f i)
⊢ Injective (Pi.map (α := α) (β := β) f)

Tactic:
fun _ _ h ↦
  funext fun i ↦ hf i <| congrFun h _

Premises used: funext, congrFun, Function.Injective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
g : β → γ
hg : Injective g
⊢ Injective (β := α → γ) fun (x : α → β) ↦ g ∘ x

Tactic:
.piMap fun _ ↦ hg

Premises used: Function.Injective.piMap
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
inst : Nonempty α
g : β → γ
⊢ (Injective (β := α → γ) fun (x : α → β) ↦ g ∘ x) ↔ Injective g

Tactic:
⟨fun h b₁ b₂ eq ↦ Nonempty.elim ‹_›
    (congr_fun <| h (a₁ := fun _ ↦ b₁) (a₂ := fun _ ↦ b₂) <| funext fun _ ↦ eq), (·.comp_left)⟩

Premises used: Nonempty.elim, funext, Iff.intro, Function.Injective.comp_left, congr_fun
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Subsingleton α
f : α → β
⊢ Injective f

Tactic:
fun _ _ _ ↦ Subsingleton.elim _ _

Premises used: Function.Injective, Subsingleton.elim
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
inst : Subsingleton α
f : α → α
⊢ Bijective f

Tactic:
⟨injective_of_subsingleton f, fun a ↦ ⟨a, Subsingleton.elim ..⟩⟩

Premises used: Function.injective_of_subsingleton, And.intro, Exists.intro, Function.Bijective, Subsingleton.elim
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
p : α → Prop
inst : DecidablePred p
f : { a : α // p a } → β
f' : { a : α // ¬p a } → β
hf : Injective.{max 1 u_1, u_2} f
hf' : Injective.{max 1 u_1, u_2} f'
im_disj :
  ∀ {x x' : α} {hx : p x} {hx' : ¬p x'},
    f (Subtype.mk (p := fun (a : α) ↦ p a) x hx) ≠ f' (Subtype.mk (p := fun (a : α) ↦ ¬p a) x' hx')
x₁ x₂ : α
h :
  Eq.{u_2} (α := β)
    ((fun (x : α) ↦
        (if h : p x then f (Subtype.mk (p := fun (a : α) ↦ p a) x h)
          else f' (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h) :
          β))
      x₁)
    ((fun (x : α) ↦
        (if h : p x then f (Subtype.mk (p := fun (a : α) ↦ p a) x h)
          else f' (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h) :
          β))
      x₂)
⊢ x₁ = x₂

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
S : Surjective (f ∘ g)
⊢ Surjective f

Tactic:
fun y ↦
  let ⟨x, h⟩ := S y
  ⟨g x, h⟩

Premises used: _private.0.Function.Surjective.of_comp.match_1, Exists, Exists.intro, Eq, Function.Surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
hg : Surjective g
⊢ Surjective (f ∘ g) ↔ Surjective f

Tactic:
⟨Surjective.of_comp, fun h ↦ h.comp hg⟩

Premises used: Function.Surjective.of_comp, Iff.intro, Function.Surjective.comp
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
S : Surjective (f ∘ g)
hf : Injective f
⊢ Surjective g

Tactic:
fun a ↦ let ⟨c, hc⟩ := S (f a); ⟨c, hf hc⟩

Premises used: Exists, Exists.intro, _private.0.Function.Surjective.of_comp_left.match_1, Eq, Function.Surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
hf : Injective f
hg : Injective g
S : Surjective (f ∘ g)
⊢ Bijective f ∧ Bijective g

Tactic:
⟨⟨hf, S.of_comp⟩, hg, S.of_comp_left hf⟩

Premises used: Function.Surjective.of_comp_left, Function.Surjective.of_comp, And.intro
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : γ → α
⊢ Surjective (f ∘ g) ↔ Surjective g

Tactic:
⟨fun S ↦ S.of_comp_left hf.1, hf.surjective.comp⟩

Premises used: Function.Surjective.of_comp_left, And.left, Function.Bijective.surjective, Iff.intro, Function.Surjective.comp
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Surjective f
p : β → Prop
⊢ (∀ (y : β), p y) ↔ ∀ (x : α), p (f x)

Tactic:
⟨fun h x ↦ h (f x), fun h y ↦
    let ⟨x, hx⟩ := hf y
    hx ▸ h x⟩

Premises used: Eq.rec, Iff.intro, _private.0.Function.Surjective.forall.match_1
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Surjective f
p : β → β → Prop
⊢ (∀ (y₁ y₂ : β), p y₁ y₂) ↔ ∀ (x₁ x₂ : α), p (f x₁) (f x₂)

Tactic:
hf.forall.trans <| forall_congr' fun _ ↦ hf.forall

Premises used: Function.Surjective.forall, forall_congr', Iff.trans
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Surjective f
p : β → β → β → Prop
⊢ (∀ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ↔ ∀ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)

Tactic:
hf.forall.trans <| forall_congr' fun _ ↦ hf.forall₂

Premises used: Function.Surjective.forall, forall_congr', Iff.trans, Function.Surjective.forall₂
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Surjective f
p : β → Prop
⊢ (∃ (y : β), p y) ↔ ∃ (x : α), p (f x)

Tactic:
⟨fun ⟨y, hy⟩ ↦
    let ⟨x, hx⟩ := hf y
    ⟨x, hx.symm ▸ hy⟩,
    fun ⟨x, hx⟩ ↦ ⟨f x, hx⟩⟩

Premises used: Exists, Eq.rec, _private.0.Function.Surjective.exists.match_2, _private.0.Function.Surjective.exists.match_1, Iff.intro, Exists.intro, Eq.symm, _private.0.Function.Surjective.forall.match_1
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Surjective f
p : β → β → Prop
⊢ (∃ (y₁ : β), ∃ (y₂ : β), p y₁ y₂) ↔ ∃ (x₁ : α), ∃ (x₂ : α), p (f x₁) (f x₂)

Tactic:
hf.exists.trans <| exists_congr fun _ ↦ hf.exists

Premises used: Function.Surjective.exists, exists_congr, Iff.trans
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Surjective f
p : β → β → β → Prop
⊢ (∃ (y₁ : β), ∃ (y₂ : β), ∃ (y₃ : β), p y₁ y₂ y₃) ↔ ∃ (x₁ : α), ∃ (x₂ : α), ∃ (x₃ : α), p (f x₁) (f x₂) (f x₃)

Tactic:
hf.exists.trans <| exists_congr fun _ ↦ hf.exists₂

Premises used: Function.Surjective.exists, exists_congr, Function.Surjective.exists₂, Iff.trans
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Surjective f
⊢ Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f

Tactic:
fun _ _ h ↦ funext <| hf.forall.2 <| congr_fun h

Premises used: Iff.mpr, Function.Surjective.forall, funext, Function.Injective, congr_fun
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
⊢ (Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Surjective f

Tactic:
⟨not_imp_not.mp fun not_surj inj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.injective_comp_right)⟩

Premises used: Function.Surjective.injective_comp_right, Subsingleton.intro, Iff.intro, not_subsingleton, Iff.mp, not_imp_not
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
refine : ∀ (not_surj : ¬Surjective f) (inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
⊢ (Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Surjective f

Tactic:
refine ⟨not_imp_not.mp fun not_surj inj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.injective_comp_right)⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
have : ∀ (b₀ : β) (hb : ¬∃ (a : α), f a = b₀), c = c'
⊢ c = c'

Tactic:
have ⟨b₀, hb⟩ := not_forall.mp not_surj
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
refine_2 : ∀ (this : Eq (α := β → γ) (fun (x : β) ↦ c) fun (x : β) ↦ if x = b₀ then c' else c), c = c'
refine_1 :
  Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ c)
    ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ if x = b₀ then c' else c)
⊢ c = c'

Tactic:
have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
refine_2 : ∀ (this : Eq (α := β → γ) (fun (x : β) ↦ c) fun (x : β) ↦ if x = b₀ then c' else c), c = c'
refine_1 :
  Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ c)
    ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ if x = b₀ then c' else c)
⊢ c = c'

Tactic:
classical have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
this : Eq (α := β → γ) (fun (x : β) ↦ c) fun (x : β) ↦ if x = b₀ then c' else c
⊢ c = c'

Tactic:
simpa using congr_fun this b₀

Premises used: congr_fun
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
refine_1 :
  ∀ (a : α),
    Eq.{u_4 + 1} (α := γ) ((fun (g : β → γ) ↦ g ∘ f) (fun (x : β) ↦ c) a)
      ((fun (g : β → γ) ↦ g ∘ f) (fun (x : β) ↦ if x = b₀ then c' else c) a)
⊢ Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ c)
    ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ if x = b₀ then c' else c)

Tactic:
ext a
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((fun (g : β → γ) ↦ g ∘ f) (fun (x : β) ↦ c) a)
    ((fun (g : β → γ) ↦ g ∘ f) (fun (x : β) ↦ if x = b₀ then c' else c) a)

Tactic:
simp only [comp_apply, if_neg fun h ↦ hb ⟨a, h⟩]

Premises used: Exists.intro, Function.comp_apply, if_neg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Surjective f
g₁ g₂ : β → γ
⊢ g₁ ∘ f = g₂ ∘ f ↔ g₁ = g₂

Tactic:
hf.injective_comp_right.eq_iff

Premises used: Function.Injective.eq_iff, Function.Surjective.injective_comp_right
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
h : ∀ (g₁ g₂ : β → Prop), Eq.{max 1 u_1} (g₁ ∘ f) (g₂ ∘ f) → Eq.{max 1 u_2} g₁ g₂
⊢ Surjective f

Tactic:
injective_comp_right_iff_surjective.mp h

Premises used: Function.injective_comp_right_iff_surjective, Iff.mp
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
⊢ Bijective f ↔ ∀ (b : β), ∃! a : α, f a = b

Tactic:
⟨fun hf b ↦
      let ⟨a, ha⟩ := hf.surjective b
      ⟨a, ha, fun _ ha' ↦ hf.injective (ha'.trans ha.symm)⟩,
    fun he ↦ ⟨fun {_a a'} h ↦ (he (f a')).unique h rfl, fun b ↦ (he b).exists⟩⟩

Premises used: ExistsUnique.exists, Function.Bijective.injective, Function.Bijective.surjective, ExistsUnique, And.intro, Iff.intro, Exists.intro, ExistsUnique.unique, Eq.symm, Eq, rfl, Eq.trans, _private.0.Function.Surjective.forall.match_1
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
b : β
⊢ ∃! a : α, f a = b

Tactic:
(bijective_iff_existsUnique f).mp hf b

Premises used: Iff.mp, Function.bijective_iff_existsUnique
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
p : β → Prop
h : ∃! 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:
simpa [hx]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
p : β → Prop
h : ∃! 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:
simpa [hz]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
hg : Bijective g
⊢ Bijective (f ∘ g) ↔ Bijective f

Tactic:
and_congr (Injective.of_comp_iff' _ hg) (Surjective.of_comp_iff _ hg.surjective)

Premises used: Function.Injective.of_comp_iff', Function.Surjective.of_comp_iff, Function.Bijective.surjective, Function.Bijective, and_congr
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : γ → α
⊢ Bijective (f ∘ g) ↔ Bijective g

Tactic:
and_congr (Injective.of_comp_iff hf.injective _) (Surjective.of_comp_iff' hf _)

Premises used: Function.Surjective.of_comp_iff', Function.Bijective.injective, Function.Bijective, Function.Injective.of_comp_iff, and_congr
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Type u_5
f : α → α → β
hf : Surjective f
g : β → β
⊢ ∃ (x : β), g x = x

Tactic:
let ⟨a, ha⟩ := hf fun a => g (f a a)
  ⟨f a a, (congr_fun ha a).symm⟩

Premises used: _private.0.Function.exists_fixed_point_of_surjective.match_1, Exists, Exists.intro, congr_fun, Eq.symm, Eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
f : α → Set α
⊢ ¬Surjective f

Tactic:
fun hf ↦
  let ⟨a, ha⟩ := hf {a | a ∉ f a}
  iff_not_self <| .of_eq <| congrArg (a ∈ ·) ha

Premises used: False, Iff.of_eq, congrArg, setOf, iff_not_self, Membership.mem, _private.0.Function.cantor_surjective.match_1, Not