awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
hai : ¬Membership.mem (γ := Set α) {i} a
has : a ∈ s
⊢ Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a

Tactic:
exact ⟨a, has, swap_apply_of_ne_of_ne hai (ne_of_mem_of_not_mem has hj)⟩
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : Type u_10
inst : DecidableEq α
inst_1 : DecidableEq β
i j : α
⊢ (swap i j).sumCongr (Equiv.refl β) = swap (Sum.inl i) (Sum.inl j)

Tactic:
aesop
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : Type u_10
inst : DecidableEq α
inst_1 : DecidableEq β
i j : β
⊢ sumCongr (Equiv.refl α) (swap i j) = swap (Sum.inr i) (Sum.inr j)

Tactic:
aesop
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
f : α ≃ β
a : α
b : β
⊢ (f.setValue a b : (a : α) → β) a = b

Tactic:
simp [setValue, swap_apply_left]

Premises used: Equiv.setValue, Equiv.swap_apply_left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
f : α → α
h : Involutive f
⊢ (⇑(toPerm f h) : (a : α) → α) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
f : α → α
h : Involutive f
⊢ Eq.{max 1 u_1} (Equiv.symm (toPerm f h)) (toPerm f h)

Tactic:
rfl

Premises used: Function.Involutive.toPerm, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
f : α → α
h : Involutive f
⊢ Involutive.{u_1} (α := α) (⇑(toPerm f h) : (a : α) → α)

Tactic:
h
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
f : Equiv.Perm α
h : Involutive.{u_1} (α := α) (⇑f : (a : α) → α)
⊢ Eq.{max 1 u_1} (Equiv.symm f) f

Tactic:
DFunLike.coe_injective (h.leftInverse_iff.mp f.left_inv)

Premises used: DFunLike.coe_injective, Iff.mp, Function.Involutive.leftInverse_iff, Equiv.left_inv
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
x : PLift α
y : α
⊢ x = { down := y } ↔ x.down = y

Tactic:
Equiv.plift.eq_symm_apply

