awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst : Nonempty γ
h : ∃ (e : β → γ), g = e ∘ f
x x_1 : α
hf : f x = f x_1
rw :
  (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x =
    (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x_1
rw₁ :
  Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x) =
    (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x_1
rw₂ :
  Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x) =
    Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x_1)
rw₃ rw₄ :
  Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x_1) =
    Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x_1)
⊢ g x = g x_1

Tactic:
rw [Classical.choose_spec h, comp_apply, comp_apply, hf]

Premises used: Classical.choose_spec, Function.comp_apply
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
g : α → γ
F : γ → δ
f : α → β
e' : β → γ
b : β
⊢ F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b

Tactic:
open scoped Classical in apply_dite F _ _ _

Premises used: apply_dite, Function.extend
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : Eq (α := β → γ) ((fun (g : α → γ) ↦ extend f g e') g₁) ((fun (g : α → γ) ↦ extend f g e') g₂)
⊢ g₁ = g₂

Tactic:
funext fun x ↦ ?_

Premises used: funext
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : Eq (α := β → γ) ((fun (g : α → γ) ↦ extend f g e') g₁) ((fun (g : α → γ) ↦ extend f g e') g₂)
refine : ∀ (x : α), g₁ x = g₂ x
⊢ g₁ = g₂

Tactic:
refine funext fun x ↦ ?_

Premises used: funext
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : Eq (α := β → γ) ((fun (g : α → γ) ↦ extend f g e') g₁) ((fun (g : α → γ) ↦ extend f g e') g₂)
x : α
⊢ Eq.{u_3} (α := γ) ((fun (g : α → γ) ↦ extend f g e') g₁ (f x)) ((fun (g : α → γ) ↦ extend f g e') g₂ (f x))

Tactic:
have H := congr_fun hg (f x)
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : Eq (α := β → γ) ((fun (g : α → γ) ↦ extend f g e') g₁) ((fun (g : α → γ) ↦ extend f g e') g₂)
x : α
H : Eq.{u_3} (α := γ) ((fun (g : α → γ) ↦ extend f g e') g₁ (f x)) ((fun (g : α → γ) ↦ extend f g e') g₂ (f x))
⊢ g₁ x = g₂ x

Tactic:
simp only [hf.extend_apply] at H

Premises used: Function.Injective.extend_apply
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : Eq (α := β → γ) ((fun (g : α → γ) ↦ extend f g e') g₁) ((fun (g : α → γ) ↦ extend f g e') g₂)
x : α
H : g₁ x = g₂ x
⊢ g₁ x = g₂ x

Tactic:
H
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : Eq (α := β → γ) ((fun (g : α → γ) ↦ extend f g e') g₁) ((fun (g : α → γ) ↦ extend f g e') g₂)
x : α
H : g₁ x = g₂ x
⊢ g₁ x = g₂ x

Tactic:
exact H
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
hf : FactorsThrough g f
⊢ extend f g e' ∘ f = g

Tactic:
funext fun a => hf.extend_apply e' a

Premises used: Function.FactorsThrough.extend_apply, funext
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
c : γ
⊢ Eq (α := β → γ) (extend f (fun (x : α) ↦ c) fun (x : β) ↦ c) fun (x : β) ↦ c

Tactic:
funext fun _ ↦ open scoped Classical in ite_id _

Premises used: ite_id, funext
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
g : α → γ
e' : β → γ
⊢ extend f g e' ∘ f = g

Tactic:
funext fun a ↦ hf.extend_apply g e' a

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

Tactic:
fun g ↦ ⟨extend f g g₀, Function.extend_comp hf _ _⟩

Premises used: Function.extend, Function.extend_comp, Exists.intro, Function.Surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
inst : Nonempty γ
hf : Injective f
⊢ Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f

Tactic:
hf.surjective_comp_right' fun _ ↦ Classical.choice ‹_›

Premises used: Classical.choice, Function.Injective.surjective_comp_right'
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f

Tactic:
⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩

Premises used: Function.Injective.surjective_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_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f

Tactic:
refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_inj : ¬Injective f
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
⊢ ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1

Tactic:
simp only [Injective, not_forall] at not_inj

Premises used: Function.Injective, Classical.not_forall
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1
have : ∀ (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂), c = c'
⊢ c = c'

