awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
h :
  ∀ (x : α) (y : δ),
    ((↑((e.prod e').trans (f.prod f')) : α × δ → γ × ε) (x, y)).1 =
      ((↑((e.trans f).prod (e'.trans f')) : α × δ → γ × ε) (x, y)).1
h₁ :
  ∀ (x : α) (y : δ),
    ((↑((e.prod e').trans (f.prod f')) : α × δ → γ × ε) (x, y)).2 =
      ((↑((e.trans f).prod (e'.trans f')) : α × δ → γ × ε) (x, y)).2
hsymm :
  ∀ (x : γ) (y : ε),
    ((↑((e.prod e').trans (f.prod f')).symm : γ × ε → α × δ) (x, y)).1 =
      ((↑((e.trans f).prod (e'.trans f')).symm : γ × ε → α × δ) (x, y)).1
hsymm₁ :
  ∀ (x : γ) (y : ε),
    ((↑((e.prod e').trans (f.prod f')).symm : γ × ε → α × δ) (x, y)).2 =
      ((↑((e.trans f).prod (e'.trans f')).symm : γ × ε → α × δ) (x, y)).2
hs :
  ∀ (x : α) (y : δ), (x, y) ∈ ((e.prod e').trans (f.prod f')).source ↔ (x, y) ∈ ((e.trans f).prod (e'.trans f')).source
