awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P ((e.symm : (a : β) → α) b)
b' : β
h :
  ∀ (x : P ((e.symm : (a : β) → α) b')),
    Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
      ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
          (update (β := P) f ((e.symm : (a : β) → α) b') x) b' :
        P ((e.symm : (a : β) → α) b'))
      (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
          ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b' x b' :
        P ((e.symm : (a : β) → α) b'))
h₁ :
  ∀ (h : b' ≠ b),
    Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
      ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
          (update (β := P) f ((e.symm : (a : β) → α) b) x) b' :
        P ((e.symm : (a : β) → α) b'))
      (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
          ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b x b' :
        P ((e.symm : (a : β) → α) b'))
⊢ Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
    ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
        (update (β := P) f ((e.symm : (a : β) → α) b) x) b' :
      P ((e.symm : (a : β) → α) b'))
    (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
        ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b x b' :
      P ((e.symm : (a : β) → α) b'))

Tactic:
rcases eq_or_ne b' b with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b' : β
x : P ((e.symm : (a : β) → α) b')
⊢ Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
    ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
        (update (β := P) f ((e.symm : (a : β) → α) b') x) b' :
      P ((e.symm : (a : β) → α) b'))
    (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
        ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b' x b' :
      P ((e.symm : (a : β) → α) b'))

Tactic:
simp_all
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P ((e.symm : (a : β) → α) b)
b' : β
h : b' ≠ b
⊢ Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
    ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
        (update (β := P) f ((e.symm : (a : β) → α) b) x) b' :
      P ((e.symm : (a : β) → α) b'))
    (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
        ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b x b' :
      P ((e.symm : (a : β) → α) b'))

Tactic:
simp_all
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (b : β) → P ((e.symm : (a : β) → α) b)
b : β
x : P ((e.symm : (a : β) → α) b)
⊢ Eq (α := (a : α) → P a)
    (((Equiv.piCongrLeft' P e).symm : (a : (b : β) → P ((e.symm : (a : β) → α) b)) → (a : α) → P a)
        (update (β := fun (b : β) ↦ P ((e.symm : (a : β) → α) b)) f b x) :
      (a : α) → P a)
    (update (β := P) (((Equiv.piCongrLeft' P e).symm : (a : (b : β) → P ((e.symm : (a : β) → α) b)) → (a : α) → P a) f)
        ((e.symm : (a : β) → α) b) x :
      (a : α) → P a)

Tactic:
simp [(e.piCongrLeft' P).symm_apply_eq, piCongrLeft'_update]

Premises used: Equiv.symm_apply_eq, Function.piCongrLeft'_update, Equiv.piCongrLeft'
-- Module: Mathlib.Logic.Equiv.Bool
Goal:
⊢ Bijective not

Tactic:
Equiv.boolNot.bijective

Premises used: Equiv.bijective, Equiv.boolNot
-- Module: Mathlib.Logic.Equiv.Bool
Goal:
⊢ Injective not

Tactic:
Equiv.boolNot.injective

Premises used: Equiv.injective, Equiv.boolNot
-- Module: Mathlib.Logic.Equiv.Bool
Goal:
⊢ Surjective not

Tactic:
Equiv.boolNot.surjective

Premises used: Equiv.surjective, Equiv.boolNot
-- Module: Mathlib.Logic.Equiv.Bool
Goal:
⊢ LeftInverse not not

Tactic:
not_not

Premises used: Function.LeftInverse, Bool.not_not
-- Module: Mathlib.Logic.Equiv.Bool
Goal:
⊢ RightInverse not not

Tactic:
not_not

Premises used: Function.LeftInverse, Bool.not_not, Function.RightInverse
-- Module: Mathlib.Logic.Equiv.Bool
Goal:
⊢ HasLeftInverse not

Tactic:
⟨not, not_leftInverse⟩

Premises used: Bool.not, Bool.not_leftInverse, Exists.intro, Function.HasLeftInverse
-- Module: Mathlib.Logic.Equiv.Bool
Goal:
⊢ HasRightInverse not

Tactic:
⟨not, not_rightInverse⟩

Premises used: Bool.not, Exists.intro, Bool.not_rightInverse, Function.HasRightInverse
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
e₁ e₂ : α ≃ β
h₁ : e₁.toFun = e₂.toFun
h₂ : e₁.invFun = e₂.invFun
mk :
  ∀ (toFun : α → β) (invFun : β → α) (left_inv : LeftInverse invFun toFun) (right_inv : RightInverse invFun toFun)
    (h₁ : { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun = e₂.toFun)
    (h₂ :
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.invFun = e₂.invFun),
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } = e₂
⊢ e₁ = e₂

Tactic:
cases e₁
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
e₂ : α ≃ β
toFun : α → β
invFun : β → α
left_inv : LeftInverse invFun toFun
right_inv : RightInverse invFun toFun
h₁ : { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun = e₂.toFun
h₂ : { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.invFun = e₂.invFun
mk :
  ∀ (toFun_1 : α → β) (invFun_1 : β → α) (left_inv_1 : LeftInverse invFun_1 toFun_1)
    (right_inv_1 : RightInverse invFun_1 toFun_1)
    (h₁ :
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun =
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }.toFun)
    (h₂ :
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.invFun =
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }.invFun),
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }
⊢ { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } = e₂

Tactic:
cases e₂
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
toFun : α → β
invFun : β → α
left_inv : LeftInverse invFun toFun
right_inv : RightInverse invFun toFun
toFun_1 : α → β
invFun_1 : β → α
left_inv_1 : LeftInverse invFun_1 toFun_1
right_inv_1 : RightInverse invFun_1 toFun_1
h₁ :
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun =
    { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }.toFun
h₂ :
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.invFun =
    { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }.invFun
⊢ { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } =
    { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }

Tactic:
congr
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
F : Sort u_1
inst : EquivLike F α β
e : F
⊢ Eq (α := (a : α) → β) (⇑(↑e : α ≃ β) : (a : α) → β) (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α → β
g : β → α
l : LeftInverse g f
r : RightInverse g f
⊢ (⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r : α ≃ β } : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
⊢ Injective (β := α → β) fun (e : α ≃ β) ↦ (⇑e : (a : α) → β)

Tactic:
DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e₁ e₂ : α ≃ β
⊢ Eq (α := (a : α) → β) (⇑e₁ : (a : α) → β) (⇑e₂ : (a : α) → β) ↔ e₁ = e₂

Tactic:
@DFunLike.coe_fn_eq _ _ _ _ e₁ e₂

Premises used: DFunLike.coe_fn_eq
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f g : α ≃ β
H : ∀ (x : α), Eq.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext f g H

Premises used: DFunLike.ext
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
x x' : α
⊢ x = x' → Eq.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x' : β)

Tactic:
DFunLike.congr_arg f

Premises used: DFunLike.congr_arg
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f g : α ≃ β
h : f = g
x : α
⊢ Eq.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
σ τ : Perm α
H : ∀ (x : α), Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
⊢ Eq.{max 1 u} σ τ

Tactic:
Equiv.ext H

Premises used: Equiv.ext
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
f : Perm α
x x' : α
⊢ x = x' → Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x' : α)

Tactic:
Equiv.congr_arg

Premises used: Equiv.congr_arg
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
f g : Perm α
h : Eq.{max 1 u} f g
x : α
⊢ Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
Equiv.congr_fun h x

Premises used: Equiv.congr_fun
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ LeftInverse.{u, v} (α := α) (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)

Tactic:
e.left_inv

Premises used: Equiv.left_inv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ RightInverse.{u, v} (α := α) (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)

Tactic:
e.right_inv

Premises used: Equiv.right_inv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α → β
g : β → α
hl : LeftInverse g f
hr : RightInverse g f
⊢ { toFun := f, invFun := g, left_inv := hl, right_inv := hr : α ≃ β }.symm =
    { toFun := g, invFun := f, left_inv := hr, right_inv := hl }

Tactic:
rfl

Premises used: Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ e.toFun = (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ e.invFun = (⇑e.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Injective.{u, v} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
EquivLike.injective e

Premises used: EquivLike.injective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Surjective.{u, v} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
EquivLike.surjective e

Premises used: EquivLike.surjective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Bijective.{u, v} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
EquivLike.bijective e

Premises used: EquivLike.bijective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
inst : Subsingleton β
⊢ Subsingleton α

Tactic:
e.injective.subsingleton

Premises used: Function.Injective.subsingleton, Equiv.injective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
inst : Subsingleton α
⊢ Subsingleton β

Tactic:
e.symm.injective.subsingleton

Premises used: Function.Injective.subsingleton, Equiv.injective, Equiv.symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Subsingleton α ↔ Subsingleton β

Tactic:
⟨fun _ => e.symm.subsingleton, fun _ => e.subsingleton⟩

Premises used: Iff.intro, Equiv.symm, Equiv.subsingleton
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Subsingleton β
⊢ Subsingleton (α ≃ β)

Tactic:
⟨fun _ _ => Equiv.ext fun _ => Subsingleton.elim _ _⟩

Premises used: Equiv.ext, Subsingleton.intro, Subsingleton.elim, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Subsingleton α
⊢ Subsingleton (α ≃ β)

Tactic:
⟨fun f _ => Equiv.ext fun _ => @Subsingleton.elim _ (Equiv.subsingleton.symm f) _ _⟩

Premises used: Equiv.ext, Subsingleton.intro, Subsingleton.elim, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
inst : Subsingleton α
e : Perm α
⊢ Eq.{max 1 u} e (Equiv.refl α)

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Nontrivial β
⊢ Nontrivial α

Tactic:
e.surjective.nontrivial

Premises used: Function.Surjective.nontrivial, Equiv.surjective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ Nontrivial α ↔ Nontrivial β

Tactic:
⟨fun _ ↦ e.symm.nontrivial, fun _ ↦ e.nontrivial⟩

Premises used: Equiv.nontrivial, Iff.intro, Equiv.symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Nonempty α ↔ Nonempty β

Tactic:
Nonempty.congr e e.symm

Premises used: Nonempty.congr, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
inst : Nonempty β
⊢ Nonempty α

Tactic:
e.nonempty_congr.mpr ‹_›

Premises used: Iff.mpr, Equiv.nonempty_congr
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α β : Sort u_1
h : α = β
⊢ LeftInverse (cast ⋯) (cast h)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α β : Sort u_1
h : α = β
⊢ RightInverse (cast ⋯) (cast h)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α → β
g : β → α
l : LeftInverse g f
r : RightInverse g f
⊢ (⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r : α ≃ β }.symm : (a : β) → α) = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
⊢ Eq.{u} (α := (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
inst : Subsingleton α
e : Perm α
rw : Eq (α := (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) id
rw₁ rw₂ : Eq.{u_1 + 1} (α := (a : α) → α) id id
⊢ Eq (α := (a : α) → α) (⇑e : (a : α) → α) id

Tactic:
rw [Perm.subsingleton_eq_refl e, coe_refl]

Premises used: Equiv.Perm.subsingleton_eq_refl, Equiv.coe_refl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
x : α
⊢ (Equiv.refl α : (a : α) → α) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : β ≃ γ
⊢ Eq (α := (a : α) → γ) (⇑(f.trans g) : (a : α) → γ) (comp.{u, v, w} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : β ≃ γ
a : α
⊢ Eq.{w} (α := γ) ((f.trans g : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
x : β
⊢ (e : (a : α) → β) ((e.symm : (a : β) → α) x : α) = x

Tactic:
e.right_inv x

Premises used: Equiv.right_inv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
x : α
⊢ (e.symm : (a : β) → α) ((e : (a : α) → β) x : β) = x

Tactic:
e.left_inv x

Premises used: Equiv.left_inv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Eq.{u} (α := α → α) (comp.{u, v, u} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) id

Tactic:
funext e.symm_apply_apply

Premises used: Equiv.symm_apply_apply, funext
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Eq.{v} (α := β → β) (comp.{v, u, v} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) id

Tactic:
funext e.apply_symm_apply

Premises used: Equiv.apply_symm_apply, funext
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
F : Sort u_1
inst : EquivLike F α β
e : F
x : β
⊢ (e : (a : α) → β) (((↑e : α ≃ β).symm : (a : β) → α) x : α) = x

Tactic:
(e : α ≃ β).apply_symm_apply x

Premises used: Equiv.apply_symm_apply, EquivLike.toEquiv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
F : Sort u_1
inst : EquivLike F α β
e : F
x : α
⊢ ((↑e : α ≃ β).symm : (a : β) → α) ((e : (a : α) → β) x : β) = x

Tactic:
(e : α ≃ β).symm_apply_apply x

Premises used: Equiv.symm_apply_apply, EquivLike.toEquiv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
F : Sort u_1
inst : EquivLike F α β
e : F
⊢ Eq.{u} (α := α → α) (comp.{u, v, u} (β := β) (⇑(↑e : α ≃ β).symm : (a : β) → α) (⇑e : (a : α) → β)) id

Tactic:
(e : α ≃ β).symm_comp_self

Premises used: Equiv.symm_comp_self, EquivLike.toEquiv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
F : Sort u_1
inst : EquivLike F α β
e : F
⊢ Eq.{v} (α := β → β) (comp.{v, u, v} (β := α) (⇑e : (a : α) → β) (⇑(↑e : α ≃ β).symm : (a : β) → α)) id

Tactic:
(e : α ≃ β).self_comp_symm

Premises used: Equiv.self_comp_symm, EquivLike.toEquiv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : β ≃ γ
a : γ
⊢ Eq.{u} (α := α) (((f.trans g).symm : (a : γ) → α) a : α) ((f.symm : (a : β) → α) ((g.symm : (a : γ) → β) a : β) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
b : α
⊢ Eq.{v} (α := β) ((f.symm.symm : (a : α) → β) b : β) ((f : (a : α) → β) b : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
x y : α
⊢ Eq.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x = y

Tactic:
EquivLike.apply_eq_iff_eq f

Premises used: EquivLike.apply_eq_iff_eq
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
x : α
y : β
f : α ≃ β
⊢ (f : (a : α) → β) x = y ↔ x = (f.symm : (a : β) → α) y

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α β : Sort u_1
h : α = β
x : α
⊢ (Equiv.cast h : (a : α) → β) x = cast h x

Tactic:
rfl

Premises used: cast, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α β : Sort u_1
h : α = β
⊢ Eq.{max 1 u_1} (Equiv.cast ⋯) (Equiv.cast h).symm

Tactic:
rfl

Premises used: Equiv.cast, cast, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
h : α = α
⊢ Eq.{max 1 u_1} (Equiv.cast h) (Equiv.refl α)

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
substs : Eq (α := α) ((Equiv.cast ⋯ : (a : α) → α) x : α) (((Equiv.cast ⋯).trans (Equiv.cast ⋯) : (a : α) → α) x : α)
⊢ Eq (α := γ) ((Equiv.cast ⋯ : (a : α) → γ) x : γ) (((Equiv.cast h).trans (Equiv.cast h2) : (a : α) → γ) x : γ)

Tactic:
substs h h2
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
x : α
⊢ Eq (α := α) ((Equiv.cast ⋯ : (a : α) → α) x : α) (((Equiv.cast ⋯).trans (Equiv.cast ⋯) : (a : α) → α) x : α)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α β : Sort u_1
h : α = β
a : α
b : β
subst : ∀ {b : α}, (Equiv.cast ⋯ : (a : α) → α) a = b ↔ a ≍ b
⊢ (Equiv.cast h : (a : α) → β) a = b ↔ a ≍ b

Tactic:
subst h
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
a b : α
⊢ (Equiv.cast ⋯ : (a : α) → α) a = b ↔ a ≍ b

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
⊢ (e.symm : (a : β) → α) x = y ↔ x = (e : (a : α) → β) y

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
⊢ y = (e.symm : (a : β) → α) x ↔ (e : (a : α) → β) y = x

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
⊢ Bijective (α := α ≃ β) Equiv.symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Equiv.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ e.trans (Equiv.refl β) = e

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
⊢ Eq.{max 1 u} (Equiv.refl α).symm (Equiv.refl α)

Tactic:
rfl

Premises used: Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
mk :
  ∀ (toFun : α → β) (invFun : β → α) (left_inv : LeftInverse invFun toFun) (right_inv : RightInverse invFun toFun),
    (Equiv.refl α).trans { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } =
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }
⊢ (Equiv.refl α).trans e = e

Tactic:
cases e
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
toFun : α → β
invFun : β → α
left_inv : LeftInverse invFun toFun
right_inv : RightInverse invFun toFun
⊢ (Equiv.refl α).trans { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } =
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Eq.{max 1 v} (e.symm.trans e) (Equiv.refl β)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ Eq.{max 1 u} (e.trans e.symm) (Equiv.refl α)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
bc : β ≃ γ
cd : γ ≃ δ
⊢ (ab.trans bc).trans cd = ab.trans (bc.trans cd)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β ≃ γ
g : α ≃ γ
⊢ e.trans f = g ↔ f = e.symm.trans g

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β ≃ γ
g : α ≃ γ
⊢ e.trans f = g ↔ e = g.trans f.symm

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
⊢ LeftInverse.{u, v} (α := α) (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)

Tactic:
f.left_inv

Premises used: Equiv.left_inv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
⊢ RightInverse.{u, v} (α := α) (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)

Tactic:
f.right_inv

Premises used: Equiv.right_inv
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β → γ
⊢ Injective.{u, w} (α := α) (f ∘ (⇑e : (a : α) → β)) ↔ Injective f

Tactic:
EquivLike.injective_comp e f

Premises used: EquivLike.injective_comp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α → β
e : β ≃ γ
⊢ Injective.{u, w} (β := γ) ((⇑e : (a : β) → γ) ∘ f) ↔ Injective f

Tactic:
EquivLike.comp_injective f e

Premises used: EquivLike.comp_injective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β → γ
⊢ Surjective.{u, w} (α := α) (f ∘ (⇑e : (a : α) → β)) ↔ Surjective f

Tactic:
EquivLike.surjective_comp e f

Premises used: EquivLike.surjective_comp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α → β
e : β ≃ γ
⊢ Surjective.{u, w} (β := γ) ((⇑e : (a : β) → γ) ∘ f) ↔ Surjective f

Tactic:
EquivLike.comp_surjective f e

Premises used: EquivLike.comp_surjective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β → γ
⊢ Bijective.{u, w} (α := α) (f ∘ (⇑e : (a : α) → β)) ↔ Bijective f

Tactic:
EquivLike.bijective_comp e f

Premises used: EquivLike.bijective_comp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α → β
e : β ≃ γ
⊢ Bijective.{u, w} (β := γ) ((⇑e : (a : β) → γ) ∘ f) ↔ Bijective f

Tactic:
EquivLike.comp_bijective f e

Premises used: EquivLike.comp_bijective