awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
h : ∀ (x : β × δ), ((↑(e.prod e').symm : β × δ → α × γ) x).1 = ((↑(e.symm.prod e'.symm) : β × δ → α × γ) x).1
h₁ : ∀ (x : β × δ), ((↑(e.prod e').symm : β × δ → α × γ) x).2 = ((↑(e.symm.prod e'.symm) : β × δ → α × γ) x).2
hsymm :
  ∀ (x : α × γ), ((↑(e.prod e').symm.symm : α × γ → β × δ) x).1 = ((↑(e.symm.prod e'.symm).symm : α × γ → β × δ) x).1
⊢ (e.prod e').symm = e.symm.prod e'.symm
have hsymm₁ : ∀ (x : α × γ), ((↑(e.prod e').symm.symm : α × γ → β × δ) x).2 = ((↑(e.symm.prod e'.symm).symm : α × γ → β × δ) x).2
Tactic: ext x
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
h : ∀ (x : β × δ), ((↑(e.prod e').symm : β × δ → α × γ) x).1 = ((↑(e.symm.prod e'.symm) : β × δ → α × γ) x).1
h₁ : ∀ (x : β × δ), ((↑(e.prod e').symm : β × δ → α × γ) x).2 = ((↑(e.symm.prod e'.symm) : β × δ → α × γ) x).2
hsymm :
  ∀ (x : α × γ), ((↑(e.prod e').symm.symm : α × γ → β × δ) x).1 = ((↑(e.symm.prod e'.symm).symm : α × γ → β × δ) x).1
hsymm₁ :
  ∀ (x : α × γ), ((↑(e.prod e').symm.symm : α × γ → β × δ) x).2 = ((↑(e.symm.prod e'.symm).symm : α × γ → β × δ) x).2
⊢ (e.prod e').symm = e.symm.prod e'.symm
have hs : ∀ (x : β × δ), x ∈ (e.prod e').symm.source ↔ x ∈ (e.symm.prod e'.symm).source
Tactic: ext x
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
⊢ (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)
have h : ∀ (x : α) (y : β),
  ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).1 =
    ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).1
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
h :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).1 =
      ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).1
⊢ (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)
have h₁ : ∀ (x : α) (y : β),
  ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).2 =
    ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).2
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
h :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).1 =
      ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).1
h₁ :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).2 =
      ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).2
⊢ (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)
have hsymm : ∀ (x : α) (y : β),
  ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm : α × β → α × β) (x, y)).1 =
    ((↑(PartialEquiv.symm (PartialEquiv.refl (α × β))) : α × β → α × β) (x, y)).1
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
h :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).1 =
      ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).1
h₁ :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).2 =
      ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).2
hsymm :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm : α × β → α × β) (x, y)).1 =
      ((↑(PartialEquiv.symm (PartialEquiv.refl (α × β))) : α × β → α × β) (x, y)).1
⊢ (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)
have hsymm₁ : ∀ (x : α) (y : β),
  ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm : α × β → α × β) (x, y)).2 =
    ((↑(PartialEquiv.symm (PartialEquiv.refl (α × β))) : α × β → α × β) (x, y)).2
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
h :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).1 =
      ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).1
h₁ :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).2 =
      ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).2
hsymm :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm : α × β → α × β) (x, y)).1 =
      ((↑(PartialEquiv.symm (PartialEquiv.refl (α × β))) : α × β → α × β) (x, y)).1
hsymm₁ :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm : α × β → α × β) (x, y)).2 =
      ((↑(PartialEquiv.symm (PartialEquiv.refl (α × β))) : α × β → α × β) (x, y)).2
⊢ (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)
have hs : ∀ (x : α) (y : β),
  (x, y) ∈ ((PartialEquiv.refl α).prod (PartialEquiv.refl β)).source ↔
    Membership.mem (γ := Set (α × β)) (source (PartialEquiv.refl (α × β))) (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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 η ε
⊢ (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
have h : ∀ (x : α) (y : δ),
  ((↑((e.prod e').trans (f.prod f')) : α × δ → γ × ε) (x, y)).1 =
    ((↑((e.trans f).prod (e'.trans f')) : α × δ → γ × ε) (x, y)).1
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
have h₁ : ∀ (x : α) (y : δ),
  ((↑((e.prod e').trans (f.prod f')) : α × δ → γ × ε) (x, y)).2 =
    ((↑((e.trans f).prod (e'.trans f')) : α × δ → γ × ε) (x, y)).2
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
have 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
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
have 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
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
have hs : ∀ (x : α) (y : δ), (x, y) ∈ ((e.prod e').trans (f.prod f')).source ↔ (x, y) ∈ ((e.trans f).prod (e'.trans f')).source
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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 : δ
⊢ (x, y) ∈ ((e.prod e').trans (f.prod f')).source ↔ (x, y) ∈ ((e.trans f).prod (e'.trans f')).source
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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 : δ
⊢ (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
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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 ∈ 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
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (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
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (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
have hs₄ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → x ∈ e.source
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (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
have hs₅ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → (↑e : α → β) x ∈ f.source
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (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
have hs₆ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → y ∈ e'.source
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (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
have hs₇ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → (↑e' : δ → η) y ∈ f'.source
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (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
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (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
have hs₁₀ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → x ∈ e.source
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ (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
have hs₁₁ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → y ∈ e'.source
Tactic: tauto