awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
hf : Injective2 f
a : α
⊢ Injective (f a)

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

Premises used: And.right, Function.Injective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
f : α → β → γ
hf : Injective2 f
⊢ Injective (uncurry f)

Tactic:
fun ⟨_, _⟩ ⟨_, _⟩ h ↦ (hf h).elim (congr_arg₂ _)

Premises used: Prod.mk, And.elim, Function.Injective, Eq, _private.0.Function.Injective2.uncurry.match_2, _private.0.Function.Injective2.uncurry.match_1, congr_arg₂
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
hf : Injective2 f
inst : Nonempty β
⊢ Injective f

Tactic:
fun _ _ h ↦
  let ⟨b⟩ := ‹Nonempty β›
  hf.left b <| (congr_fun h b :)

Premises used: _private.0.Function.const_injective.match_1, Function.Injective, congr_fun, Eq, Function.Injective2.left
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
hf : Injective2 f
inst : Nonempty α
⊢ Injective (β := (a : α) → γ) fun (b : β) (a : α) ↦ f a b

Tactic:
fun _ _ h ↦
    let ⟨a⟩ := ‹Nonempty α›
    hf.right a <| (congr_fun h a :)

Premises used: _private.0.Function.const_injective.match_1, Function.Injective2.right, Function.Injective, congr_fun, Eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
hf : Injective2 f
a₁ a₂ : α
b₁ b₂ : β
⊢ f a₁ b₁ = f a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
⟨fun h ↦ hf h, fun ⟨h1, h2⟩ ↦ congr_arg₂ f h1 h2⟩

Premises used: Iff.intro, _private.0.Function.Injective2.eq_iff.match_1, Eq, congr_arg₂
-- Module: Mathlib.Logic.Function.Basic
Goal:
p : Prop
α : Sort u_1
inst : Nonempty α
f : p → α
a : p
⊢ sometimes f = f a

Tactic:
dif_pos ⟨a⟩

Premises used: dif_pos, Function.sometimes
-- Module: Mathlib.Logic.Function.Basic
Goal:
p : Prop
α : Sort u_1
inst : Nonempty α
P : α → Prop
f : p → α
a : p
h rwa : P (f a)
a₁ : p
rwa₁ : P (f a)
a₂ : p
rwa₂ : P (f a)
a₃ : p
rwa₃ : P (f a)
a₄ : p
⊢ P (sometimes f)

Tactic:
rwa [sometimes_eq]

Premises used: Function.sometimes_eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b : β, r a b) ↔ ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b

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

Premises used: Iff.intro
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
refine_1 : ∀ (h : ∀ (a : α), ∃! b : β, r a b), ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b
refine_2 : (∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b) → ∀ (a : α), ∃! b : β, r a b
⊢ (∀ (a : α), ∃! b : β, r a b) ↔ ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b : β, r a b
⊢ ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩

Premises used: Eq.rec, Iff.intro, Exists.intro, Exists.choose
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b : β, r a b
refine_1 :
  ∀ {a : α} {b : β} (hr : r a b),
    (fun (a : α) ↦
          Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) ⋯)
        a =
      b
refine_1₁ :
  ∀ {a : α} {b : β}
    (h' :
      (fun (a : α) ↦
            Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) ⋯)
          a =
        b),
    r a
      ((fun (a : α) ↦
          Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) ⋯)
        a)
⊢ ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b : β, r a b
a : α
b : β
hr : r a b
⊢ (fun (a : α) ↦
        Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) ⋯)
      a =
    b

Tactic:
((h _).choose_spec.2 _ hr).symm

Premises used: Exists.choose_spec, And.right, Eq.symm
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b : β, r a b
a : α
b : β
h' :
  (fun (a : α) ↦
        Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) ⋯)
      a =
    b
⊢ r a
    ((fun (a : α) ↦
        Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) ⋯)
      a)

