awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun (s : Set T) ↦ Sigma.mk (β := f) U (cast ⋯ s)
s t : Set T
h : g s = g t
this : cast hU ((g s).snd (β := f)) = cast hU ((g t).snd (β := f))
⊢ s = t

Tactic:
simp only [g, cast_cast, cast_eq] at this

Premises used: cast_cast, cast_eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun (s : Set T) ↦ Sigma.mk (β := f) U (cast ⋯ s)
s t : Set T
h : g s = g t
this : s = t
⊢ s = t

Tactic:
assumption
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun (s : Set T) ↦ Sigma.mk (β := f) U (cast ⋯ s)
s t : Set T
h : g s = g t
suffices : cast hU ((g s).snd (β := f)) = cast hU ((g t).snd (β := f))
⊢ s = t

Tactic:
suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun (s : Set T) ↦ Sigma.mk (β := f) U (cast ⋯ s)
s t : Set T
h : g s = g t
⊢ cast hU ((g s).snd (β := f)) = cast hU ((g t).snd (β := f))

Tactic:
congr
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun (s : Set T) ↦ Sigma.mk (β := f) U (cast ⋯ s)
⊢ Injective g

Tactic:
have hg : Injective g := by
    intro s t h
    suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
    · congr
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun (s : Set T) ↦ Sigma.mk (β := f) U (cast ⋯ s)
hg : Injective g
⊢ False

Tactic:
cantor_injective g hg

Premises used: Function.cantor_injective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun (s : Set T) ↦ Sigma.mk (β := f) U (cast ⋯ s)
hg : Injective g
⊢ False

Tactic:
exact cantor_injective g hg

Premises used: Function.cantor_injective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
⊢ ∃ (a : α), f a = Set T

Tactic:
cases hf (Set T) with | intro U hU =>
  let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
  have hg : Injective g := by
    intro s t h
    suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
    · congr
  exact cantor_injective g hg

Premises used: Set
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
g : β → Option α
H : IsPartialInv f g
x : α
⊢ g (f x) = some x

Tactic:
(H _ _).2 rfl

Premises used: Iff.mpr, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
g : β → Option α
H : IsPartialInv f g
x : β
h : (g x).isSome = true
⊢ f ((g x).get h) = x

Tactic:
(H _ _).1 (Option.eq_some_of_isSome h)

Premises used: Option.eq_some_of_isSome, Iff.mp
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
g : β → Option α
H : IsPartialInv f g
x y : α
⊢ (fun (x_1 : β) ↦ (g x_1).getD x) (f y) = y

Tactic:
simp [H.eq]

Premises used: Function.IsPartialInv.eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
g : β → Option α
H : IsPartialInv f g
⊢ Injective f

Tactic:
fun _ _ h ↦
  Option.some.inj <| ((H _ _).2 h).symm.trans ((H _ _).2 rfl)

Premises used: Iff.mpr, Option.some.inj, Function.Injective, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
g : β → Option α
H : IsPartialInv f g
x y : β
b : α
h₁ : b ∈ g x
h₂ : b ∈ g y
⊢ x = y

Tactic:
((H _ _).1 h₁).symm.trans ((H _ _).1 h₂)

Premises used: Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Type u_5
γ : Sort u_6
f : α → β
g : β → Option α
h : β → γ
i : γ → Option β
hf : IsPartialInv f g
hh : IsPartialInv h i
a : α
b : γ
⊢ (fun (x : γ) ↦ (i x).bind g) b = some a ↔ (h ∘ f) a = b

Tactic:
simp [Option.bind_eq_some_iff, hh _, hf _]

Premises used: Option.bind_eq_some_iff
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
g : β → α
f : α → β
h : LeftInverse g f
x : α
⊢ g (f x) = x

Tactic:
h x
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
g : β → α
f : α → β
h : RightInverse g f
x : β
⊢ f (g x) = x

Tactic:
h x
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
h : LeftInverse f g
⊢ f ∘ g = id

Tactic:
funext h

Premises used: funext
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
⊢ LeftInverse f g ↔ f ∘ g = id