Premises used: Equiv.plift, Equiv.eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f ((Equiv.swap x y : (a : α) → α) z) = (Equiv.swap (f x) (f y) : (a : β) → β) (f z)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
P : α → Sort u_9
e : α ≃ β
f : (a : α) → P a
⊢ (fun (f : (b : β) → P ((e.symm : (a : β) → α) b)) (x : α) ↦ Eq.ndrec (motive := P) (f ((e : (a : α) → β) x)) ⋯)
      ((fun (f : (a : α) → P a) (x : β) ↦ (f ((e.symm : (a : β) → α) x) : P ((e.symm : (a : β) → α) x))) f) =
    f

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
P : α → Sort u_9
e : α ≃ β
f : (b : β) → P ((e.symm : (a : β) → α) b)
⊢ (fun (f : (a : α) → P a) (x : β) ↦ (f ((e.symm : (a : β) → α) x) : P ((e.symm : (a : β) → α) x)))
      ((fun (f : (b : β) → P ((e.symm : (a : β) → α) b)) (x : α) ↦ Eq.ndrec (motive := P) (f ((e : (a : α) → β) x)) ⋯)
        f) =
    f

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
H :
  ∀ (x : (b : β) → P) (x_1 : α),
    Eq.{u_9} (α := P)
      (((Equiv.symm (piCongrLeft' (fun (x : α) ↦ P) e) : ((b : β) → P) ≃ ((a : α) → P)) :
            (a : (b : β) → P) → (a : α) → P)
          x x_1 :
        P)
      ((piCongrLeft' (fun (a : β) ↦ P) e.symm : (a : (b : β) → P) → (a : α) → P) x x_1 : P)
⊢ Eq (α := ((b : β) → P) ≃ ((a : α) → P))
    (Equiv.symm (piCongrLeft' (fun (x : α) ↦ P) e) : ((b : β) → P) ≃ ((a : α) → P))
    (piCongrLeft' (fun (a : β) ↦ P) e.symm : ((a : β) → P) ≃ ((b : α) → P))

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
x : (b : β) → P
x_1 : α
⊢ Eq.{u_9} (α := P)
    (((Equiv.symm (piCongrLeft' (fun (x : α) ↦ P) e) : ((b : β) → P) ≃ ((a : α) → P)) : (a : (b : β) → P) → (a : α) → P)
        x x_1 :
      P)
    ((piCongrLeft' (fun (a : β) ↦ P) e.symm : (a : (b : β) → P) → (a : α) → P) x x_1 : P)

Tactic:
simp [piCongrLeft']

Premises used: Equiv.piCongrLeft'
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P ((e.symm : (a : β) → α) b)
b : β
rw :
  HEq (α := P ((e.symm : (a : β) → α) ((e : (a : α) → β) ((e.symm : (a : β) → α) b : α) : β)))
    (g ((e : (a : α) → β) ((e.symm : (a : β) → α) b : α))) (g b)
⊢ ((piCongrLeft' P e).symm : (a : (b : β) → P ((e.symm : (a : β) → α) b)) → (a : α) → P a) g
      ((e.symm : (a : β) → α) b) =
    g b

Tactic:
rw [piCongrLeft'_symm_apply, ← heq_iff_eq, eqRec_heq_iff_heq]

Premises used: eqRec_heq_iff_heq, heq_iff_eq, Equiv.piCongrLeft'_symm_apply
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P ((e.symm : (a : β) → α) b)
b : β
⊢ HEq (α := P ((e.symm : (a : β) → α) ((e : (a : α) → β) ((e.symm : (a : β) → α) b : α) : β)))
    (g ((e : (a : α) → β) ((e.symm : (a : β) → α) b : α))) (g b)

Tactic:
congr_arg_heq _ (e.apply_symm_apply _)

Premises used: Equiv.apply_symm_apply, congr_arg_heq
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P ((e.symm : (a : β) → α) b)
b : β
⊢ HEq (α := P ((e.symm : (a : β) → α) ((e : (a : α) → β) ((e.symm : (a : β) → α) b : α) : β)))
    (g ((e : (a : α) → β) ((e.symm : (a : β) → α) b : α))) (g b)

Tactic:
exact congr_arg_heq _ (e.apply_symm_apply _)

Premises used: Equiv.apply_symm_apply, congr_arg_heq
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
P : α → Sort u_9
⊢ piCongrLeft' P (Equiv.refl α) = Equiv.refl ((a : α) → P a)

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
P : β → Sort w
e : α ≃ β
f : (a : α) → P ((e : (a : α) → β) a)
b : β
⊢ Eq.{w} (α := P b) ((piCongrLeft P e : (a : (a : α) → P ((e : (a : α) → β) a)) → (b : β) → P b) f b : P b)
    (Eq.rec (motive := fun (x : β) (h : (e : (a : α) → β) ((e.symm : (a : β) → α) b : α) = x) ↦ P x)
        (f ((e.symm : (a : β) → α) b)) ⋯ :
      P b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
P : β → Sort w
e : α ≃ β
g : (b : β) → P b
a : α
⊢ Eq.{w} (α := P ((e : (a : α) → β) a))
    (((piCongrLeft P e).symm : (a : (b : β) → P b) → (a : α) → P ((e : (a : α) → β) a)) g a : P ((e : (a : α) → β) a))
    (g ((e : (a : α) → β) a) : P ((e : (a : α) → β) a))

Tactic:
piCongrLeft'_apply P e.symm g a

Premises used: Equiv.symm, Equiv.piCongrLeft'_apply
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
P : α → Sort u_9
⊢ piCongrLeft P (Equiv.refl α) = Equiv.refl ((a : α) → P a)

Tactic:
rfl

Premises used: Equiv.piCongrLeft, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
P : β → Sort w
e : α ≃ β
f : (a : α) → P ((e : (a : α) → β) a)
a : α
⊢ (piCongrLeft P e : (a : (a : α) → P ((e : (a : α) → β) a)) → (b : β) → P b) f ((e : (a : α) → β) a) = f a

Tactic:
piCongrLeft'_symm_apply_apply P e.symm f a

Premises used: Equiv.piCongrLeft'_symm_apply_apply, Equiv.symm
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
P : β → Sort v
e : α ≃ β
f : (a : α) → P ((e : (a : α) → β) a)
b : β
⊢ (piCongrLeft P e : (a : (a : α) → P ((e : (a : α) → β) a)) → (b : β) → P b) f b =
    cast ⋯ (f ((e.symm : (a : β) → α) b))

Tactic:
eqRec_eq_cast _ _

Premises used: eqRec_eq_cast
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ι : Type u_10
ι' : Type u_11
ι'' : Sort u_12
π : ι'' → Type u_9
e : ι ⊕ ι' ≃ ι''
f : (i : ι) → π ((e : (a : ι ⊕ ι') → ι'') (inl i))
g : (i : ι') → π ((e : (a : ι ⊕ ι') → ι'') (inr i))
i : ι
⊢ (piCongrLeft π e : (a : (a : ι ⊕ ι') → π ((e : (a : ι ⊕ ι') → ι'') a)) → (b : ι'') → π b)
      (((Equiv.symm (sumPiEquivProdPi fun (x : ι ⊕ ι') ↦ π ((e : (a : ι ⊕ ι') → ι'') x)) :
              ((i : ι) → π ((e : (a : ι ⊕ ι') → ι'') (inl i))) × ((i' : ι') → π ((e : (a : ι ⊕ ι') → ι'') (inr i'))) ≃
                ((i : ι ⊕ ι') → π ((e : (a : ι ⊕ ι') → ι'') i))) :
            (a :
                ((i : ι) → π ((e : (a : ι ⊕ ι') → ι'') (inl i))) ×
                  ((i' : ι') → π ((e : (a : ι ⊕ ι') → ι'') (inr i')))) →
              (i : ι ⊕ ι') → π ((e : (a : ι ⊕ ι') → ι'') i))
          (f, g) :
        (i : ι ⊕ ι') → π ((e : (a : ι ⊕ ι') → ι'') i))
      ((e : (a : ι ⊕ ι') → ι'') (inl i)) =
    f i

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ι : Type u_10
ι' : Type u_11
ι'' : Sort u_12
π : ι'' → Type u_9
e : ι ⊕ ι' ≃ ι''
f : (i : ι) → π ((e : (a : ι ⊕ ι') → ι'') (inl i))
g : (i : ι') → π ((e : (a : ι ⊕ ι') → ι'') (inr i))
j : ι'
⊢ (piCongrLeft π e : (a : (a : ι ⊕ ι') → π ((e : (a : ι ⊕ ι') → ι'') a)) → (b : ι'') → π b)
      (((Equiv.symm (sumPiEquivProdPi fun (x : ι ⊕ ι') ↦ π ((e : (a : ι ⊕ ι') → ι'') x)) :
              ((i : ι) → π ((e : (a : ι ⊕ ι') → ι'') (inl i))) × ((i' : ι') → π ((e : (a : ι ⊕ ι') → ι'') (inr i'))) ≃
                ((i : ι ⊕ ι') → π ((e : (a : ι ⊕ ι') → ι'') i))) :
            (a :
                ((i : ι) → π ((e : (a : ι ⊕ ι') → ι'') (inl i))) ×
                  ((i' : ι') → π ((e : (a : ι ⊕ ι') → ι'') (inr i')))) →
              (i : ι ⊕ ι') → π ((e : (a : ι ⊕ ι') → ι'') i))
          (f, g) :
        (i : ι ⊕ ι') → π ((e : (a : ι ⊕ ι') → ι'') i))
      ((e : (a : ι ⊕ ι') → ι'') (inr j)) =
    g j

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → Equiv.{w, z} (W a) (Z ((h₁ : (a : α) → β) a))
⊢ Eq (α := (a : (b : β) → Z b) → (a : α) → W a)
    (⇑(h₁.piCongr (W := W) (Z := Z) h₂).symm : (a : (b : β) → Z b) → (a : α) → W a) fun (f : (b : β) → Z b) (a : α) ↦
    ((h₂ a).symm : (a_1 : Z ((h₁ : (a : α) → β) a)) → W a) (f ((h₁ : (a : α) → β) a))

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → Equiv.{w, z} (W a) (Z ((h₁ : (a : α) → β) a))
f : (b : β) → Z b
⊢ Eq (α := (a : α) → W a)
    (((h₁.piCongr (W := W) (Z := Z) h₂).symm : (a : (b : β) → Z b) → (a : α) → W a) f : (a : α) → W a) fun (a : α) ↦
    (((h₂ a).symm : (a_1 : Z ((h₁ : (a : α) → β) a)) → W a) (f ((h₁ : (a : α) → β) a)) : W a)

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → Equiv.{w, z} (W a) (Z ((h₁ : (a : α) → β) a))
f : (a : α) → W a
a : α
rw :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    (((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂).trans (piCongrLeft Z h₁) :
          (a : (a : α) → W a) → (b : β) → Z b)
        f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₁ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((piCongrLeft Z h₁ : (a : (a : α) → Z ((h₁ : (a : α) → β) a)) → (b : β) → Z b)
        ((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂ :
              (a : (a : α) → W a) → (a : α) → Z ((h₁ : (a : α) → β) a))
            f :
          (a : α) → Z ((h₁ : (a : α) → β) a))
        ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₂ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂ :
          (a : (a : α) → W a) → (a : α) → Z ((h₁ : (a : α) → β) a))
        f a :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₃ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    (Pi.map.{u_1, w, z} (α := W) (β := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a))
        (fun (a : α) ↦ ((⇑(h₂ a) : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) : (a_1 : W a) → Z ((h₁ : (a : α) → β) a))) f
        a :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₄ rw₅ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
⊢ Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((h₁.piCongr (W := W) (Z := Z) h₂ : (a : (a : α) → W a) → (b : β) → Z b) f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))

Tactic:
rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Pi.map_apply]

Premises used: Equiv.trans_apply, Equiv.piCongrRight_apply, Equiv.piCongr, Equiv.piCongrLeft_apply_apply, Pi.map_apply
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → Equiv.{w, z} (W ((h₁.symm : (a : β) → α) b)) (Z b)
⊢ Eq (α := (a : (a : α) → W a) → (b : β) → Z b)
    (⇑(h₁.piCongr' (W := W) (Z := Z) h₂) : (a : (a : α) → W a) → (b : β) → Z b) fun (f : (a : α) → W a) (b : β) ↦
    (h₂ b : (a : W ((h₁.symm : (a : β) → α) b)) → Z b) (f ((h₁.symm : (a : β) → α) b))

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → Equiv.{w, z} (W ((h₁.symm : (a : β) → α) b)) (Z b)
f : (a : α) → W a
⊢ Eq (α := (b : β) → Z b) ((h₁.piCongr' (W := W) (Z := Z) h₂ : (a : (a : α) → W a) → (b : β) → Z b) f : (b : β) → Z b)
    fun (b : β) ↦ ((h₂ b : (a : W ((h₁.symm : (a : β) → α) b)) → Z b) (f ((h₁.symm : (a : β) → α) b)) : Z b)

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → Equiv.{w, z} (W ((h₁.symm : (a : β) → α) b)) (Z b)
f : (b : β) → Z b
b : β
⊢ Eq.{w} (α := W ((h₁.symm : (a : β) → α) b))
    (((h₁.piCongr' (W := W) (Z := Z) h₂).symm : (a : (b : β) → Z b) → (a : α) → W a) f ((h₁.symm : (a : β) → α) b) :
      W ((h₁.symm : (a : β) → α) b))
    (((h₂ b).symm : (a : Z b) → W ((h₁.symm : (a : β) → α) b)) (f b) : W ((h₁.symm : (a : β) → α) b))

Tactic:
simp [piCongr', piCongr_apply_apply]

Premises used: Equiv.piCongr_apply_apply, Equiv.piCongr'
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : Type u_10
f : α → β
γ₁ : α → Sort u_11
γ₂ : α → Sort u_12
e : (a : α) → Equiv.{u_11, u_12} (γ₁ a) (γ₂ a)
g : (σ : (y : β) × { x : α // f x = y }) → γ₁ (↑(σ.snd (β := fun (y : β) ↦ { x : α // f x = y })) : α)
a : α
⊢ Eq.{u_12} (α := γ₂ a)
    ((piCongrSigmaFiber (γ₁ := γ₁) (γ₂ := γ₂) e :
          (a : (σ : (y : β) × { x : α // f x = y }) → γ₁ (↑σ.snd : α)) → (a : α) → γ₂ a)
        g a :
      γ₂ a)
    ((e a : (a_1 : γ₁ a) → γ₂ a)
        (g (Sigma.mk (β := fun (y : β) ↦ { x : α // f x = y }) (f a) (Subtype.mk (p := fun (x : α) ↦ f x = f a) a ⋯))) :
      γ₂ a)

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : Type u_10
f : α → β
γ₁ : α → Sort u_11
γ₂ : α → Sort u_12
e : (a : α) → Equiv.{u_11, u_12} (γ₁ a) (γ₂ a)
g : (a : α) → γ₂ a
σ : (y : β) × { x : α // f x = y }
⊢ Eq.{u_11} (α := γ₁ (↑(σ.snd (β := fun (y : β) ↦ { x : α // f x = y })) : α))
    ((Equiv.symm (piCongrSigmaFiber (γ₁ := γ₁) (γ₂ := γ₂) e) :
          (a : (a : α) → γ₂ a) → (σ : (y : β) × { x : α // f x = y }) → γ₁ (↑σ.snd : α))
        g σ :
      γ₁ (↑(σ.snd (β := fun (y : β) ↦ { x : α // f x = y })) : α))
    (((Equiv.symm (e (↑(σ.snd (β := fun (y : β) ↦ { x : α // f x = y })) : α)) :
            Equiv.{u_12, u_11} (γ₂ (↑(σ.snd (β := fun (y : β) ↦ { x : α // f x = y })) : α))
              (γ₁ (↑(σ.snd (β := fun (y : β) ↦ { x : α // f x = y })) : α))) :
          (a : γ₂ (↑σ.snd : α)) → γ₁ (↑σ.snd : α))
        (g (↑(σ.snd (β := fun (y : β) ↦ { x : α // f x = y })) : α)) :
      γ₁ (↑(σ.snd (β := fun (y : β) ↦ { x : α // f x = y })) : α))

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : Type u_10
γ₁ : α → Type u_11
γ₂ : β → Type u_12
f : α → β
e : (b : β) → ((σ : { a : α // f a = b }) → γ₁ (↑σ : α)) ≃ γ₂ b
g : (a : α) → γ₁ a
b : β
⊢ Eq.{u_12 + 1} (α := γ₂ b)
    ((piCongrFiberwise (γ₁ := γ₁) (γ₂ := γ₂) e : (a : (a : α) → γ₁ a) → (b : β) → γ₂ b) g b : γ₂ b)
    ((e b : (a : (σ : { a : α // f a = b }) → γ₁ (↑σ : α)) → γ₂ b) fun (σ : { a : α // f a = b }) ↦ g (↑σ : α) : γ₂ b)

Tactic:
rfl

Premises used: Pi.map, Sigma.curry, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : Type u_10
γ₁ : α → Type u_11
γ₂ : β → Type u_12
f : α → β
e : (b : β) → ((σ : { a : α // f a = b }) → γ₁ (↑σ : α)) ≃ γ₂ b
g : (b : β) → γ₂ b
a : α
⊢ Eq.{u_11 + 1} (α := γ₁ a)
    (((piCongrFiberwise (γ₁ := γ₁) (γ₂ := γ₂) e).symm : (a : (b : β) → γ₂ b) → (a : α) → γ₁ a) g a : γ₁ a)
    ((Equiv.symm (e (f a)) : (a_1 : γ₂ (f a)) → (σ : { a_2 : α // f a_2 = f a }) → γ₁ (↑σ : α)) (g (f a))
        (Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a) a ⋯) :
      γ₁ (↑(Subtype.mk (p := fun (a_1 : α) ↦ f a_1 = f a) a ⋯) : α))

Tactic:
rfl

Premises used: Sigma.uncurry, Pi.map, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α_2 : Type u_9
β : Type u_10
f_1 : α_2 → β
α : Type u_11
W : α → Sort w
s : Set α
f : (i : { i : α // i ∈ s }) → W (↑i : α)
i : { i : α // i ∈ s }
⊢ (↑i : α) ∈ s

Tactic:
i.2

Premises used: Subtype.property
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α_2 : Type u_9
β : Type u_10
f_1 : α_2 → β
α : Type u_11
W : α → Sort w
t : Set α
f : (i : { i : α // i ∈ t }) → W (↑i : α)
h : t = t
i : { i : α // i ∈ t }
⊢ (↑i : α) ∈ t

Tactic:
i.2

Premises used: Subtype.property
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_11
α' : Sort u_12
β : Sort u_13
β' : Sort u_14
ε₁ : α ≃ α'
ε₂ : β' ≃ β
f : α → β
f' : α' → β'
rw : f ∘ (⇑ε₁.symm : (a : α') → α) = (⇑ε₂ : (a : β') → β) ∘ f' ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
rw₁ : f = ((⇑ε₂ : (a : β') → β) ∘ f') ∘ (⇑ε₁ : (a : α) → α') ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
rw₂ rw₃ : f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α') ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
⊢ (⇑ε₂.symm : (a : β) → β') ∘ f ∘ (⇑ε₁.symm : (a : α') → α) = f' ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')

Tactic:
rw [Equiv.symm_comp_eq, Equiv.comp_symm_eq, Function.comp_assoc]

Premises used: Equiv.symm_comp_eq, Equiv.comp_symm_eq, Function.comp_assoc
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α₁ : Type u_11
β₁ : Type u_12
e : α₁ ≃ β₁
f : α₁ → α₁
x : α₁
⊢ Eq.{u_12 + 1} (α := β₁) ((e : (a : α₁) → β₁) (f x) : β₁)
    ((e.conj : (a : α₁ → α₁) → β₁ → β₁) f ((e : (a : α₁) → β₁) x) : β₁)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α₁ : Type u_11
β₁ : Type u_12
e : α₁ ≃ β₁
f : α₁ → α₁ → α₁
x y : α₁
⊢ Eq.{u_12 + 1} (α := β₁) ((e : (a : α₁) → β₁) (f x y) : β₁)
    ((e.arrowCongr e.conj : (a : α₁ → α₁ → α₁) → β₁ → β₁ → β₁) f ((e : (a : α₁) → β₁) x) ((e : (a : α₁) → β₁) y) : β₁)

Tactic:
simp [arrowCongr]

Premises used: Equiv.arrowCongr
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁_1 : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁_1 : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
f_1 : α → β
α₁ : Type u_11
β₁ : Type u_12
e : α₁ ≃ β₁
f : α₁ → α₁ → α₁
inst : Std.Associative f
⊢ Std.Associative.{u_12 + 1} (α := β₁) ((e.arrowCongr (e.arrowCongr e) : (a : α₁ → α₁ → α₁) → β₁ → β₁ → β₁) f)

Tactic:
(e.semiconj₂_conj f).isAssociative_right e.surjective

Premises used: Function.Semiconj₂.isAssociative_right, Equiv.semiconj₂_conj, Equiv.surjective
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁_1 : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁_1 : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
f_1 : α → β
α₁ : Type u_11
β₁ : Type u_12
e : α₁ ≃ β₁
f : α₁ → α₁ → α₁
inst : Std.IdempotentOp f
⊢ Std.IdempotentOp.{u_12 + 1} (α := β₁) ((e.arrowCongr (e.arrowCongr e) : (a : α₁ → α₁ → α₁) → β₁ → β₁ → β₁) f)

Tactic:
(e.semiconj₂_conj f).isIdempotent_right e.surjective

Premises used: Function.Semiconj₂.isIdempotent_right, Equiv.semiconj₂_conj, Equiv.surjective
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type v
x : α
⊢ ULift.down.{u, v} ((Equiv.symm Equiv.ulift : (a : α) → ULift α) x) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ (Equiv.swap (f x) (f y) : (a : β) → β) (f z) = f ((Equiv.swap x y : (a : α) → α) z)

Tactic:
Eq.symm (map_swap hf x y z)

Premises used: Function.Injective.map_swap, Eq.symm
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x y : α
⊢ (⇑(Equiv.swap (f x) (f y)) : (a : β) → β) ∘ f = f ∘ (⇑(Equiv.swap x y) : (a : α) → α)

Tactic:
funext fun _ => hf.swap_apply _ _ _

Premises used: funext, Function.Injective.swap_apply
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
α' : Sort u_9
inst : DecidableEq α'
inst_1 : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
rw :
  Eq (α := α' → β) (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α))
    (update (β := fun (a : α) ↦ β) f ((g : (a : α') → α) ((g.symm : (a : α) → α') a : α')) v ∘ (⇑g : (a : α') → α))
rw₁ rw₂ :
  Eq (α := α' → β) (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α))
    (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α))
⊢ Eq (α := α' → β) (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α) : α' → β)
    (update (β := fun (a : α') ↦ β) (f ∘ (⇑g : (a : α') → α)) ((g.symm : (a : α) → α') a) v : (a : α') → β)

Tactic:
rw [← update_comp_eq_of_injective _ g.injective, g.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.injective, Function.update_comp_eq_of_injective
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
α' : Sort u_9
inst : DecidableEq α'
inst_1 : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
a' : α'
⊢ update (β := fun (a : α) ↦ β) f a v ((g : (a : α') → α) a') =
    update (β := fun (a : α') ↦ β) (f ∘ (⇑g : (a : α') → α)) ((g.symm : (a : α) → α') a) v a'

Tactic:
congr_fun (update_comp_equiv f g a v) a'

Premises used: Function.update, Function.update_comp_equiv, dite, congr_fun
-- 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)
h :
  ∀ (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 (α := (b : β) → 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 :
      (a : β) → P ((e.symm : (a : β) → α) a))

Tactic:
ext b'