awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' s
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ (↑e.symm : β → α) ⁻¹' s
have rw₁ : (↑e.symm : β → α) ⁻¹' s ∩ (↑e : α → β) '' e.source = e.target ∩ (↑e.symm : β → α) ⁻¹' s
Tactic: rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' s
rw₁ : (↑e.symm : β → α) ⁻¹' s ∩ (↑e : α → β) '' e.source = e.target ∩ (↑e.symm : β → α) ⁻¹' s
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ (↑e.symm : β → α) ⁻¹' s
have rw₂ : (↑e.symm : β → α) ⁻¹' s ∩ e.target = e.target ∩ (↑e.symm : β → α) ⁻¹' s
Tactic: rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' s
rw₁ : (↑e.symm : β → α) ⁻¹' s ∩ (↑e : α → β) '' e.source = e.target ∩ (↑e.symm : β → α) ⁻¹' s
rw₂ : (↑e.symm : β → α) ⁻¹' s ∩ e.target = e.target ∩ (↑e.symm : β → α) ⁻¹' s
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ (↑e.symm : β → α) ⁻¹' s
have rw₃ : e.target ∩ (↑e.symm : β → α) ⁻¹' s = e.target ∩ (↑e.symm : β → α) ⁻¹' s
Tactic: rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ (↑e.symm : β → α) ⁻¹' (e.source ∩ s)
have rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
Tactic: rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ (↑e.symm : β → α) ⁻¹' (e.source ∩ s)
have rw₁ : (↑e.symm : β → α) ⁻¹' (s ∩ e.source) ∩ (↑e : α → β) '' e.source = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
Tactic: rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
rw₁ : (↑e.symm : β → α) ⁻¹' (s ∩ e.source) ∩ (↑e : α → β) '' e.source = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ (↑e.symm : β → α) ⁻¹' (e.source ∩ s)
have rw₂ : (↑e.symm : β → α) ⁻¹' (s ∩ e.source) ∩ e.target = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
Tactic: rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
rw₁ : (↑e.symm : β → α) ⁻¹' (s ∩ e.source) ∩ (↑e : α → β) '' e.source = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
rw₂ : (↑e.symm : β → α) ⁻¹' (s ∩ e.source) ∩ e.target = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ (↑e.symm : β → α) ⁻¹' (e.source ∩ s)
have rw₃ : e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
Tactic: rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ (↑e : α → β) '' s = e.target ∩ (↑e.symm : β → α) ⁻¹' s
have rw : (↑e : α → β) '' s = (↑e : α → β) '' (e.source ∩ s)
Tactic: rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
rw : (↑e : α → β) '' s = (↑e : α → β) '' (e.source ∩ s)
⊢ (↑e : α → β) '' s = e.target ∩ (↑e.symm : β → α) ⁻¹' s
have rw₁ : (↑e : α → β) '' s = (↑e : α → β) '' s
Tactic: rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
⊢ e = e'
have A : (↑e : α → β) = (↑e' : α → β)
Tactic: have A : (e : α → β) = e' := by
    ext x
    exact h x
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
⊢ e = e'
have B : (↑e.symm : β → α) = (↑e'.symm : β → α)
Tactic: have B : (e.symm : β → α) = e'.symm := by
    ext x
    exact hsymm x
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
B : (↑e.symm : β → α) = (↑e'.symm : β → α)
⊢ e = e'
have I : (↑e : α → β) '' e.source = e.target
Tactic: have I : e '' e.source = e.target := e.image_source_eq_target
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
B : (↑e.symm : β → α) = (↑e'.symm : β → α)
I : (↑e : α → β) '' e.source = e.target
⊢ e = e'
have I' : (↑e' : α → β) '' e'.source = e'.target
Tactic: have I' : e' '' e'.source = e'.target := e'.image_source_eq_target
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
B : (↑e.symm : β → α) = (↑e'.symm : β → α)
I : (↑e : α → β) '' e.source = e.target
I' : (↑e' : α → β) '' e'.source = e'.target
⊢ e = e'
have I₁ : e'.target = e.target
Tactic: rw [A, hs, I'] at I
Cleared hypotheses: I, I'
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
B : (↑e.symm : β → α) = (↑e'.symm : β → α)
I : e'.target = e.target
I' : (↑e' : α → β) '' e'.source = e'.target
⊢ e = e'
have mk : ∀ (toFun : α → β) (invFun : β → α) (source : Set α) (target : Set β)
  (map_source' : ∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target) (map_target' : ∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source)
  (left_inv' : ∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x) (right_inv' : ∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x)
  (h :
    ∀ (x : α),
      (↑{ toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
                map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β } :
            α → β)
          x =
        (↑e' : α → β) x)
  (hsymm :
    ∀ (x : β),
      (↑{ toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
                  map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' :
                  PartialEquiv α β }.symm :
            β → α)
          x =
        (↑e'.symm : β → α) x)
  (hs :
    { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
          map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.source =
      e'.source)
  (A :
    (↑{ toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
            map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β } :
        α → β) =
      (↑e' : α → β))
  (B :
    (↑{ toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
              map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.symm :
        β → α) =
      (↑e'.symm : β → α))
  (I :
    e'.target =
      { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
          map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.target),
  { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
      map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β } =
    e'
Tactic: cases e
Cleared hypotheses: e, h, hsymm, hs, A, B, I
-- 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 β γ
a : α
b : β
a' : α
ha' : Membership.mem (γ := Set α) {a} a'
⊢ const β a (const α b a') = a'
have rw : const β a (const α b a) = a
Tactic: rw [eq_of_mem_singleton ha', const_apply]
-- 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 β γ
a : α
b : β
a' : α
ha' : Membership.mem (γ := Set α) {a} a'
rw : const β a (const α b a) = a
⊢ const β a (const α b a') = a'
have rw₁ : a = a
Tactic: rw [eq_of_mem_singleton ha', const_apply]
-- 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 β γ
a : α
b b' : β
hb' : Membership.mem (γ := Set β) {b} b'
⊢ const α b (const β a b') = b'
have rw : const α b (const β a b) = b
Tactic: rw [eq_of_mem_singleton hb', const_apply]
-- 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 β γ
a : α
b b' : β
hb' : Membership.mem (γ := Set β) {b} b'
rw : const α b (const β a b) = b
⊢ const α b (const β a b') = b'
have rw₁ : b = b
Tactic: rw [eq_of_mem_singleton hb', const_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').source = e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source)
have h : ∀ (x : α), x ∈ (e.trans e').source ↔ x ∈ e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source)
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').source = (↑e.symm : β → α) '' (e.target ∩ e'.source)
have rw : e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source) = (↑e.symm : β → α) '' (e.target ∩ e'.source)
Tactic: rw [e.trans_source', e.symm_image_target_inter_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
rw : e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source) = (↑e.symm : β → α) '' (e.target ∩ e'.source)
⊢ (e.trans e').source = (↑e.symm : β → α) '' (e.target ∩ e'.source)
have rw₁ : e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source) = e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source)
Tactic: rw [e.trans_source', e.symm_image_target_inter_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ (e.trans ((PartialEquiv.refl β).restr s)).source = (e.restr (e.source ∩ (↑e : α → β) ⁻¹' s)).source
have simp : e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ (e.source ∩ (↑e : α → β) ⁻¹' s)
Tactic: simp only [trans_source, restr_source, refl_source, univ_inter]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ (e.source ∩ (↑e : α → β) ⁻¹' s)
have rw : e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ e.source ∩ (↑e : α → β) ⁻¹' s
Tactic: rw [← inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
rw : e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ e.source ∩ (↑e : α → β) ⁻¹' s
⊢ e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ (e.source ∩ (↑e : α → β) ⁻¹' s)
have rw₁ : e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ (↑e : α → β) ⁻¹' s
Tactic: rw [← inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
⊢ (↑e : α → β) x ∈ (↑e.symm.symm.symm : β → α) ⁻¹' e'.source
have rwa : (↑e.symm.symm.symm : β → α) ((↑e : α → β) x) ∈ e'.source
Tactic: rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
rwa : (↑e.symm.symm.symm : β → α) ((↑e : α → β) x) ∈ e'.source
⊢ (↑e : α → β) x ∈ (↑e.symm.symm.symm : β → α) ⁻¹' e'.source
have rwa₁ : (↑e.symm : β → α) ((↑e : α → β) x) ∈ e'.source
Tactic: rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]
-- 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 β γ
⊢ Equivalence (α := PartialEquiv α β) EqOnSource
have refl : ∀ (x : PartialEquiv α β), x.EqOnSource x
Tactic: constructor
-- 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 β γ
refl : ∀ (x : PartialEquiv α β), x.EqOnSource x
⊢ Equivalence (α := PartialEquiv α β) EqOnSource
have symm : ∀ {x y : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource x
Tactic: constructor
-- 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 β γ
refl : ∀ (x : PartialEquiv α β), x.EqOnSource x
symm : ∀ {x y : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource x
⊢ Equivalence (α := PartialEquiv α β) EqOnSource
have trans : ∀ {x y z : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource z → x.EqOnSource z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ e.symm ≈ e'.symm
have refine_1 : RightInvOn (↑e'.symm : β → α) (↑e : α → β) e.symm.source
Tactic: refine ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
refine_1 : RightInvOn (↑e'.symm : β → α) (↑e : α → β) e.symm.source
⊢ e.symm ≈ e'.symm
have refine_2 : MapsTo (↑e'.symm : β → α) e.symm.source e.source
Tactic: refine ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑e'.symm : β → α) (↑e : α → β) e.symm.source
have refine_1 : RightInvOn (↑e'.symm : β → α) (↑e : α → β) e'.target
Tactic: simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ e.trans f ≈ e'.trans f'
have left : (e.trans f).source = (e'.trans f').source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
left : (e.trans f).source = (e'.trans f').source
⊢ e.trans f ≈ e'.trans f'
have right : EqOn (↑(e.trans f) : α → γ) (↑(e'.trans f') : α → γ) (e.trans f).source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (e.trans f).source = (e'.trans f').source
have left : (↑e.symm : β → α) '' (e.target ∩ f.source) = (↑e'.symm : β → α) '' (e.target ∩ f.source)
Tactic: rw [trans_source'', trans_source'', ← target_eq he, ← hf.1]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ (e.trans f).source
⊢ (↑(e.trans f) : α → γ) x = (↑(e'.trans f') : α → γ) x
have hx₁ : x ∈ e.source ∩ (↑e : α → β) ⁻¹' f.source
Tactic: rw [trans_source] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ e.restr s ≈ e'.restr s
have left : (e.restr s).source = (e'.restr s).source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
left : (e.restr s).source = (e'.restr s).source
⊢ e.restr s ≈ e'.restr s
have right : EqOn (↑(e.restr s) : α → β) (↑(e'.restr s) : α → β) (e.restr s).source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ (e.restr s).source
⊢ (↑(e.restr s) : α → β) x = (↑(e'.restr s) : α → β) x
have hx₁ : x ∈ e.source ∧ x ∈ s
Tactic: simp only [mem_inter_iff, restr_source] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set β
⊢ e.source ∩ (↑e : α → β) ⁻¹' s = e'.source ∩ (↑e' : α → β) ⁻¹' s
have rw : e.source ∩ (↑e' : α → β) ⁻¹' s = e'.source ∩ (↑e' : α → β) ⁻¹' s
Tactic: rw [he.eqOn.inter_preimage_eq, source_eq he]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set β
rw : e.source ∩ (↑e' : α → β) ⁻¹' s = e'.source ∩ (↑e' : α → β) ⁻¹' s
⊢ e.source ∩ (↑e : α → β) ⁻¹' s = e'.source ∩ (↑e' : α → β) ⁻¹' s
have rw₁ : e'.source ∩ (↑e' : α → β) ⁻¹' s = e'.source ∩ (↑e' : α → β) ⁻¹' s
Tactic: rw [he.eqOn.inter_preimage_eq, source_eq he]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (e.trans e.symm).source = e.source
have h : ∀ (x : α), x ∈ (e.trans e.symm).source ↔ x ∈ e.source
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.trans e.symm ≈ ofSet e.source
have A : (e.trans e.symm).source = e.source
Tactic: have A : (e.trans e.symm).source = e.source := by mfld_set_tac
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
⊢ (e.trans e.symm).source = (ofSet e.source).source
have rw : e.source = (ofSet e.source).source
Tactic: rw [A, ofSet_source]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
rw : e.source = (ofSet e.source).source
⊢ (e.trans e.symm).source = (ofSet e.source).source
have rw₁ : e.source = e.source
Tactic: rw [A, ofSet_source]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
⊢ e.trans e.symm ≈ ofSet e.source
have refine : ∀ (x : α) (hx : x ∈ (e.trans e.symm).source), (↑(e.trans e.symm) : α → α) x = (↑(ofSet e.source) : α → α) x
Tactic: refine ⟨by rw [A, ofSet_source], fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ (e.trans e.symm).source
⊢ (↑(e.trans e.symm) : α → α) x = (↑(ofSet e.source) : α → α) x
have hx₁ : x ∈ e.source
Tactic: rw [A] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
⊢ e = e'
have refine_1 : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
Tactic: refine PartialEquiv.ext (fun x => ?_) (fun x => ?_) h.1
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
refine_1 : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
⊢ e = e'
have refine_2 : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
Tactic: refine PartialEquiv.ext (fun x => ?_) (fun x => ?_) h.1
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ (↑e : α → β) x = (↑e' : α → β) x
have refine_1 : x ∈ e.source
Tactic: apply h.2
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ e.source
have refine_1 : Membership.mem (γ := Set α) univ x
Tactic: rw [s]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ (↑e.symm : β → α) x = (↑e'.symm : β → α) x
have refine_2 : x ∈ e.symm.source
Tactic: apply h.symm'.2
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ e.symm.source
have refine_2 : Membership.mem (γ := Set β) univ x
Tactic: rw [symm_source, t]
-- 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 γ δ
⊢ (e.prod e').symm = e.symm.prod e'.symm
have h : ∀ (x : β × δ), ((↑(e.prod e').symm : β × δ → α × γ) x).1 = ((↑(e.symm.prod e'.symm) : β × δ → α × γ) x).1
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
⊢ (e.prod e').symm = e.symm.prod e'.symm
have h₁ : ∀ (x : β × δ), ((↑(e.prod e').symm : β × δ → α × γ) x).2 = ((↑(e.symm.prod e'.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
⊢ (e.prod e').symm = e.symm.prod e'.symm
have hsymm : ∀ (x : α × γ), ((↑(e.prod e').symm.symm : α × γ → β × δ) x).1 = ((↑(e.symm.prod e'.symm).symm : α × γ → β × δ) x).1
Tactic: ext x