Tactic:
(h _).choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b : β, r a b
a : α
b : β
hr : r a b
⊢ (fun (a : α) ↦
        Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) ⋯)
      a =
    b

Tactic:
exacts [((h _).choose_spec.2 _ hr).symm, (h _).choose_spec.1]

Premises used: Exists.choose_spec, And.right, And.left, Eq.symm
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
f : α → β
hf : ∀ {a : α} {b : β}, r a b ↔ f a = b
⊢ ∀ (a : α), ∃! b : β, r a b

Tactic:
simp [hf]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b : β, r a b) ↔ ∃ (f : α → β), r = fun (x1 : α) (x2 : β) ↦ f x1 = x2

Tactic:
simp [forall_existsUnique_iff, funext_iff]

Premises used: funext_iff, forall_existsUnique_iff
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
⊢ (∀ (a : α), ∃! b : α, r a b) ↔ ∃ (f : α → α), Involutive f ∧ Eq.{max 1 u_1} r fun (x1 x2 : α) ↦ f x1 = x2

Tactic:
⟨fun h ↦ ?_, fun ⟨f, _, hf⟩ ↦ forall_existsUnique_iff'.2 ⟨f, hf⟩⟩

Premises used: Iff.mpr, _private.0.Symmetric.forall_existsUnique_iff'.match_1, Iff.intro, Exists.intro, forall_existsUnique_iff'
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
refine : ∀ (h : ∀ (a : α), ∃! b : α, r a b), ∃ (f : α → α), Involutive f ∧ Eq.{max 1 u_1} r fun (x1 x2 : α) ↦ f x1 = x2
⊢ (∀ (a : α), ∃! b : α, r a b) ↔ ∃ (f : α → α), Involutive f ∧ Eq.{max 1 u_1} r fun (x1 x2 : α) ↦ f x1 = x2

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨f, _, hf⟩ ↦ forall_existsUnique_iff'.2 ⟨f, hf⟩⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
h : ∀ (a : α), ∃! b : α, r a b
rcases :
  ∀ (f : α → α) (hr : Symmetric fun (x1 x2 : α) ↦ f x1 = x2)
    (h : ∀ (a : α), ∃! b : α, (fun (x1 x2 : α) ↦ f x1 = x2) a b),
    ∃ (f_1 : α → α),
      Involutive f_1 ∧ Eq.{max 1 u_1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ f x1 = x2) fun (x1 x2 : α) ↦ f_1 x1 = x2
⊢ ∃ (f : α → α), Involutive f ∧ Eq.{max 1 u_1} r fun (x1 x2 : α) ↦ f x1 = x2

Tactic:
rcases forall_existsUnique_iff'.1 h with ⟨f, rfl : r = _⟩

Premises used: Iff.mp, forall_existsUnique_iff', rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
f : α → α
hr : Symmetric fun (x1 x2 : α) ↦ f x1 = x2
h : ∀ (a : α), ∃! b : α, (fun (x1 x2 : α) ↦ f x1 = x2) a b
⊢ ∃ (f_1 : α → α),
    Involutive f_1 ∧ Eq.{max 1 u_1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ f x1 = x2) fun (x1 x2 : α) ↦ f_1 x1 = x2

Tactic:
⟨f, symmetric_apply_eq_iff.1 hr, rfl⟩

Premises used: And.intro, Exists.intro, Iff.mp, Function.symmetric_apply_eq_iff, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
f : α → α
hr : Symmetric fun (x1 x2 : α) ↦ f x1 = x2
h : ∀ (a : α), ∃! b : α, (fun (x1 x2 : α) ↦ f x1 = x2) a b
⊢ ∃ (f_1 : α → α),
    Involutive f_1 ∧ Eq.{max 1 u_1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ f x1 = x2) fun (x1 x2 : α) ↦ f_1 x1 = x2

Tactic:
exact ⟨f, symmetric_apply_eq_iff.1 hr, rfl⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
⊢ (∀ (a : α), ∃! b : α, r a b) ↔ ∃ (f : α → α), Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b