⊢ (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ ((↑((e.prod e').trans (f.prod f')) : α × δ → γ × ε) (x, y)).1 =
    ((↑((e.trans f).prod (e'.trans f')) : α × δ → γ × ε) (x, y)).1

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ ((↑((e.prod e').trans (f.prod f')) : α × δ → γ × ε) (x, y)).2 =
    ((↑((e.trans f).prod (e'.trans f')) : α × δ → γ × ε) (x, y)).2

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : γ
y : ε
⊢ ((↑((e.prod e').trans (f.prod f')).symm : γ × ε → α × δ) (x, y)).1 =
    ((↑((e.trans f).prod (e'.trans f')).symm : γ × ε → α × δ) (x, y)).1

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : γ
y : ε
⊢ ((↑((e.prod e').trans (f.prod f')).symm : γ × ε → α × δ) (x, y)).2 =
    ((↑((e.trans f).prod (e'.trans f')).symm : γ × ε → α × δ) (x, y)).2

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
hs :
  (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source ↔
    (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source
⊢ (x, y) ∈ ((e.prod e').trans (f.prod f')).source ↔ (x, y) ∈ ((e.trans f).prod (e'.trans f')).source

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
hs :
  (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source →
    (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₁ :
  (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source →
    (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₂ hs₃ :
  x ∈ e.source →
    y ∈ e'.source →
      (↑e : α → β) x ∈ f.source →
        (↑e' : δ → η) y ∈ f'.source →
          (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₄ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → x ∈ e.source
hs₅ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → (↑e : α → β) x ∈ f.source
hs₆ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → y ∈ e'.source
hs₇ :
  x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → (↑e' : δ → η) y ∈ f'.source
hs₈ hs₉ :
  x ∈ e.source →
    (↑e : α → β) x ∈ f.source →
      y ∈ e'.source →
        (↑e' : δ → η) y ∈ f'.source →
          (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₁₀ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → x ∈ e.source
hs₁₁ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → y ∈ e'.source
hs₁₂ :
  x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → (↑e : α → β) x ∈ f.source
hs₁₃ :
  x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → (↑e' : δ → η) y ∈ f'.source
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source ↔
    (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source

Tactic:
tauto
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
s : Set α
t : Set β
inst : (x : α) → Decidable (x ∈ s)
inst_1 : (y : β) → Decidable (y ∈ t)
H : e.IsImage s t
H' : e'.IsImage s t
⊢ (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s ⋯ ⋯

Tactic:
rfl

Premises used: Set.ite, PartialEquiv.symm, Set.piecewise, PartialEquiv.piecewise, rfl, ite
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
inst : (x : α) → Decidable (x ∈ e.source)
inst_1 : (y : β) → Decidable (y ∈ e.target)
⊢ e.disjointUnion e' hs ht = e.piecewise e' e.source e.target ⋯ ⋯

Tactic:
copy_eq ..

Premises used: PartialEquiv.copy_eq, PartialEquiv.disjointUnion
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
ei : (i : ι) → PartialEquiv.{u_6, u_7} (αi i) (βi i)
⊢ (PartialEquiv.pi (αi := αi) (βi := βi) ei).symm = PartialEquiv.pi (αi := βi) (βi := αi) fun (i : ι) ↦ (ei i).symm

Tactic:
rfl

Premises used: Set.Mem, setOf, PartialEquiv.symm, Pi.map, PartialEquiv.pi, Set.pi, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
ei : (i : ι) → PartialEquiv.{u_6, u_7} (αi i) (βi i)
⊢ (↑(PartialEquiv.pi (αi := αi) (βi := βi) ei).symm : ((i : ι) → βi i) → (i : ι) → αi i) =
    fun (f : (i : ι) → βi i) (i : ι) ↦ (↑(ei i).symm : βi i → αi i) (f i)

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
h :
  ∀ (x : (i : ι) → αi i) (x_1 : ι),
    (↑(PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)) :
          ((i : ι) → αi i) → (i : ι) → αi i)
        x x_1 =
      (↑(PartialEquiv.refl ((i : ι) → αi i)) : ((i : ι) → αi i) → (i : ι) → αi i) x x_1
hsymm :
  ∀ (x : (i : ι) → αi i) (x_1 : ι),
    (↑(PartialEquiv.symm (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i))) :
          ((i : ι) → αi i) → (i : ι) → αi i)
        x x_1 =
      (↑(PartialEquiv.symm (PartialEquiv.refl ((i : ι) → αi i))) : ((i : ι) → αi i) → (i : ι) → αi i) x x_1
hs :
  ∀ (x : (i : ι) → αi i),
    Membership.mem (γ := Set ((i : ι) → αi i))
        (source (β := (i : ι) → αi i) (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)))
        x ↔
      Membership.mem (γ := Set ((i : ι) → αi i)) (source (PartialEquiv.refl ((i : ι) → αi i))) x
⊢ Eq (α := PartialEquiv ((i : ι) → αi i) ((i : ι) → αi i))
    (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)) (PartialEquiv.refl ((i : ι) → αi i))

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
x : (i : ι) → αi i
x_1 : ι
⊢ (↑(PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)) : ((i : ι) → αi i) → (i : ι) → αi i)
      x x_1 =
    (↑(PartialEquiv.refl ((i : ι) → αi i)) : ((i : ι) → αi i) → (i : ι) → αi i) x x_1

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
x : (i : ι) → αi i
x_1 : ι
⊢ (↑(PartialEquiv.symm (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i))) :
        ((i : ι) → αi i) → (i : ι) → αi i)
      x x_1 =
    (↑(PartialEquiv.symm (PartialEquiv.refl ((i : ι) → αi i))) : ((i : ι) → αi i) → (i : ι) → αi i) x x_1

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
x : (i : ι) → αi i
⊢ Membership.mem (γ := Set ((i : ι) → αi i))
      (source (β := (i : ι) → αi i) (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i))) x ↔
    Membership.mem (γ := Set ((i : ι) → αi i)) (source (PartialEquiv.refl ((i : ι) → αi i))) x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv.{u_6, u_7} (αi i) (βi i)
ei' : (i : ι) → PartialEquiv.{u_7, u_8} (βi i) (γi i)
h :
  ∀ (x : (i : ι) → αi i) (x_1 : ι),
    (↑((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')) :
          ((i : ι) → αi i) → (i : ι) → γi i)
        x x_1 =
      (↑(PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i)) : ((i : ι) → αi i) → (i : ι) → γi i)
        x x_1
hsymm :
  ∀ (x : (i : ι) → γi i) (x_1 : ι),
    (↑((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')).symm :
          ((i : ι) → γi i) → (i : ι) → αi i)
        x x_1 =
      (↑(PartialEquiv.symm (PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i))) :
          ((i : ι) → γi i) → (i : ι) → αi i)
        x x_1
hs :
  ∀ (x : (i : ι) → αi i),
    x ∈ ((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')).source ↔
      Membership.mem (γ := Set ((i : ι) → αi i))
        (source (β := (i : ι) → γi i) (PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i))) x
⊢ (PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei') =
    PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i)

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv.{u_6, u_7} (αi i) (βi i)
ei' : (i : ι) → PartialEquiv.{u_7, u_8} (βi i) (γi i)
x : (i : ι) → αi i
x_1 : ι
⊢ (↑((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')) :
        ((i : ι) → αi i) → (i : ι) → γi i)
      x x_1 =
    (↑(PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i)) : ((i : ι) → αi i) → (i : ι) → γi i) x
      x_1

Tactic:
simp [forall_and]

Premises used: forall_and
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv.{u_6, u_7} (αi i) (βi i)
ei' : (i : ι) → PartialEquiv.{u_7, u_8} (βi i) (γi i)
x : (i : ι) → γi i
x_1 : ι
⊢ (↑((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')).symm :
        ((i : ι) → γi i) → (i : ι) → αi i)
      x x_1 =
    (↑(PartialEquiv.symm (PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i))) :
        ((i : ι) → γi i) → (i : ι) → αi i)
      x x_1

Tactic:
simp [forall_and]

Premises used: forall_and
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv.{u_6, u_7} (αi i) (βi i)
ei' : (i : ι) → PartialEquiv.{u_7, u_8} (βi i) (γi i)
x : (i : ι) → αi i
⊢ x ∈ ((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')).source ↔
    Membership.mem (γ := Set ((i : ι) → αi i))
      (source (β := (i : ι) → γi i) (PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i))) x

Tactic:
simp [forall_and]

Premises used: forall_and
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
h : e.target = univ
⊢ e.source ⊆ univ

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
h : e.target = univ
⊢ univ ⊆ e.target

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
h : e.source = univ
⊢ Injective (↑e : α → β)

Tactic:
simpa [h] using e.injOn

Premises used: PartialEquiv.injOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
h : e.target = univ
⊢ Injective (↑e.symm : β → α)

Tactic:
e.symm.injective_of_source_eq_univ h

Premises used: PartialEquiv.symm, PartialEquiv.injective_of_source_eq_univ
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
h : e.source = univ
⊢ Surjective (↑e.symm : β → α)

Tactic:
e.symm.surjective_of_target_eq_univ h

Premises used: PartialEquiv.symm, PartialEquiv.surjective_of_target_eq_univ
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
⊢ (Equiv.refl α).toPartialEquiv = PartialEquiv.refl α

Tactic:
rfl

Premises used: PartialEquiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ e.symm.toPartialEquiv = e.toPartialEquiv.symm

Tactic:
rfl

Premises used: Equiv.toPartialEquivOfImageEq, Set.univ, setOf, PartialEquiv.symm, Equiv.toPartialEquiv, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
⊢ (e.trans e').toPartialEquiv.source = (e.toPartialEquiv.trans e'.toPartialEquiv).source

Tactic:
simp [PartialEquiv.trans_source, Equiv.toPartialEquiv]

Premises used: PartialEquiv.trans_source, Equiv.toPartialEquiv
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
f' : PartialEquiv β γ
⊢ e.transPartialEquiv f' = e.toPartialEquiv.trans f'

Tactic:
PartialEquiv.copy_eq ..

Premises used: PartialEquiv.copy_eq, Equiv.transPartialEquiv
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
f' : PartialEquiv β γ
f'' : PartialEquiv γ δ
⊢ (e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'')

Tactic:
simp only [transPartialEquiv_eq_trans, PartialEquiv.trans_assoc]

Premises used: PartialEquiv.trans_assoc, Equiv.transPartialEquiv_eq_trans
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
e' : β ≃ γ
f'' : PartialEquiv γ δ
⊢ (e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')

Tactic:
simp only [transPartialEquiv_eq_trans, PartialEquiv.trans_assoc, trans_toPartialEquiv]

Premises used: Equiv.trans_toPartialEquiv, PartialEquiv.trans_assoc, Equiv.transPartialEquiv_eq_trans
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ≃ β
g : PartialEquiv β γ
⊢ (↑(f.transPartialEquiv g) : α → γ) = (↑g : β → γ) ∘ (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ≃ β
g : PartialEquiv β γ
⊢ (↑(f.transPartialEquiv g).symm : γ → α) = (⇑f.symm : (a : β) → α) ∘ (↑g.symm : γ → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : β ≃ γ
⊢ e.transEquiv e' = e.trans e'.toPartialEquiv

Tactic:
copy_eq ..

Premises used: PartialEquiv.transEquiv, PartialEquiv.copy_eq
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
f' : β ≃ γ
f'' : γ ≃ δ
⊢ (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.trans f'')

Tactic:
simp only [transEquiv_eq_trans, trans_assoc, Equiv.trans_toPartialEquiv]

Premises used: Equiv.trans_toPartialEquiv, PartialEquiv.transEquiv_eq_trans, PartialEquiv.trans_assoc
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
f'' : γ ≃ δ
⊢ (e.trans e').transEquiv f'' = e.trans (e'.transEquiv f'')

Tactic:
simp only [transEquiv_eq_trans, trans_assoc]

Premises used: PartialEquiv.transEquiv_eq_trans, PartialEquiv.trans_assoc
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : PartialEquiv α β
g : β ≃ γ
⊢ (↑(f.transEquiv g) : α → γ) = (⇑g : (a : β) → γ) ∘ (↑f : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : PartialEquiv α β
g : β ≃ γ
⊢ (↑(f.transEquiv g).symm : γ → α) = (↑f.symm : β → α) ∘ (⇑g.symm : (a : γ) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
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
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ LeftInverse (fun (x : β ×' δ) ↦ ⟨(e₁.symm : (a : β) → α) x.fst, (e₂.symm : (a : δ) → γ) x.snd⟩) fun (x : α ×' γ) ↦
    ⟨(e₁ : (a : α) → β) x.fst, (e₂ : (a : γ) → δ) x.snd⟩

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
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
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ RightInverse (fun (x : β ×' δ) ↦ ⟨(e₁.symm : (a : β) → α) x.fst, (e₂.symm : (a : δ) → γ) x.snd⟩) fun (x : α ×' γ) ↦
    ⟨(e₁ : (a : α) → β) x.fst, (e₂ : (a : γ) → δ) x.snd⟩

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
x : α₁ × β₁
a : α₁
b : β₁
⊢ Prod.map.{u_10, u_9, u_12, u_11} (α₁ := α₂) (β₁ := β₂) (⇑e₁.symm : (a : α₂) → α₁) (⇑e₂.symm : (a : β₂) → β₁)
      (Prod.map (⇑e₁ : (a : α₁) → α₂) (⇑e₂ : (a : β₁) → β₂) (a, b)) =
    (a, b)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
x : α₂ × β₂
a : α₂
b : β₂
⊢ Prod.map.{u_9, u_10, u_11, u_12} (α₁ := α₁) (β₁ := β₁) (⇑e₁ : (a : α₁) → α₂) (⇑e₂ : (a : β₁) → β₂)
      (Prod.map (⇑e₁.symm : (a : α₂) → α₁) (⇑e₂.symm : (a : β₂) → β₁) (a, b)) =
    (a, b)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
⊢ (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm

Tactic:
rfl

Premises used: Prod.map, Equiv.symm, Equiv.prodCongr, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
⊢ Eq (α := (a : α × β) → β × α) (⇑(prodComm α β) : (a : α × β) → β × α) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
x : α × β
⊢ (prodComm α β : (a : α × β) → β × α) x = x.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
⊢ (prodComm α β).symm = prodComm β α

Tactic:
rfl

Premises used: Equiv.prodComm, Prod.swap, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
δ : Type u_12
⊢ (prodProdProdComm α β γ δ).symm = prodProdProdComm α γ β δ

Tactic:
rfl

Premises used: Equiv.prodProdProdComm, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
inst : Unique β
⊢ Eq (α := (a : α × β) → α) (⇑(prodUnique α β) : (a : α × β) → α) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
inst : Unique β
x : α × β
⊢ (prodUnique α β : (a : α × β) → α) x = x.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
inst : Unique β
x : α
⊢ Eq (α := α × β) (((prodUnique α β).symm : (a : α) → α × β) x : α × β) ((x, default) : α × β)

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
inst : Unique β
⊢ Eq (α := (a : β × α) → α) (⇑(uniqueProd α β) : (a : β × α) → α) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
inst : Unique β
x : β × α
⊢ (uniqueProd α β : (a : β × α) → α) x = x.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
inst : Unique β
x : α
⊢ Eq (α := β × α) (((uniqueProd α β).symm : (a : α) → β × α) x : β × α) ((default, x) : β × α)

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_10
β : α → Type u_9
inst : (a : α) → Unique (β a)
⊢ Eq (α := (a : (a : α) × β a) → α) (⇑(sigmaUnique α β) : (a : (a : α) × β a) → α) (Sigma.fst (β := fun (a : α) ↦ β a))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_10
β : α → Type u_9
inst : (a : α) → Unique (β a)
x : (a : α) × β a
⊢ (sigmaUnique α β : (a : (a : α) × β a) → α) x = x.fst (β := fun (a : α) ↦ β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_10
β : α → Type u_9
inst : (a : α) → Unique (β a)
x : α
⊢ Eq (α := (a : α) × β a) (((sigmaUnique α β).symm : (a : α) → (a : α) × β a) x : (a : α) × β a)
    (Sigma.mk (β := fun (a : α) ↦ β a) x default : (a : α) × β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_10
β : α → Type u_9
inst : Unique α
x : (a : α) × β a
⊢ Eq.{u_9 + 1} (α := β default) ((uniqueSigma β : (a : (i : α) × β i) → β default) x : β default)
    (@Eq.rec _ _ (fun (x_1 : α) (x : x.fst (β := fun (a : α) ↦ β a) = x_1) ↦ β x_1) (x.snd (β := fun (a : α) ↦ β a))
        default ⋯ :
      β default)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_10
β : α → Type u_9
inst : Unique α
y : β default
⊢ (Equiv.symm (uniqueSigma β) : (a : β default) → (i : α) × β i) y = Sigma.mk (β := fun (i : α) ↦ β i) default y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun (ab : β₂ × α₁) ↦ (((e ab.snd).symm : (a : β₂) → β₁) ab.fst, ab.snd)) fun (ab : β₁ × α₁) ↦
    ((e ab.snd : (a : β₁) → β₂) ab.fst, ab.snd)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ RightInverse (fun (ab : β₂ × α₁) ↦ (((e ab.snd).symm : (a : β₂) → β₁) ab.fst, ab.snd)) fun (ab : β₁ × α₁) ↦
    ((e ab.snd : (a : β₁) → β₂) ab.fst, ab.snd)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
b : β₁
a : α₁
⊢ Eq (α := β₂ × α₁) ((prodCongrLeft e : (a : β₁ × α₁) → β₂ × α₁) (b, a) : β₂ × α₁)
    (((e a : (a : β₁) → β₂) b, a) : β₂ × α₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : β₁ ≃ β₂
⊢ e.prodCongr (Equiv.refl α₁) = prodCongrLeft fun (x : α₁) ↦ e

Tactic:
rfl

Premises used: Prod.map, Equiv.prodCongrLeft, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrLeft e).symm = prodCongrLeft (Equiv.symm ∘ e)

Tactic:
rfl

Premises used: Equiv.prodCongrLeft, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun (ab : α₁ × β₂) ↦ (ab.fst, ((e ab.fst).symm : (a : β₂) → β₁) ab.snd)) fun (ab : α₁ × β₁) ↦
    (ab.fst, (e ab.fst : (a : β₁) → β₂) ab.snd)

Tactic:
grind