Tactic:
⟨LeftInverse.comp_eq_id, congr_fun⟩

Premises used: Iff.intro, Function.LeftInverse.comp_eq_id, congr_fun
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
h : RightInverse f g
⊢ g ∘ f = id

Tactic:
funext h

Premises used: funext
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
⊢ RightInverse f g ↔ g ∘ f = id

Tactic:
⟨RightInverse.comp_eq_id, congr_fun⟩

Premises used: Function.RightInverse.comp_eq_id, Iff.intro, congr_fun
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : β → α
h : β → γ
i : γ → β
hf : LeftInverse f g
hh : LeftInverse h i
a : γ
rw : h (i a) = a
rw₁ rw₂ : a = a
⊢ h (f (g (i a))) = a

Tactic:
rw [hf (i a), hh a]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : β → α
h : β → γ
i : γ → β
hf : RightInverse f g
hh : RightInverse h i
⊢ RightInverse (h ∘ f) (g ∘ i)

Tactic:
LeftInverse.comp hh hf

Premises used: Function.RightInverse, Function.LeftInverse.comp
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
h : LeftInverse g f
⊢ RightInverse f g

Tactic:
h

Premises used: Function.RightInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
h : RightInverse g f
⊢ LeftInverse f g

Tactic:
h

Premises used: Function.RightInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
h : LeftInverse f g
⊢ Surjective f

Tactic:
h.rightInverse.surjective

Premises used: Function.LeftInverse.rightInverse, Function.RightInverse.surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
h : RightInverse f g
⊢ Injective f

Tactic:
h.leftInverse.injective

Premises used: Function.LeftInverse.injective, Function.RightInverse.leftInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
h : LeftInverse f g
hf : Injective f
⊢ RightInverse f g

Tactic:
fun x ↦ hf <| h (f x)

Premises used: Function.LeftInverse, Function.RightInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
h : LeftInverse f g
hg : Surjective g
⊢ RightInverse f g

Tactic:
fun x ↦ let ⟨y, hy⟩ := hg x; hy ▸ congr_arg g (h y)

Premises used: Function.LeftInverse, Eq.rec, congr_arg, _private.0.Function.LeftInverse.rightInverse_of_surjective.match_1, Function.RightInverse, Eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
⊢ RightInverse f g → Surjective f → LeftInverse f g

Tactic:
LeftInverse.rightInverse_of_surjective

Premises used: Function.RightInverse, Function.LeftInverse.rightInverse_of_surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g : β → α
⊢ RightInverse f g → Injective g → LeftInverse f g

Tactic:
LeftInverse.rightInverse_of_injective

Premises used: Function.LeftInverse.rightInverse_of_injective, Function.RightInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
rw : g₁ = g₁ ∘ id
rw₁ rw₂ : g₁ = g₁
⊢ g₁ = g₁ ∘ f ∘ g₂

Tactic:
rw [h₂.comp_eq_id, comp_id]

Premises used: Function.comp_id, Function.RightInverse.comp_eq_id
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
rw : (g₁ ∘ f) ∘ g₂ = g₂
rw₁ : id ∘ g₂ = g₂
rw₂ rw₃ : g₂ = g₂
⊢ g₁ ∘ f ∘ g₂ = g₂

Tactic:
rw [← comp_assoc, h₁.comp_eq_id, id_comp]

Premises used: Function.LeftInverse.comp_eq_id, Function.comp_assoc, Function.id_comp
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ∃ (a : α), f a = b
⊢ partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none

