awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
rw :
  extend (⇑f : (a : α) → β) g e' ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α)) =
    g ((f.symm : (a : β) → α) ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β))
rw₁ : g ((f.symm : (a : β) → α) b) = g ((f.symm : (a : β) → α) ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β))
rw₂ rw₃ : g ((f.symm : (a : β) → α) b) = g ((f.symm : (a : β) → α) b)
⊢ extend (⇑f : (a : α) → β) g e' b = g ((f.symm : (a : β) → α) b)

Tactic:
rw [← f.apply_symm_apply b, f.injective.extend_apply, apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Function.Injective.extend_apply, Equiv.injective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
ac : α ≃ γ
⊢ (fun (bd : β ≃ δ) ↦ ab.trans (bd.trans cd.symm)) ((fun (ac : α ≃ γ) ↦ (ab.symm.trans ac).trans cd) ac) = ac

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

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
e : α ≃ γ
x : β
⊢ Eq.{u_1} (α := δ) ((((ab.equivCongr cd : (a : α ≃ γ) → β ≃ δ) e : β ≃ δ) : (a : β) → δ) x : δ)
    ((cd : (a : γ) → δ) ((e : (a : α) → γ) ((ab.symm : (a : β) → α) x : α) : γ) : δ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
H :
  ∀ (x : β ≃ δ) (x_1 : α),
    Eq.{w} (α := γ) (((((ab.equivCongr cd).symm : (a : β ≃ δ) → α ≃ γ) x : α ≃ γ) : (a : α) → γ) x_1 : γ)
      ((((ab.symm.equivCongr cd.symm : (a : β ≃ δ) → α ≃ γ) x : α ≃ γ) : (a : α) → γ) x_1 : γ)
⊢ (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x : β ≃ δ
x_1 : α
⊢ Eq.{w} (α := γ) (((((ab.equivCongr cd).symm : (a : β ≃ δ) → α ≃ γ) x : α ≃ γ) : (a : α) → γ) x_1 : γ)
    ((((ab.symm.equivCongr cd.symm : (a : β ≃ δ) → α ≃ γ) x : α ≃ γ) : (a : α) → γ) x_1 : γ)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
⊢ (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
⊢ (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
bg : β ≃ γ
e : α ≃ β
⊢ ((Equiv.refl α).equivCongr bg : (a : α ≃ β) → α ≃ γ) e = e.trans bg

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
ab e : α ≃ β
⊢ Eq.{max 1 u_2} ((ab.equivCongr (Equiv.refl β) : (a : α ≃ β) → β ≃ β) e) (ab.symm.trans e)

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p : Perm α'
⊢ (e.permCongr : (a : Perm α') → Perm β') p = (e.symm.trans p).trans e

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
⊢ (e.permCongr : (a : Perm α') → Perm β') (Equiv.refl α') = Equiv.refl β'

Tactic:
simp [permCongr_def]

Premises used: Equiv.permCongr_def
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
⊢ e.permCongr.symm = e.symm.permCongr

Tactic:
rfl

Premises used: Equiv.equivCongr, Equiv.trans, Equiv.permCongr, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p : Perm α'
x : β'
⊢ Eq (α := β') ((((e.permCongr : (a : Perm α') → Perm β') p : Perm β') : (a : β') → β') x : β')
    ((e : (a : α') → β') ((p : (a : α') → α') ((e.symm : (a : β') → α') x : α') : α') : β')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p : Perm β'
x : α'
⊢ Eq (α := α') ((((e.permCongr.symm : (a : Perm β') → Perm α') p : Perm α') : (a : α') → α') x : α')
    ((e.symm : (a : β') → α') ((p : (a : β') → β') ((e : (a : α') → β') x : β') : β') : α')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
⊢ Eq.{u_2 + 1} (α := β' ≃ β')
    (Equiv.trans (β := β') ((e.permCongr : (a : Perm α') → Perm β') p) ((e.permCongr : (a : Perm α') → Perm β') p'))
    ((e.permCongr : (a : Perm α') → Perm β') (Equiv.trans p p'))

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₁ → β₁
⊢ (fun (f : α₂ → β₂) ↦ ((⇑e₂.symm : (a : β₂) → β₁) ∘ f ∘ (⇑e₁ : (a : α₁) → α₂) : α₁ → β₁))
      ((fun (f : α₁ → β₁) ↦ ((⇑e₂ : (a : β₁) → β₂) ∘ f ∘ (⇑e₁.symm : (a : α₂) → α₁) : α₂ → β₂)) f) =
    f

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₂ → β₂
⊢ (fun (f : α₁ → β₁) ↦ ((⇑e₂ : (a : β₁) → β₂) ∘ f ∘ (⇑e₁.symm : (a : α₂) → α₁) : α₂ → β₂))
      ((fun (f : α₂ → β₂) ↦ ((⇑e₂.symm : (a : β₂) → β₁) ∘ f ∘ (⇑e₁ : (a : α₁) → α₂) : α₁ → β₁)) f) =
    f

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
⊢ Eq (α := α₂ → γ₂) ((ea.arrowCongr ec : (a : α₁ → γ₁) → α₂ → γ₂) (g ∘ f) : α₂ → γ₂)
    (comp.{u_4, u_5, u_6} (β := β₂) ((eb.arrowCongr ec : (a : β₁ → γ₁) → β₂ → γ₂) g)
        ((ea.arrowCongr eb : (a : α₁ → β₁) → α₂ → β₂) f) :
      α₂ → γ₂)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
⊢ (Equiv.refl α).arrowCongr (Equiv.refl β) = Equiv.refl (α → β)

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α₁ : Sort u_1
α₂ : Sort u_2
α₃ : Sort u_3
β₁ : Sort u_4
β₂ : Sort u_5
β₃ : Sort u_6
e₁ : α₁ ≃ α₂
e₁' : β₁ ≃ β₂
e₂ : α₂ ≃ α₃
e₂' : β₂ ≃ β₃
⊢ (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α₁ : Sort u_1
α₂ : Sort u_2
β₁ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
⊢ (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm

Tactic:
rfl

Premises used: Equiv.arrowCongr, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : Type u_2
⊢ (Equiv.refl α).arrowCongr' (Equiv.refl β) = Equiv.refl (α → β)

Tactic:
rfl

Premises used: Equiv.arrowCongr', Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
α₃ : Type u_5
β₃ : Type u_6
e₁ : α₁ ≃ α₂
e₁' : β₁ ≃ β₂
e₂ : α₂ ≃ α₃
e₂' : β₂ ≃ β₃
⊢ (e₁.trans e₂).arrowCongr' (e₁'.trans e₂') = (e₁.arrowCongr' e₁').trans (e₂.arrowCongr' e₂')

Tactic:
rfl

Premises used: Equiv.trans, Equiv.arrowCongr', rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
⊢ (e₁.arrowCongr' e₂).symm = e₁.symm.arrowCongr' e₂.symm

Tactic:
rfl

Premises used: Equiv.arrowCongr, Equiv.arrowCongr', Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
⊢ Eq.{max 1 u} (Equiv.refl α).conj (Equiv.refl (α → α))

Tactic:
rfl

Premises used: Equiv.conj, Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ e.conj.symm = e.symm.conj

Tactic:
rfl

Premises used: Equiv.conj, Equiv.arrowCongr, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
e₁ : α ≃ β
e₂ : β ≃ γ
⊢ (e₁.trans e₂).conj = e₁.conj.trans e₂.conj

Tactic:
rfl

Premises used: Equiv.trans, Equiv.conj, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
e : α ≃ β
f₁ f₂ : α → α
⊢ Eq.{v} (α := β → β) ((e.conj : (a : α → α) → β → β) (f₁ ∘ f₂) : β → β)
    (comp (β := β) ((e.conj : (a : α → α) → β → β) f₁) ((e.conj : (a : α → α) → β → β) f₂) : β → β)

Tactic:
apply arrowCongr_comp

Premises used: Equiv.arrowCongr_comp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
e : α ≃ β
f : β → γ
g : α → γ
⊢ f = g ∘ (⇑e.symm : (a : β) → α) ↔ f ∘ (⇑e : (a : α) → β) = g

Tactic:
(e.arrowCongr (Equiv.refl γ)).symm_apply_eq.symm

Premises used: Equiv.arrowCongr, Equiv.symm_apply_eq, Equiv.refl, Iff.symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
e : α ≃ β
f : β → γ
g : α → γ
⊢ g ∘ (⇑e.symm : (a : β) → α) = f ↔ g = f ∘ (⇑e : (a : α) → β)

Tactic:
(e.arrowCongr (Equiv.refl γ)).eq_symm_apply.symm

Premises used: Equiv.arrowCongr, Equiv.refl, Iff.symm, Equiv.eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
e : α ≃ β
f : γ → α
g : γ → β
⊢ f = (⇑e.symm : (a : β) → α) ∘ g ↔ (⇑e : (a : α) → β) ∘ f = g

Tactic:
((Equiv.refl γ).arrowCongr e).eq_symm_apply

Premises used: Equiv.arrowCongr, Equiv.refl, Equiv.eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
e : α ≃ β
f : γ → α
g : γ → β
⊢ (⇑e.symm : (a : β) → α) ∘ g = f ↔ g = (⇑e : (a : α) → β) ∘ f

Tactic:
((Equiv.refl γ).arrowCongr e).symm_apply_eq

Premises used: Equiv.arrowCongr, Equiv.symm_apply_eq, Equiv.refl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
rw : Eq.{u} (α := (a : α) → α) (⇑(f.trans g) : (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) ↔ f = g.symm
rw₁ :
  Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β))
      (⇑(Equiv.refl α) : (a : α) → α) ↔
    f = g.symm
rw₂ : Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β)) id ↔ f = g.symm
rw₃ : Eq (α := α → β) (⇑f : (a : α) → β) ((⇑g.symm : (a : α) → β) ∘ id) ↔ f = g.symm
rw₄ : Eq (α := α → β) (⇑f : (a : α) → β) (⇑g.symm : (a : α) → β) ↔ f = g.symm
rw₅ rw₆ : f = g.symm ↔ f = g.symm
⊢ Eq.{max 1 u} (f.trans g) (Equiv.refl α) ↔ f = g.symm

Tactic:
rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]

Premises used: Function.comp_id, Equiv.eq_symm_comp, Equiv.coe_refl, Equiv.coe_inj, Equiv.coe_trans
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
rw : f = g.symm ↔ f.symm = g
⊢ Eq.{max 1 u} (f.trans g) (Equiv.refl α) ↔ f.symm = g

Tactic:
rw [trans_eq_refl_iff_eq_symm]

Premises used: Equiv.trans_eq_refl_iff_eq_symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f.symm = g

Tactic:
⟨fun h ↦ h ▸ rfl, fun h ↦ h ▸ rfl⟩

Premises used: Eq.rec, Iff.intro, Eq.symm, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f.symm = g

Tactic:
exact ⟨fun h ↦ h ▸ rfl, fun h ↦ h ▸ rfl⟩
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ Eq.{max 1 u} (f.trans g) (Equiv.refl α)

Tactic:
trans_eq_refl_iff_eq_symm.symm

Premises used: Iff.symm, Equiv.trans_eq_refl_iff_eq_symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.symm = g ↔ Eq.{max 1 u} (f.trans g) (Equiv.refl α)

Tactic:
trans_eq_refl_iff_symm_eq.symm

Premises used: Equiv.trans_eq_refl_iff_symm_eq, Iff.symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
p : Prop
⊢ (fun (b : Bool) ↦ b = true) ((fun (p : Prop) ↦ decide p) p) = p

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
b : Bool
⊢ (fun (p : Prop) ↦ decide p) ((fun (b : Bool) ↦ b = true) b) = b

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β_1 : Sort v
γ : Sort w
inst : Unique α
β : α → Sort u_1
f : (i : α) → β i
h : ∀ (i : α), uniqueElim (α := β) ((fun (f : (i : α) → β i) ↦ (f default : β default)) f) i = f i
⊢ uniqueElim (α := β) ((fun (f : (i : α) → β i) ↦ (f default : β default)) f) = f

Tactic:
ext i
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β_1 : Sort v
γ : Sort w
inst : Unique α
β : α → Sort u_1
f : (i : α) → β i
i : α
h :
  Eq (α := β default) (uniqueElim (α := β) ((fun (f : (i : α) → β i) ↦ (f default : β default)) f) default) (f default)
⊢ uniqueElim (α := β) ((fun (f : (i : α) → β i) ↦ (f default : β default)) f) i = f i

Tactic:
cases Unique.eq_default i

Premises used: Unique.eq_default
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β_1 : Sort v
γ : Sort w
inst : Unique α
β : α → Sort u_1
f : (i : α) → β i
⊢ Eq (α := β default) (uniqueElim (α := β) ((fun (f : (i : α) → β i) ↦ (f default : β default)) f) default) (f default)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → Equiv.{u_1, u_2} (β₁ a) (β₂ a)
⊢ LeftInverse
    (fun (a : (a : α) ×' β₂ a) ↦
      PSigma.mk (β := fun (a : α) ↦ β₁ a) (a.fst (β := fun (a : α) ↦ β₂ a))
        (((Equiv.symm (F (a.fst (β := fun (a : α) ↦ β₂ a))) :
              Equiv.{u_2, u_1} (β₂ (a.fst (β := fun (a : α) ↦ β₂ a))) (β₁ (a.fst (β := fun (a : α) ↦ β₂ a)))) :
            (a_1 : β₂ a.fst) → β₁ a.fst)
          (a.snd (β := fun (a : α) ↦ β₂ a))))
    fun (a : (a : α) ×' β₁ a) ↦
    PSigma.mk (β := fun (a : α) ↦ β₂ a) (a.fst (β := fun (a : α) ↦ β₁ a))
      ((F (a.fst (β := fun (a : α) ↦ β₁ a)) : (a_1 : β₁ a.fst) → β₂ a.fst) (a.snd (β := fun (a : α) ↦ β₁ a)))

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → Equiv.{u_1, u_2} (β₁ a) (β₂ a)
⊢ RightInverse
    (fun (a : (a : α) ×' β₂ a) ↦
      PSigma.mk (β := fun (a : α) ↦ β₁ a) (a.fst (β := fun (a : α) ↦ β₂ a))
        (((Equiv.symm (F (a.fst (β := fun (a : α) ↦ β₂ a))) :
              Equiv.{u_2, u_1} (β₂ (a.fst (β := fun (a : α) ↦ β₂ a))) (β₁ (a.fst (β := fun (a : α) ↦ β₂ a)))) :
            (a_1 : β₂ a.fst) → β₁ a.fst)
          (a.snd (β := fun (a : α) ↦ β₂ a))))
    fun (a : (a : α) ×' β₁ a) ↦
    PSigma.mk (β := fun (a : α) ↦ β₂ a) (a.fst (β := fun (a : α) ↦ β₁ a))
      ((F (a.fst (β := fun (a : α) ↦ β₁ a)) : (a_1 : β₁ a.fst) → β₂ a.fst) (a.snd (β := fun (a : α) ↦ β₁ a)))

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_4
β₁ : α → Sort u_1
β₂ : α → Sort u_2
β₃ : α → Sort u_3
F : (a : α) → Equiv.{u_1, u_2} (β₁ a) (β₂ a)
G : (a : α) → Equiv.{u_2, u_3} (β₂ a) (β₃ a)
⊢ (psigmaCongrRight (β₁ := β₁) (β₂ := β₂) F).trans (psigmaCongrRight (β₁ := β₂) (β₂ := β₃) G) =
    psigmaCongrRight (β₁ := β₁) (β₂ := β₃) fun (a : α) ↦ (F a).trans (G a)

Tactic:
rfl

Premises used: Equiv.psigmaCongrRight, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_3
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → Equiv.{u_1, u_2} (β₁ a) (β₂ a)
⊢ (psigmaCongrRight (β₁ := β₁) (β₂ := β₂) F).symm = psigmaCongrRight (β₁ := β₂) (β₂ := β₁) fun (a : α) ↦ (F a).symm

Tactic:
rfl

Premises used: Equiv.psigmaCongrRight, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_2
β : α → Sort u_1
⊢ Eq (α := (a : α) ×' β a ≃ (a : α) ×' β a) (psigmaCongrRight (β₁ := β) (β₂ := β) fun (a : α) ↦ Equiv.refl (β a))
    (Equiv.refl ((a : α) ×' β a))

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α_1 : Sort u
β : Sort v
γ : Sort w
α : Type u_3
β₁ : α → Type u_1
β₂ : α → Type u_2
F : (a : α) → Equiv.{u_1 + 1, u_2 + 1} (β₁ a) (β₂ a)
⊢ LeftInverse
    (fun (a : (a : α) × β₂ a) ↦
      Sigma.mk (β := fun (a : α) ↦ β₁ a) (a.fst (β := fun (a : α) ↦ β₂ a))
        (((Equiv.symm (F (a.fst (β := fun (a : α) ↦ β₂ a))) :
              Equiv.{u_2 + 1, u_1 + 1} (β₂ (a.fst (β := fun (a : α) ↦ β₂ a))) (β₁ (a.fst (β := fun (a : α) ↦ β₂ a)))) :
            (a_1 : β₂ a.fst) → β₁ a.fst)
          (a.snd (β := fun (a : α) ↦ β₂ a))))
    fun (a : (a : α) × β₁ a) ↦
    Sigma.mk (β := fun (a : α) ↦ β₂ a) (a.fst (β := fun (a : α) ↦ β₁ a))
      ((F (a.fst (β := fun (a : α) ↦ β₁ a)) : (a_1 : β₁ a.fst) → β₂ a.fst) (a.snd (β := fun (a : α) ↦ β₁ a)))

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α_1 : Sort u
β : Sort v
γ : Sort w
α : Type u_3
β₁ : α → Type u_1
β₂ : α → Type u_2
F : (a : α) → Equiv.{u_1 + 1, u_2 + 1} (β₁ a) (β₂ a)
⊢ RightInverse
    (fun (a : (a : α) × β₂ a) ↦
      Sigma.mk (β := fun (a : α) ↦ β₁ a) (a.fst (β := fun (a : α) ↦ β₂ a))
        (((Equiv.symm (F (a.fst (β := fun (a : α) ↦ β₂ a))) :
              Equiv.{u_2 + 1, u_1 + 1} (β₂ (a.fst (β := fun (a : α) ↦ β₂ a))) (β₁ (a.fst (β := fun (a : α) ↦ β₂ a)))) :
            (a_1 : β₂ a.fst) → β₁ a.fst)
          (a.snd (β := fun (a : α) ↦ β₂ a))))
    fun (a : (a : α) × β₁ a) ↦
    Sigma.mk (β := fun (a : α) ↦ β₂ a) (a.fst (β := fun (a : α) ↦ β₁ a))
      ((F (a.fst (β := fun (a : α) ↦ β₁ a)) : (a_1 : β₁ a.fst) → β₂ a.fst) (a.snd (β := fun (a : α) ↦ β₁ a)))

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_4
β₁ : α → Type u_1
β₂ : α → Type u_2
β₃ : α → Type u_3
F : (a : α) → Equiv.{u_1 + 1, u_2 + 1} (β₁ a) (β₂ a)
G : (a : α) → Equiv.{u_2 + 1, u_3 + 1} (β₂ a) (β₃ a)
⊢ (sigmaCongrRight (β₁ := β₁) (β₂ := β₂) F).trans (sigmaCongrRight (β₁ := β₂) (β₂ := β₃) G) =
    sigmaCongrRight (β₁ := β₁) (β₂ := β₃) fun (a : α) ↦ (F a).trans (G a)

Tactic:
rfl

Premises used: Equiv.sigmaCongrRight, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_3
β₁ : α → Type u_1
β₂ : α → Type u_2
F : (a : α) → Equiv.{u_1 + 1, u_2 + 1} (β₁ a) (β₂ a)
⊢ (sigmaCongrRight (β₁ := β₁) (β₂ := β₂) F).symm = sigmaCongrRight (β₁ := β₂) (β₂ := β₁) fun (a : α) ↦ (F a).symm

Tactic:
rfl

Premises used: Equiv.symm, Equiv.sigmaCongrRight, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_2
β : α → Type u_1
⊢ Eq (α := (a : α) × β a ≃ (a : α) × β a) (sigmaCongrRight (β₁ := β) (β₂ := β) fun (a : α) ↦ Equiv.refl (β a))
    (Equiv.refl ((a : α) × β a))

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : α → Type u_2
F G : (a : α) → Perm (β a)
⊢ Equiv.trans (sigmaCongrRight (β := β) F) (sigmaCongrRight (β := β) G) =
    sigmaCongrRight (β := β) fun (a : α) ↦ Equiv.trans (F a) (G a)

Tactic:
rfl

Premises used: Equiv.sigmaCongrRight, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : α → Type u_2
F : (a : α) → Perm (β a)
⊢ Equiv.symm (sigmaCongrRight (β := β) F) = sigmaCongrRight (β := β) fun (a : α) ↦ Equiv.symm (F a)

Tactic:
rfl

Premises used: Equiv.symm, Equiv.sigmaCongrRight, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : α → Type u_2
⊢ Eq (α := Perm ((a : α) × β a)) (sigmaCongrRight (β := β) fun (a : α) ↦ Equiv.refl (β a)) (Equiv.refl ((a : α) × β a))

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u_1
β : Sort u_2
γ : α → β → Sort u_3
⊢ Bijective (α := (x : α) → (y : β) → γ x y) (swap (φ := γ))

Tactic:
functionSwap _ _ _ |>.bijective

Premises used: Equiv.bijective, Equiv.functionSwap
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β_1 : Sort v
γ : Sort w
α₁ : Type u_1
α₂ : Type u_2
β : α₂ → Type u_3
e : α₁ ≃ α₂
x : (a : α₁) × β ((e : (a : α₁) → α₂) a)
a : α₁
b : β ((e : (a : α₁) → α₂) a)
⊢ Eq (α := (a : α₁) × β ((e : (a : α₁) → α₂) a))
    ((fun (a : (a : α₂) × β a) ↦
        (Sigma.mk (β := fun (a : α₁) ↦ β ((e : (a : α₁) → α₂) a))
            ((e.symm : (a : α₂) → α₁) (a.fst (β := fun (a : α₂) ↦ β a)))
            (Eq.rec (motive := fun (x : α₂) (h : a.fst (β := fun (a : α₂) ↦ β a) = x) ↦ β x)
              (a.snd (β := fun (a : α₂) ↦ β a)) ⋯) :
          (a : α₁) × β ((e : (a : α₁) → α₂) a)))
      ((fun (a : (a : α₁) × β ((e : (a : α₁) → α₂) a)) ↦
          (Sigma.mk (β := fun (a : α₂) ↦ β a)
              ((e : (a : α₁) → α₂) (a.fst (β := fun (a : α₁) ↦ β ((e : (a : α₁) → α₂) a))))
              (a.snd (β := fun (a : α₁) ↦ β ((e : (a : α₁) → α₂) a))) :
            (a : α₂) × β a))
        (Sigma.mk (β := fun (a : α₁) ↦ β ((e : (a : α₁) → α₂) a)) a b)))
    (Sigma.mk (β := fun (a : α₁) ↦ β ((e : (a : α₁) → α₂) a)) a b)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β_1 : Sort v
γ : Sort w
α₁ : Type u_1
α₂ : Type u_2
β : α₂ → Type u_3
e : α₁ ≃ α₂
x : (a : α₂) × β a
a : α₂
b : β a
⊢ (fun (a : (a : α₁) × β ((e : (a : α₁) → α₂) a)) ↦
        (Sigma.mk (β := fun (a : α₂) ↦ β a)
            ((e : (a : α₁) → α₂) (a.fst (β := fun (a : α₁) ↦ β ((e : (a : α₁) → α₂) a))))
            (a.snd (β := fun (a : α₁) ↦ β ((e : (a : α₁) → α₂) a))) :
          (a : α₂) × β a))
      ((fun (a : (a : α₂) × β a) ↦
          (Sigma.mk (β := fun (a : α₁) ↦ β ((e : (a : α₁) → α₂) a))
              ((e.symm : (a : α₂) → α₁) (a.fst (β := fun (a : α₂) ↦ β a)))
              (Eq.rec (motive := fun (x : α₂) (h : a.fst (β := fun (a : α₂) ↦ β a) = x) ↦ β x)
                (a.snd (β := fun (a : α₂) ↦ β a)) ⋯) :
            (a : α₁) × β ((e : (a : α₁) → α₂) a)))
        (Sigma.mk (β := fun (a : α₂) ↦ β a) a b)) =
    Sigma.mk (β := fun (a : α₂) ↦ β a) a b

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
h : ∀ (a : α), q ((e : (a : α) → β) a)
a : β
⊢ q a

Tactic:
simpa using h (e.symm a)

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
e : α ≃ β
⊢ (∀ (a : α), p a) ↔ ∀ (b : β), p ((e.symm : (a : β) → α) b)

Tactic:
e.symm.forall_congr_right.symm

Premises used: Equiv.symm, Equiv.forall_congr_right, Iff.symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
⊢ (∀ (b : β), p ((e.symm : (a : β) → α) b)) ↔ ∀ (b : β), q b

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p ((e.symm : (a : β) → α) b) ↔ q b
⊢ (∀ (b : β), p ((e.symm : (a : β) → α) b)) ↔ ∀ (b : β), q b

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
h_1 : ∃ (b : β), q b
a : β
h : q a
⊢ q ((e : (a : α) → β) ((e.symm : (a : β) → α) a : α))

Tactic:
simpa using h
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
e : α ≃ β
⊢ (∃ (a : α), p a) ↔ ∃ (b : β), p ((e.symm : (a : β) → α) b)

Tactic:
e.symm.exists_congr_right.symm

Premises used: Equiv.exists_congr_right, Equiv.symm, Iff.symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
⊢ (∃ (b : β), p ((e.symm : (a : β) → α) b)) ↔ ∃ (b : β), q b

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p ((e.symm : (a : β) → α) b) ↔ q b
⊢ (∃ (b : β), p ((e.symm : (a : β) → α) b)) ↔ ∃ (b : β), q b

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : Equiv.{max 1 u, max 1 v} { a : α // p a } { b : β // q b }
⊢ (∃ (a : α), p a) ↔ ∃ (b : β), q b

Tactic:
simp [← nonempty_subtype, nonempty_congr e]

Premises used: nonempty_subtype, Equiv.nonempty_congr
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
x : α
h : q ((e : (a : α) → β) x)
⊢ ∀ (a : α),
    q ((e : (a : α) → β) a) → a = x ↔
      q ((e : (a : α) → β) a) → Eq.{v} (α := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) x : β)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
⊢ ∀ (a : α),
    ((fun (a : α) ↦ q ((e : (a : α) → β) a)) a ∧ ∀ (y : α), (fun (a : α) ↦ q ((e : (a : α) → β) a)) y → y = a) ↔
      (fun (b : β) ↦ q b) ((e : (a : α) → β) a) ∧ ∀ (y : β), (fun (b : β) ↦ q b) y → y = (e : (a : α) → β) a

Tactic:
simpa using fun _ _ ↦ e.forall_congr (by simp)

Premises used: Equiv.forall_congr
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
e : α ≃ β
⊢ (∃! a : α, p a) ↔ ∃! b : β, p ((e.symm : (a : β) → α) b)

Tactic:
e.symm.existsUnique_congr_right.symm

Premises used: Equiv.existsUnique_congr_right, Equiv.symm, Iff.symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
⊢ (∃! b : β, p ((e.symm : (a : β) → α) b)) ↔ ∃! b : β, q b

Tactic:
simp [h]