Tactic:
simp [hr.forall_existsUnique_iff', funext_iff]

Premises used: funext_iff, Symmetric.forall_existsUnique_iff'
-- Module: Mathlib.Logic.Function.Basic
Goal:
α β : Sort u_3
h : α = β
refl : Bijective ⋯.mp
⊢ Bijective h.mp

Tactic:
cases h
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_3
⊢ Bijective ⋯.mp

Tactic:
⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Premises used: id, And.intro, Exists.intro, Function.Bijective, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_3
⊢ Bijective ⋯.mp

Tactic:
exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α β : Sort u_3
h : α = β
refl : Bijective ⋯.mpr
⊢ Bijective h.mpr

Tactic:
cases h
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_3
⊢ Bijective ⋯.mpr

Tactic:
⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Premises used: id, And.intro, Exists.intro, Function.Bijective, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_3
⊢ Bijective ⋯.mpr

Tactic:
exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α β : Sort u_3
h : α = β
refl : Bijective (cast ⋯)
⊢ Bijective (cast h)

Tactic:
cases h
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_3
⊢ Bijective (cast ⋯)

Tactic:
⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Premises used: id, And.intro, Exists.intro, Function.Bijective, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_3
⊢ Bijective (cast ⋯)

Tactic:
exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
a a' : α
h : a = a'
C : α → Type u_3
x y : C a
⊢ Eq.ndrec (motive := C) x h = Eq.ndrec (motive := C) y h ↔ x = y

Tactic:
(eq_rec_on_bijective h).injective.eq_iff

Premises used: Function.Injective.eq_iff, Function.Bijective.injective, eq_rec_on_bijective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α β : Type u
h : α = β
x y : α
⊢ cast h x = cast h y ↔ x = y

Tactic:
(cast_bijective h).injective.eq_iff

Premises used: Function.Injective.eq_iff, Function.Bijective.injective, cast_bijective
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
rw rw₁ : C a ≍ C a
⊢ HEq (α := γ (f (g (f a)))) (C (g (f a))) (C a)

Tactic:
rw [h]
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ Eq.recOn (motive := fun (x : β) (x_1 : f (g (f a)) = x) ↦ γ x) ⋯ (C (g (f a))) = C a

Tactic:
h.eq_rec_eq _ _

Premises used: Function.LeftInverse.eq_rec_eq
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ cast (α := (fun (a : α) ↦ γ (f a)) (g (f a))) ⋯ (C (g (f a))) = C a

Tactic:
grind
-- Module: Mathlib.Logic.Function.Basic
Goal:
α : Sort u
β : Sort v
r : β → β → Prop
f : α → β
h : Equivalence r
⊢ Equivalence (InvImage r f)

Tactic:
⟨fun _ ↦ h.1 _, h.symm, h.trans⟩

Premises used: Equivalence.symm, Equivalence.refl, Equivalence.trans, Equivalence.mk
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
⊢ Eq (α := ((i : ι) → α i) → (i : ι) → α i) (Pi.map (α := α) (β := α) fun (i : ι) ↦ id) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
⊢ Eq (α := ((i : ι) → α i) → (i : ι) → α i) (Pi.map (α := α) (β := α) fun (i : ι) (a : α i) ↦ a)
    fun (x : (i : ι) → α i) ↦ x

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Function.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
γ : ι → Type u_6
f : (i : ι) → α i → β i
g : (i : ι) → β i → γ i
⊢ Pi.map (α := β) (β := γ) g ∘ Pi.map (α := α) (β := β) f = Pi.map (α := α) (β := γ) fun (i : ι) ↦ g i ∘ f i

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Function.Coequalizer
Goal:
α : Type u_1
β : Type u_2
f g : α → β
x : α
⊢ mk f g (f x) = mk f g (g x)

Tactic:
Quot.sound (.intro x)

Premises used: Quot.sound, Function.Coequalizer.mk, Function.Coequalizer, Function.Coequalizer.Rel.intro
-- Module: Mathlib.Logic.Function.Coequalizer
Goal:
α : Type u_1
β : Type u_2
f g : α → β
⊢ Surjective (mk f g)

Tactic:
Quot.exists_rep

Premises used: Quot.exists_rep, Function.Coequalizer.mk, Function.Coequalizer, Function.Surjective
-- Module: Mathlib.Logic.Function.Coequalizer
Goal:
α : Type u_1
β : Type u_2
f g : α → β
γ : Type u_3
u : β → γ
hu : u ∘ f = u ∘ g
x : β
⊢ desc f g u hu (mk f g x) = u x

Tactic:
rfl

Premises used: Function.Coequalizer.desc, rfl
-- Module: Mathlib.Logic.Function.CompTypeclasses
Goal:
N : Type u_1
P : Type u_2
φ : N → N
inst : IsId φ
ψ : N → P
⊢ ψ ∘ φ = ψ

Tactic:
simp only [IsId.eq_id, Function.comp_id]

Premises used: Function.comp_id, CompTriple.IsId.eq_id
-- Module: Mathlib.Logic.Function.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
φ : M → N
ψ : N → N
inst : IsId ψ
⊢ ψ ∘ φ = φ

Tactic:
simp only [IsId.eq_id, Function.id_comp]

Premises used: CompTriple.IsId.eq_id, Function.id_comp
-- Module: Mathlib.Logic.Function.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
φ : M → N
ψ : N → M
h : Function.RightInverse φ ψ
χ : M → M
inst : IsId χ
⊢ ψ ∘ φ = χ

Tactic:
simp only [IsId.eq_id, h.id]

Premises used: Function.RightInverse.id, CompTriple.IsId.eq_id
-- Module: Mathlib.Logic.Function.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
φ : M → N
ψ : N → P
χ : M → P
h : CompTriple φ ψ χ
x : M
rw : ψ (φ x) = (ψ ∘ φ) x
rw₁ rw₂ : ψ (φ x) = ψ (φ x)
⊢ ψ (φ x) = χ x

Tactic:
rw [← h.comp_eq, Function.comp_apply]

Premises used: CompTriple.comp_eq, Function.comp_apply
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
⊢ Semiconj f ga gb ↔ f ∘ ga = gb ∘ f

Tactic:
funext_iff.symm

Premises used: funext_iff, Function.Semiconj, Iff.symm
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
h : Semiconj f ga gb
x : α
⊢ f (ga x) = gb (f x)

Tactic:
h x
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
h' : Semiconj f ga' gb'
x : α
⊢ f ((ga ∘ ga') x) = (gb ∘ gb') (f x)

Tactic:
simp only [comp_apply, h.eq, h'.eq]

Premises used: Function.Semiconj.eq, Function.comp_apply
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
fab : α → β
fbc : β → γ
ga : α → α
gb : β → β
gc : γ → γ
hab : Semiconj fab ga gb
hbc : Semiconj fbc gb gc
x : α
⊢ (fbc ∘ fab) (ga x) = gc ((fbc ∘ fab) x)

Tactic:
simp only [comp_apply, hab.eq, hbc.eq]

Premises used: Function.Semiconj.eq, Function.comp_apply
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
fab : α → β
fbc : β → γ
ga : α → α
gb : β → β
gc : γ → γ
hbc : Semiconj fbc gb gc
hab : Semiconj fab ga gb
⊢ Semiconj (fbc ∘ fab) ga gc

Tactic:
hab.trans hbc

Premises used: Function.Semiconj.trans
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Semiconj f id id

Tactic:
fun _ ↦ rfl

Premises used: Function.Semiconj, rfl
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
ga : α → α
⊢ Semiconj id ga ga

Tactic:
fun _ ↦ rfl

Premises used: Function.Semiconj, rfl
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
rw : gb' (gb (f (ga' x))) = gb' (f x)
rw₁ : gb' (f (ga (ga' x))) = gb' (f x)
rw₂ rw₃ : gb' (f x) = gb' (f x)
⊢ f (ga' x) = gb' (f x)

Tactic:
rw [← hb (f (ga' x)), ← h.eq, ha x]

Premises used: Function.Semiconj.eq
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
rw : f (f' (gb x)) = f (ga (f' x))
rw₁ : f (f' (gb x)) = gb (f (f' x))
rw₂ : gb x = gb (f (f' x))
rw₃ rw₄ : gb x = gb x
⊢ f' (gb x) = ga (f' x)

Tactic:
rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]

Premises used: Function.LeftInverse.injective, Function.Injective.eq_iff
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
f g : α → α
h : Semiconj f g g
⊢ Commute f g

Tactic:
h

Premises used: Function.Commute
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
f g : α → α
h : Commute f g
⊢ Semiconj f g g

Tactic:
h

Premises used: Function.Commute
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
f : α → α
⊢ Commute f f

Tactic:
fun _ ↦ Eq.refl _

Premises used: Function.Commute, Eq.refl, Function.Semiconj
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
f g : α → α
h : Commute f g
⊢ Commute g f

Tactic:
fun x ↦ (h x).symm

Premises used: Function.Commute, Function.Semiconj, Eq.symm
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
f g g' : α → α
h : Commute f g
h' : Commute f g'
⊢ Commute f (g ∘ g')

Tactic:
Semiconj.comp_right h h'

Premises used: Function.Commute, Function.Semiconj.comp_right
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
f f' g : α → α
h : Commute f g
h' : Commute f' g
⊢ Commute (f ∘ f') g

Tactic:
h.comp_left h'

Premises used: Function.Commute, Function.Semiconj.comp_left
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
f : α → α
⊢ Commute f id

Tactic:
Semiconj.id_right

Premises used: Function.Commute, Function.Semiconj.id_right
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
f : α → α
⊢ Commute id f

Tactic:
Semiconj.id_left

Premises used: Function.Commute, Function.Semiconj.id_left
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
f g : α → α
h : Commute f g
⊢ Commute (Option.map f) (Option.map g)

Tactic:
h.option_map

Premises used: Function.Semiconj.option_map, Function.Commute
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
h : Semiconj₂ f ga gb
x y : α
⊢ f (ga x y) = gb (f x) (f y)

Tactic:
h x y
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
h : Semiconj₂ f ga gb
⊢ bicompr f ga = bicompl gb f f

Tactic:
funext fun x ↦ funext <| h x

Premises used: funext
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
op : α → α → α
⊢ Semiconj₂ id op op

Tactic:
fun _ _ ↦ rfl

Premises used: Function.Semiconj₂, rfl
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
f' : β → γ
gc : γ → γ → γ
hf' : Semiconj₂ f' gb gc
hf : Semiconj₂ f ga gb
x y : α
⊢ (f' ∘ f) (ga x y) = gc ((f' ∘ f) x) ((f' ∘ f) y)

Tactic:
simp only [hf'.eq, hf.eq, comp_apply]

Premises used: Function.comp_apply, Function.Semiconj₂.eq
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst : Std.Associative ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x₁ x₂ x₃ : α
⊢ gb (gb (f x₁) (f x₂)) (f x₃) = gb (f x₁) (gb (f x₂) (f x₃))

Tactic:
simp only [← h.eq, Std.Associative.assoc (op := ga)]

Premises used: Std.Associative.assoc, Function.Semiconj₂.eq
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst : Std.Associative gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x₁ x₂ x₃ : α
⊢ f (ga (ga x₁ x₂) x₃) = f (ga x₁ (ga x₂ x₃))

Tactic:
simp only [h.eq, Std.Associative.assoc (op := gb)]

Premises used: Std.Associative.assoc, Function.Semiconj₂.eq
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst : Std.IdempotentOp ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x : α
⊢ gb (f x) (f x) = f x

Tactic:
simp only [← h.eq, Std.IdempotentOp.idempotent (op := ga)]

Premises used: Std.IdempotentOp.idempotent, Function.Semiconj₂.eq
-- Module: Mathlib.Logic.Function.Conjugate
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
rw : gb (f x) (f x) = f x
rw₁ rw₂ : f x = f x
⊢ f (ga x x) = f x

Tactic:
rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]

Premises used: Std.IdempotentOp.idempotent, Function.Semiconj₂.eq
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Sort u₁
β : Sort u₂
φ : Sort u₃
f : α → β → φ
⊢ flip f = fun (b : β) (a : α) ↦ f a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Defs
Goal:
ι : Sort u_3
α : ι → Type u_1
β : ι → Type u_2
f : (i : ι) → α i
g : (i : ι) → β i
i : ι
⊢ Function.prod (α := α) (β := β) f g i = (f i, g i)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := (i : α × β) → α × β)
    (Function.prod (α := fun (self : α × β) ↦ α) (β := fun (self : α × β) ↦ β) Prod.fst Prod.snd) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := (i : α × β) → β × α)
    (Function.prod (α := fun (self : α × β) ↦ β) (β := fun (self : α × β) ↦ α) Prod.snd Prod.fst) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Sort u₁
β : Sort u₂
φ : α → β → Sort u₃
f : (x : α) → (y : β) → φ x y
⊢ swap (φ := φ) f = fun (y : β) (x : α) ↦ f x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Sort u₁
β : Sort u₂
φ : Sort u₃
f : β → β → φ
g : α → β
⊢ (swap (φ := fun (a a_1 : β) ↦ φ) f on g) = swap (φ := fun (a a_1 : α) ↦ φ) (f on g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Sort u₁
β : Sort u₂
φ : Sort u₃
δ : Sort u₄
f : φ → δ
g : β → φ
h : α → β
⊢ (f ∘ g) ∘ h = f ∘ g ∘ h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Sort u₁
⊢ Bijective.{u₁, u₁} (α := α) id

Tactic:
⟨injective_id, surjective_id⟩

Premises used: Function.injective_id, Function.surjective_id, And.intro, Function.Bijective
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
I : Injective f
a b : α
pos : ∀ (h : (a == b) = true), (f a == f b) = (a == b)
neg : ∀ (h : ¬(a == b) = true), (f a == f b) = (a == b)
⊢ (f a == f b) = (a == b)

Tactic:
by_cases h : a == b
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : (a == b) = true
pos : f a = f b
⊢ (f a == f b) = (a == b)

Tactic:
simp [h]
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : ¬(a == b) = true
neg : ¬f a = f b
⊢ (f a == f b) = (a == b)

Tactic:
simp [h]
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : (a == b) = true
⊢ f a = f b

Tactic:
simpa [I.eq_iff] using h

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ ¬f a = f b

Tactic:
simpa [I.eq_iff] using h

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u_6
β : Type u_7
γ : Sort u_8
δ : Sort u_9
f : α → β → γ
g : γ → δ
⊢ uncurry (g ∘₂ f) = g ∘ uncurry f

Tactic:
rfl

Premises used: Function.bicompr, rfl
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
ε : Sort u_10
f : γ → δ → ε
g : α → γ
h : β → δ
⊢ uncurry (bicompl f g h) = uncurry f ∘ Prod.map g h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u₁
f : α → α
x : α
hf : IsFixedPt f x
⊢ f x = x

Tactic:
hf

Premises used: Function.IsFixedPt
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u₁
inst : Subsingleton α
f : α → α
x : α
⊢ IsFixedPt f x

Tactic:
Subsingleton.elim _ _

Premises used: Function.IsFixedPt, Subsingleton.elim
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u₁
x : α
⊢ IsFixedPt id x

Tactic:
rfl

Premises used: Function.IsFixedPt, rfl