Tactic:
rw [hpi, dif_pos h'] at h

Premises used: dif_pos
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ∃ (a : α), f a = b
hpi₁ : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
⊢ ∃ (a : α), f a = b

Tactic:
rw [hpi, dif_pos h'] at h

Premises used: dif_pos
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ∃ (a : α), f a = b
hpi₁ : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h'₁ : ∃ (a : α), f a = b
⊢ some (Classical.choose (p := fun (x : α) ↦ f x = b) h'₁) = some a

Tactic:
rw [hpi, dif_pos h'] at h

Premises used: dif_pos
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ∃ (a : α), f a = b
h : some (Classical.choose (p := fun (x : α) ↦ f x = b) h') = some a
⊢ Classical.choose (p := fun (x : α) ↦ f x = b) h' = a

Tactic:
injection h with h
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ∃ (a : α), f a = b
h : Classical.choose (p := fun (x : α) ↦ f x = b) h' = a
subst : f (Classical.choose (p := fun (x : α) ↦ f x = b) h') = b
⊢ f a = b

Tactic:
subst h
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
b : β
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ∃ (a : α), f a = b
⊢ f (Classical.choose (p := fun (x : α) ↦ f x = b) h') = b

Tactic:
apply Classical.choose_spec h'

Premises used: Classical.choose_spec
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ¬∃ (a : α), f a = b
⊢ none = some a

Tactic:
rw [hpi, dif_neg h'] at h

Premises used: dif_neg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ¬∃ (a : α), f a = b
h₁ : none = some a
⊢ partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none

Tactic:
rw [hpi, dif_neg h'] at h

Premises used: dif_neg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ¬∃ (a : α), f a = b
h₁ : none = some a
hpi₁ : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
⊢ ¬∃ (a : α), f a = b

Tactic:
rw [hpi, dif_neg h'] at h

Premises used: dif_neg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose (p := fun (x : α) ↦ f x = b) h) else none
h' : ¬∃ (a : α), f a = b
⊢ f a = b

Tactic:
contradiction
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
⊢ ∀ (x : α), partialInv f (f x) = some x

Tactic:
I.isPartialInv.eq

Premises used: Function.Injective.isPartialInv, Function.IsPartialInv.eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
b : β
h : ∃ (a : α), f a = b
⊢ f (invFun f b) = b

Tactic:
simp only [invFun, dif_pos h, h.choose_spec]

Premises used: Function.invFun, Exists.choose_spec, dif_pos
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_3
β : Type u_4
f : α → β
a : α
⊢ f (invFun f (f a)) = f a

Tactic:
@invFun_eq _ _ ⟨a⟩ _ _ ⟨_, rfl⟩

Premises used: Exists.intro, Function.invFun_eq, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
b : β
h : ¬∃ (a : α), f a = b
⊢ invFun f b = Classical.choice inst

Tactic:
dif_neg h

Premises used: Function.invFun, dif_neg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
rw : f (invFun f b) = b
⊢ f (invFun f b) = f (g b)

Tactic:
rw [hg b]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b

Tactic:
invFun_eq ⟨g b, hg b⟩

Premises used: Exists.intro, Function.invFun_eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b

Tactic:
exact invFun_eq ⟨g b, hg b⟩

Premises used: Exists.intro, Function.invFun_eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
hf : Surjective f
⊢ RightInverse (invFun f) f

Tactic:
fun b ↦ invFun_eq <| hf b

Premises used: Function.LeftInverse, Function.RightInverse, Function.invFun_eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
hf : Injective f
⊢ LeftInverse (invFun f) f

Tactic:
fun b ↦ hf <| invFun_eq ⟨b, rfl⟩

Premises used: Function.LeftInverse, Exists.intro, Function.invFun_eq, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
hf : Injective f
⊢ Surjective (invFun f)

Tactic:
(leftInverse_invFun hf).surjective

Premises used: Function.leftInverse_invFun, Function.LeftInverse.surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
hf : Injective f
⊢ invFun f ∘ f = id

Tactic:
funext <| leftInverse_invFun hf

Premises used: funext, Function.leftInverse_invFun
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
hf : Injective f
⊢ HasLeftInverse f

Tactic:
⟨invFun f, leftInverse_invFun hf⟩

Premises used: Function.invFun, Function.leftInverse_invFun, Exists.intro, Function.HasLeftInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : Nonempty α
f : α → β
⊢ Injective f ↔ HasLeftInverse f

Tactic:
⟨Injective.hasLeftInverse, HasLeftInverse.injective⟩

Premises used: Function.HasLeftInverse.injective, Function.Injective.hasLeftInverse, Iff.intro
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
f : α → β
h : Surjective f
b : β
⊢ f (surjInv h b) = b

Tactic:
Classical.choose_spec (h b)

Premises used: Function.surjInv, Classical.choose_spec
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
f : α → β
hf : Surjective f
⊢ f ∘ surjInv hf = id

Tactic:
funext (Function.surjInv_eq _)

Premises used: funext, Function.surjInv_eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
f : α → β
hf : Surjective f
⊢ RightInverse (surjInv hf) f

Tactic:
surjInv_eq hf

Premises used: Function.LeftInverse, Function.surjInv_eq, Function.RightInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
f : α → β
hf : Bijective f
⊢ LeftInverse (surjInv ⋯) f

Tactic:
rightInverse_of_injective_of_leftInverse hf.1 (rightInverse_surjInv hf.2)

Premises used: Function.rightInverse_of_injective_of_leftInverse, And.right, And.left, Function.RightInverse, Function.rightInverse_surjInv
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
f : α → β
hf : Surjective f
⊢ HasRightInverse f

Tactic:
⟨_, rightInverse_surjInv hf⟩

Premises used: Exists.intro, Function.rightInverse_surjInv, Function.HasRightInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
f : α → β
⊢ Surjective f ↔ HasRightInverse f

Tactic:
⟨Surjective.hasRightInverse, HasRightInverse.surjective⟩

Premises used: Function.Surjective.hasRightInverse, Function.HasRightInverse.surjective, Iff.intro
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
f : α → β
⊢ Bijective f ↔ ∃ (g : β → α), LeftInverse g f ∧ RightInverse g f

Tactic:
⟨fun hf ↦ ⟨_, leftInverse_surjInv hf, rightInverse_surjInv hf.2⟩, fun ⟨_, gl, gr⟩ ↦
    ⟨gl.injective, gr.surjective⟩⟩

Premises used: Function.LeftInverse.injective, Function.surjInv, _private.0.Function.bijective_iff_has_inverse.match_1, And.right, And.intro, Iff.intro, Exists.intro, Function.rightInverse_surjInv, Function.Bijective, Function.RightInverse.surjective, Function.leftInverse_surjInv
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
f : α → β
h : Surjective f
⊢ Injective (surjInv h)

Tactic:
(rightInverse_surjInv h).injective

Premises used: Function.rightInverse_surjInv, Function.RightInverse.injective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
na : Nonempty α
inst : Subsingleton β
f : α → β
⊢ Surjective f

Tactic:
fun _ ↦ let ⟨a⟩ := na; ⟨a, Subsingleton.elim _ _⟩

Premises used: _private.0.Function.const_injective.match_1, Exists, Exists.intro, Subsingleton.elim, Eq, Function.Surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
hf : ∀ (i : ι), Surjective (f i)
⊢ Surjective (Pi.map (α := α) (β := β) f)

Tactic:
fun g ↦
  ⟨fun i ↦ surjInv (hf i) (g i), funext fun _ ↦ rightInverse_surjInv _ _⟩

Premises used: Function.surjInv, funext, Exists.intro, Function.rightInverse_surjInv, Function.Surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
g : β → γ
hg : Surjective g
⊢ Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x

Tactic:
.piMap fun _ ↦ hg

Premises used: Function.Surjective.piMap
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Nonempty α
g : β → γ
⊢ (Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x) ↔ Surjective g

Tactic:
⟨fun h c ↦ Nonempty.elim ‹_› fun a ↦ ?_, (·.comp_left)⟩

Premises used: Function.Surjective.comp_left, Nonempty.elim, Iff.intro
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Nonempty α
g : β → γ
refine : ∀ (h : Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x) (c : γ) (a : α), ∃ (a : β), g a = c
⊢ (Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x) ↔ Surjective g

Tactic:
refine ⟨fun h c ↦ Nonempty.elim ‹_› fun a ↦ ?_, (·.comp_left)⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Nonempty α
g : β → γ
h : Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x
c : γ
a : α
have : ∀ (f : α → β) (hf : Eq (α := α → γ) ((fun (x : α → β) ↦ g ∘ x) f) fun (x : α) ↦ c), ∃ (a : β), g a = c
⊢ ∃ (a : β), g a = c

Tactic:
have ⟨f, hf⟩ := h fun _ ↦ c
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Nonempty α
g : β → γ
h : Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x
c : γ
a : α
f : α → β
hf : Eq (α := α → γ) ((fun (x : α → β) ↦ g ∘ x) f) fun (x : α) ↦ c
⊢ ∃ (a : β), g a = c

Tactic:
⟨f a, congr_fun hf _⟩

Premises used: Exists.intro, congr_fun
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Nonempty α
g : β → γ
h : Surjective (β := α → γ) fun (x : α → β) ↦ g ∘ x
c : γ
a : α
f : α → β
hf : Eq (α := α → γ) ((fun (x : α → β) ↦ g ∘ x) f) fun (x : α) ↦ c
⊢ ∃ (a : β), g a = c

Tactic:
exact ⟨f a, congr_fun hf _⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
hf : ∀ (i : ι), Bijective (f i)
⊢ Bijective (Pi.map (α := α) (β := β) f)

Tactic:
⟨.piMap fun i ↦ (hf i).1, .piMap fun i ↦ (hf i).2⟩

Premises used: Function.Surjective.piMap, And.right, And.left, And.intro, Function.Bijective, Function.Injective.piMap
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
g : β → γ
hg : Bijective g
⊢ Bijective (β := α → γ) fun (x : α → β) ↦ g ∘ x

Tactic:
⟨hg.injective.comp_left, hg.surjective.comp_left⟩

Premises used: Function.Surjective.comp_left, Function.Bijective.injective, Function.Bijective.surjective, And.intro, Function.Bijective, Function.Injective.comp_left
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
a : α
v : β a
f : (a : α) → β a
⊢ update (β := β) f a v a = v

Tactic:
dif_pos rfl

Premises used: Function.update, dif_pos, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
a a' : α
h : a ≠ a'
v : β a'
f : (a : α) → β a
⊢ update (β := β) f a' v a = f a

Tactic:
dif_neg h

Premises used: Function.update, dif_neg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
inst : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
inl : update (β := fun (a : α) ↦ β) f a b a = if a = a then b else f a
inr : ∀ (hne : a ≠ a'), update (β := fun (a : α) ↦ β) f a' b a = if a = a' then b else f a
⊢ update (β := fun (a : α) ↦ β) f a' b a = if a = a' then b else f a

Tactic:
rcases Decidable.eq_or_ne a a' with rfl | hne

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
inst : DecidableEq α
β : Sort u_1
f : α → β
b : β
a : α
⊢ update (β := fun (a : α) ↦ β) f a b a = if a = a then b else f a

Tactic:
simp [*]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
inst : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
hne : a ≠ a'
⊢ update (β := fun (a : α) ↦ β) f a' b a = if a = a' then b else f a

Tactic:
simp [*]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
α' : Sort w
inst : DecidableEq α
inst_1 : Subsingleton α
a : α
v : α'
f : α → α'
⊢ update (β := fun (a : α) ↦ α') f a v = const α v

Tactic:
funext fun a' ↦ Subsingleton.elim a a' ▸ update_self ..

Premises used: Eq.rec, funext, Function.update_self, Subsingleton.elim
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
h : ∀ (a : α), Nonempty.{v} (β a)
a : α
⊢ Surjective (α := (x : α) → β x) (eval (β := β) a)

Tactic:
fun b ↦
  ⟨@update _ _ (Classical.decEq α) (fun a ↦ (h a).some) a b,
   @update_self _ _ (Classical.decEq α) _ _ _⟩

Premises used: Function.update, Nonempty.some, Exists.intro, Function.update_self, Function.Surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : α → Sort v
inst : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update (β := β) f a' v = update (β := β) f a' v'
⊢ update (β := β) f a' v a' = update (β := β) f a' v' a'

Tactic:
have := congr_fun h a'