Tactic:
have ⟨a₁, a₂, eq, ne⟩ := not_inj
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1
a₁ a₂ : α
eq : f a₁ = f a₂
ne : ¬a₁ = a₂
have :
  ∀ (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c'), c = c'
⊢ c = c'

Tactic:
have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
⊢ (fun (g : β → γ) ↦ g ∘ f_1) f a₁ = if a₁ = a₂ then c else c'

Tactic:
have h₁ := congr_fun hf a₁
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : (fun (g : β → γ) ↦ g ∘ f_1) f a₁ = if a₁ = a₂ then c else c'
⊢ (fun (g : β → γ) ↦ g ∘ f_1) f a₂ = if a₂ = a₂ then c else c'

Tactic:
have h₂ := congr_fun hf a₂
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : (fun (g : β → γ) ↦ g ∘ f_1) f a₁ = if a₁ = a₂ then c else c'
h₂ : (fun (g : β → γ) ↦ g ∘ f_1) f a₂ = if a₂ = a₂ then c else c'
⊢ f (f_1 a₁) = c'

Tactic:
simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂

Premises used: reduceIte, Function.comp_apply, if_neg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : (fun (g : β → γ) ↦ g ∘ f_1) f a₁ = if a₁ = a₂ then c else c'
h₂ : (fun (g : β → γ) ↦ g ∘ f_1) f a₂ = if a₂ = a₂ then c else c'
h₃ : f (f_1 a₁) = c'
⊢ f (f_1 a₂) = c

Tactic:
simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂

Premises used: reduceIte, Function.comp_apply, if_neg
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : f (f_1 a₁) = c'
h₂ : f (f_1 a₂) = c
rw : c = f (f_1 a₁)
rw₁ : c = f (f_1 a₂)
rw₂ rw₃ : c = c
⊢ c = c'

Tactic:
rw [← h₁, eq, h₂]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
refine : ∀ (not_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
refine₁ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1), c = c'
refine₂ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂),
    c = c'
refine₃ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c'), c = c'
refine₄ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c')
    (h₁ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₁ = if a₁ = a₂ then c else c'), c = c'
refine₅ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c')
    (h₁ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₁ = if a₁ = a₂ then c else c')
    (h₂ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₂ = if a₂ = a₂ then c else c'), c = c'
refine₆ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c')
    (h₁ : f_1 (f a₁) = c') (h₂ : f_1 (f a₂) = c), c = c'
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f

Tactic:
classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]

Premises used: reduceIte, Function.comp_apply, Function.Injective, Classical.not_forall
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : α → γ
⊢ (fun (g : β → γ) ↦ g ∘ f) (g ∘ surjInv ⋯) = g

Tactic:
simp only [comp_assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp_id]

Premises used: Function.comp_id, Function.LeftInverse.comp_eq_id, Function.leftInverse_surjInv, Function.comp_assoc
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
⊢ FactorsThrough f f

Tactic:
fun _ _ ↦ id

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

Tactic:
fun _x _y hxy ↦
  congr_arg g' (h hxy)

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

Tactic:
fun _x _y hxy ↦
  h hxy

Premises used: Function.FactorsThrough
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Sort u_3
f : α → β → γ
⊢ uncurry f = fun (p : α × β) ↦ f p.fst p.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Sort u_3
⊢ Injective (α := α → β → γ) uncurry

Tactic:
LeftInverse.injective curry_uncurry

Premises used: Function.LeftInverse.injective, Function.curry_uncurry
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Sort u_3
⊢ Injective (α := α × β → γ) curry

Tactic:
LeftInverse.injective uncurry_curry

Premises used: Function.LeftInverse.injective, Function.uncurry_curry
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Sort u_3
f : α → β → γ
⊢ uncurry (flip f) = uncurry f ∘ Prod.swap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Sort u_3
f : α × β → γ
⊢ flip (curry f) = curry (f ∘ Prod.swap)

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
h :
  ∀ (a : α) (a' : α'),
    curry (update (β := fun (a : α × α') ↦ β) f aa' b) a a' =
      update (β := fun (a : α) ↦ α' → β) (curry f) aa'.fst (update (β := fun (a : α') ↦ β) (curry f aa'.fst) aa'.snd b)
        a a'
⊢ curry (update (β := fun (a : α × α') ↦ β) f aa' b) =
    update (β := fun (a : α) ↦ α' → β) (curry f) aa'.fst (update (β := fun (a : α') ↦ β) (curry f aa'.fst) aa'.snd b)

Tactic:
ext a a'
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
h :
  ∀ (a₂ : α) (a₂' : α'),
    curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
      update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
        (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
⊢ curry (update (β := fun (a : α × α') ↦ β) f aa' b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) aa'.fst (update (β := fun (a : α') ↦ β) (curry f aa'.fst) aa'.snd b) a
      a'

Tactic:
let ⟨a₂, a₂'⟩ := aa'
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
h :
  curry (update (β := fun (a : α × α') ↦ β) f (a, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a₂').fst) (a, a₂').snd b) a a'
h₁ :
  ∀ (ha : a ≠ a₂),
    curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
      update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
        (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'

Tactic:
obtain rfl | ha := eq_or_ne a a₂

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
h :
  curry (update (β := fun (a : α × α') ↦ β) f (a, a') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a').fst) (a, a').snd b) a a'
h₁ :
  ∀ (ha' : a' ≠ a₂'),
    curry (update (β := fun (a : α × α') ↦ β) f (a, a₂') b) a a' =
      update (β := fun (a : α) ↦ α' → β) (curry f) (a, a₂').fst
        (update (β := fun (a : α') ↦ β) (curry f (a, a₂').fst) (a, a₂').snd b) a a'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a₂').fst) (a, a₂').snd b) a a'

Tactic:
obtain rfl | ha' := eq_or_ne a' a₂'

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
h :
  curry (update (β := fun (a : α × α') ↦ β) f (a₂, a') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a').fst) (a₂, a').snd b) a a'
h₁ :
  ∀ (ha' : a' ≠ a₂'),
    curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
      update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
        (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'

Tactic:
obtain rfl | ha' := eq_or_ne a' a₂'

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a, a') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a').fst) (a, a').snd b) a a'

Tactic:
simp [*]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
ha' : a' ≠ a₂'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a₂').fst) (a, a₂').snd b) a a'

Tactic:
simp [*]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
ha : a ≠ a₂
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a₂, a') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a').fst) (a₂, a').snd b) a a'

Tactic:
simp [*]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
ha' : a' ≠ a₂'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'

Tactic:
simp [*]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α → α' → β
a : α
a' : α'
b : β
a₁ :
  curry (uncurry (update (β := fun (a : α) ↦ α' → β) f a (update (β := fun (a : α') ↦ β) (f a) a' b))) =
    curry (update (β := fun (a : α × α') ↦ β) (uncurry f) (a, a') b)
⊢ uncurry (update (β := fun (a : α) ↦ α' → β) f a (update (β := fun (a : α') ↦ β) (f a) a' b)) =
    update (β := fun (a : α × α') ↦ β) (uncurry f) (a, a') b

Tactic:
apply curry_injective

Premises used: Function.curry_injective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α → α' → β
a : α
a' : α'
b : β
⊢ curry (uncurry (update (β := fun (a : α) ↦ α' → β) f a (update (β := fun (a : α') ↦ β) (f a) a' b))) =
    curry (update (β := fun (a : α × α') ↦ β) (uncurry f) (a, a') b)

Tactic:
simp [curry_update]

Premises used: Function.curry_update
-- Module: Mathlib.Logic.Function.Basic
Goal:
⊢ Involutive not

Tactic:
Bool.not_not

Premises used: Bool.not_not, Function.Involutive
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
f : α → α
h : Involutive f
⊢ f ∘ f = id

Tactic:
funext h

Premises used: funext
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
f : α → α
h : Involutive f
⊢ LeftInverse f f

Tactic:
h

Premises used: Function.LeftInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
rw : g (f (f x)) = f (f (f x))
rw₁ : f x = f (f (f x))
rw₂ rw₃ : f x = f x
⊢ g x = f x

Tactic:
rw [← h x, hg, h]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
f : α → α
h : Involutive f
⊢ RightInverse f f

Tactic:
h

Premises used: Function.LeftInverse, Function.RightInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
f : α → α
h : Involutive f
⊢ Injective f

Tactic:
h.leftInverse.injective

Premises used: Function.LeftInverse.injective, Function.Involutive.leftInverse
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
f : α → α
h : Involutive f
⊢ Surjective f

Tactic:
fun x ↦ ⟨f x, h x⟩

Premises used: Exists.intro, Function.Surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
f : α → α
h : Involutive f
⊢ Bijective f

Tactic:
⟨h.injective, h.surjective⟩

Premises used: Function.Involutive.surjective, Function.Involutive.injective, And.intro, Function.Bijective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
f : α → α
h : Involutive f
P : Prop
inst : Decidable P
x : α
rw : (if P then f x else f (f x)) = if ¬P then x else f x
rw₁ : (if P then f x else x) = if ¬P then x else f x
rw₂ rw₃ : (if P then f x else x) = if P then f x else x
⊢ f (if P then x else f x) = if ¬P then x else f x

Tactic:
rw [apply_ite f, h, ite_not]

Premises used: apply_ite, ite_not
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
f : α → α
h : Involutive f
x y : α
⊢ f x = y ↔ x = f y

Tactic:
h.injective.eq_iff' (h y)

Premises used: Function.Injective.eq_iff', Function.Involutive.injective
-- Module: Mathlib.Logic.Function.Basic
Goal:
⊢ Involutive Not

Tactic:
fun _ ↦ propext not_not

Premises used: Classical.not_not, propext, Function.Involutive
-- Module: Mathlib.Logic.Function.Basic
Goal:
⊢ Injective Not

Tactic:
not_involutive.injective

Premises used: Function.not_involutive, Function.Involutive.injective
-- Module: Mathlib.Logic.Function.Basic
Goal:
⊢ Surjective Not

Tactic:
not_involutive.surjective

Premises used: Function.not_involutive, Function.Involutive.surjective
-- Module: Mathlib.Logic.Function.Basic
Goal:
⊢ Bijective Not

Tactic:
not_involutive.bijective

Premises used: Function.not_involutive, Function.Involutive.bijective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
f : α → α
⊢ (Symmetric fun (x1 x2 : α) ↦ f x1 = x2) ↔ Involutive f

Tactic:
simp [Symmetric, Involutive]

Premises used: Symmetric, Function.Involutive
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
hf : Injective2 f
b : β
⊢ Injective.{u_1, u_3} (β := γ) fun (a : α) ↦ f a b

Tactic:
fun _ _ h ↦ (hf h).left

Premises used: And.left, Function.Injective