awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
b : { y : β // y ≠ x }
⊢ Eq.{u_1 + 1} (α := Option α)
    (some
        ((Equiv.symm
              ((optionSubtype x :
                  (a : { e : Option α ≃ β // (e : (a : Option α) → β) none = x }) → α ≃ { y : β // y ≠ x })
                e) :
            (a : { y : β // y ≠ x }) → α)
          b) :
      Option α)
    (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β) : Option α)
have dsimp : Eq.{u_1 + 1} (α := Option α)
  (some
      ((Equiv.symm
            (({
                  toFun :=
                    fun (e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }) ↦
                    {
                      toFun := fun (a : α) ↦
                        Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) sorry,
                      invFun := fun (b : { y : β // y ≠ x }) ↦
                        Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) sorry,
                      left_inv := sorry, right_inv := sorry },
                  invFun := fun (e : Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }) ↦
                    Subtype.mk (p := fun (e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                      (e : (a : Option α) → β) none = x)
                      {
                        toFun := fun (a : Option α) ↦
                          a.casesOn' x
                            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
                              (⇑e : (a : α) → { y : β // y ≠ x })),
                        invFun := fun (b : β) ↦
                          if h : b = x then none
                          else
                            some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)),
                        left_inv := sorry, right_inv := sorry }
                      sorry,
                  left_inv := sorry, right_inv := sorry } :
                (a : { e : Option α ≃ β // (e : (a : Option α) → β) none = x }) → α ≃ { y : β // y ≠ x })
              e) :
          (a : { y : β // y ≠ x }) → α)
        b) :
    Option α)
  (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β) : Option α)
Tactic: dsimp only [optionSubtype]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
b : { y : β // y ≠ x }
⊢ Eq.{u_1 + 1} (α := Option α)
    ((Equiv.symm
            (↑((Equiv.symm (optionSubtype x) :
                    (a : α ≃ { y : β // y ≠ x }) → { e : Option α ≃ β // (e : (a : Option α) → β) none = x })
                  e) :
              Option α ≃ β) :
          (a : β) → Option α)
        (↑b : β) :
      Option α)
    (some ((e.symm : (a : { y : β // y ≠ x }) → α) b) : Option α)
have simp : (↑b : β) = x →
  Eq.{u_1 + 1} (α := Option α) (none : Option α) (some ((e.symm : (a : { y : β // y ≠ x }) → α) b) : Option α)
Tactic: simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk,
             Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
o : Option α
⊢ (fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s)
      ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) o) =
    o
have none : Eq.{w + 1} (α := Option α)
  ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s)
    ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) none))
  none
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
o : Option α
none :
  Eq.{w + 1} (α := Option α)
    ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ Option.none) s)
      ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) Option.none))
    Option.none
⊢ (fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ Option.none) s)
      ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) o) =
    o
have some : ∀ (val : α),
  (fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ Option.none) s)
      ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) (some val)) =
    some val
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
s : α ⊕ PUnit
⊢ (fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl)
      ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) s) =
    s
have inl : ∀ (val : α),
  Eq (α := α ⊕ PUnit)
    ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl)
      ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) (inl val)))
    (inl val)
Tactic: rcases s with (_ | ⟨⟨⟩⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
s : α ⊕ PUnit
inl :
  ∀ (val : α),
    Eq (α := α ⊕ PUnit)
      ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) Sum.inl)
        ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) (Sum.inl val)))
      (Sum.inl val)
⊢ (fun (o : Option α) ↦ o.elim (inr PUnit.unit) Sum.inl)
      ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) s) =
    s
have inr : Eq (α := α ⊕ PUnit)
  ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) Sum.inl)
    ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) (inr PUnit.unit)))
  (inr PUnit.unit)
Tactic: rcases s with (_ | ⟨⟨⟩⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : x = (↑e.symm : β → α) y
⊢ (↑e : α → β) x = y
have rw : (↑e : α → β) x = (↑e : α → β) ((↑e.symm : β → α) y)
Tactic: rw [← e.right_inv hy, h]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : x = (↑e.symm : β → α) y
rw : (↑e : α → β) x = (↑e : α → β) ((↑e.symm : β → α) y)
⊢ (↑e : α → β) x = y
have rw₁ : (↑e : α → β) ((↑e.symm : β → α) y) = (↑e : α → β) ((↑e.symm : β → α) y)
Tactic: rw [← e.right_inv hy, h]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : (↑e : α → β) x = y
⊢ x = (↑e.symm : β → α) y
have rw : (↑e.symm : β → α) ((↑e : α → β) x) = (↑e.symm : β → α) y
Tactic: rw [← e.left_inv hx, h]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : (↑e : α → β) x = y
rw : (↑e.symm : β → α) ((↑e : α → β) x) = (↑e.symm : β → α) y
⊢ x = (↑e.symm : β → α) y
have rw₁ : (↑e.symm : β → α) y = (↑e.symm : β → α) y
Tactic: rw [← e.left_inv hx, h]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
s : Set α
t : Set β
h : (⇑e : (a : α) → β) '' s = t
x : β
hx : x ∈ t
⊢ Membership.mem (α := α) s ((e.symm : (a : β) → α) x : α)
have hx₁ : Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x
Tactic: subst t
Cleared hypotheses: t, h, hx
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
s : Set α
x : β
hx : Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x
⊢ Membership.mem (α := α) s ((e.symm : (a : β) → α) x : α)
have rcases : ∀ (x : α) (hx : x ∈ s), Membership.mem (α := α) s ((e.symm : (a : β) → α) ((e : (a : α) → β) x : β) : α)
Tactic: rcases hx with ⟨x, hx, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
⊢ Eq.{u_2 + 1} (α := Set β) (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) univ) univ
have rw : Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β)) univ
Tactic: rw [image_univ, e.surjective.range_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
rw : Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β)) univ
⊢ Eq.{u_2 + 1} (α := Set β) (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) univ) univ
have rw₁ : Eq.{u_2 + 1} (α := Set β) univ univ
Tactic: rw [image_univ, e.surjective.range_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
f : α → β
hf : (↑e : α → β) = f
g : β → α
hg : (↑e.symm : β → α) = g
s : Set α
hs : e.source = s
t : Set β
ht : e.target = t
⊢ e.copy f hf g hg s hs t ht = e
have substs : e.copy (↑e : α → β) sorry (↑e.symm : β → α) sorry e.source sorry e.target sorry = e
Tactic: substs f g s t
Cleared hypotheses: f, hf, g, hg, s, hs, t, ht
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.copy (↑e : α → β) ⋯ (↑e.symm : β → α) ⋯ e.source ⋯ e.target ⋯ = 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),
  { 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 α β }.copy
      (↑{ 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 α β } :
        α → β)
      sorry
      (↑{ 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 :
        β → α)
      sorry
      { 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
      sorry
      { 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
      sorry =
    { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
      map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' }
Tactic: cases e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p ((↑e : α → β) x)
have rw : (∀ (y : β), y ∈ (↑e : α → β) '' e.source → p y) ↔ ∀ (x : α), x ∈ e.source → p ((↑e : α → β) x)
Tactic: rw [← image_source_eq_target, forall_mem_image]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
rw : (∀ (y : β), y ∈ (↑e : α → β) '' e.source → p y) ↔ ∀ (x : α), x ∈ e.source → p ((↑e : α → β) x)
⊢ (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p ((↑e : α → β) x)
have rw₁ : (∀ ⦃x : α⦄, x ∈ e.source → p ((↑e : α → β) x)) ↔ ∀ (x : α), x ∈ e.source → p ((↑e : α → β) x)
Tactic: rw [← image_source_eq_target, forall_mem_image]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∃ (y : β), y ∈ e.target ∧ p y) ↔ ∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)
have rw : (∃ (y : β), y ∈ (↑e : α → β) '' e.source ∧ p y) ↔ ∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)
Tactic: rw [← image_source_eq_target, exists_mem_image]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
rw : (∃ (y : β), y ∈ (↑e : α → β) '' e.source ∧ p y) ↔ ∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)
⊢ (∃ (y : β), y ∈ e.target ∧ p y) ↔ ∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)
have rw₁ : (∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)) ↔ ∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)
Tactic: rw [← image_source_eq_target, exists_mem_image]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
x : α
hx : x ∈ e.source
⊢ (↑e.symm : β → α) ((↑e : α → β) x) ∈ s ↔ (↑e : α → β) x ∈ t
have rw : x ∈ s ↔ (↑e : α → β) x ∈ t
Tactic: rw [e.left_inv hx, h hx]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
x : α
hx : x ∈ e.source
rw : x ∈ s ↔ (↑e : α → β) x ∈ t
⊢ (↑e.symm : β → α) ((↑e : α → β) x) ∈ s ↔ (↑e : α → β) x ∈ t
have rw₁ : x ∈ s ↔ x ∈ s
Tactic: rw [e.left_inv hx, h hx]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst : (i : α) → Decidable (i ∈ s)
inst_1 : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e.source
hs : x ∈ s
⊢ t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α)
      (s.piecewise (β := fun (a : α) ↦ β) (↑e : α → β) (↑e' : α → β) x) =
    x
have inl : t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α) ((↑e : α → β) x) = x
Tactic: rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst : (i : α) → Decidable (i ∈ s)
inst_1 : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e.source
hs : x ∈ s
inl : t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α) ((↑e : α → β) x) = x
⊢ t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α)
      (s.piecewise (β := fun (a : α) ↦ β) (↑e : α → β) (↑e' : α → β) x) =
    x
have inl₁ : (↑e.symm : β → α) ((↑e : α → β) x) = x
Tactic: rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst : (i : α) → Decidable (i ∈ s)
inst_1 : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e.source
hs : x ∈ s
inl : t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α) ((↑e : α → β) x) = x
inl₁ : (↑e.symm : β → α) ((↑e : α → β) x) = x
⊢ t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α)
      (s.piecewise (β := fun (a : α) ↦ β) (↑e : α → β) (↑e' : α → β) x) =
    x
have inl₂ : x = x
Tactic: rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst : (i : α) → Decidable (i ∈ s)
inst_1 : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
⊢ t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α)
      (s.piecewise (β := fun (a : α) ↦ β) (↑e : α → β) (↑e' : α → β) x) =
    x
have inr : t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α) ((↑e' : α → β) x) = x
Tactic: rw [piecewise_eq_of_notMem _ _ _ hs, piecewise_eq_of_notMem _ _ _ ((h'.compl he).2 hs),
      e'.left_inv he]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst : (i : α) → Decidable (i ∈ s)
inst_1 : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
inr : t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α) ((↑e' : α → β) x) = x
⊢ t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α)
      (s.piecewise (β := fun (a : α) ↦ β) (↑e : α → β) (↑e' : α → β) x) =
    x
have inr₁ : (↑e'.symm : β → α) ((↑e' : α → β) x) = x
Tactic: rw [piecewise_eq_of_notMem _ _ _ hs, piecewise_eq_of_notMem _ _ _ ((h'.compl he).2 hs),
      e'.left_inv he]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst : (i : α) → Decidable (i ∈ s)
inst_1 : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
inr : t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α) ((↑e' : α → β) x) = x
inr₁ : (↑e'.symm : β → α) ((↑e' : α → β) x) = x
⊢ t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α)
      (s.piecewise (β := fun (a : α) ↦ β) (↑e : α → β) (↑e' : α → β) x) =
    x
have inr₂ : x = x
Tactic: rw [piecewise_eq_of_notMem _ _ _ hs, piecewise_eq_of_notMem _ _ _ ((h'.compl he).2 hs),
      e'.left_inv he]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t
have rw : (↑e : α → β) '' (e.source ∩ s) = e'.target ∩ t
Tactic: rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
rw : (↑e : α → β) '' (e.source ∩ s) = e'.target ∩ t
⊢ e.target ∩ t = e'.target ∩ t
have rw₁ : (↑e : α → β) '' (e.source ∩ s) = (↑e' : α → β) '' (e'.source ∩ s)
Tactic: rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
rw : (↑e : α → β) '' (e.source ∩ s) = e'.target ∩ t
rw₁ : (↑e : α → β) '' (e.source ∩ s) = (↑e' : α → β) '' (e'.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t
have rw₂ : (↑e : α → β) '' (e.source ∩ s) = (↑e' : α → β) '' (e.source ∩ s)
Tactic: rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
rw : (↑e : α → β) '' (e.source ∩ s) = e'.target ∩ t
rw₁ : (↑e : α → β) '' (e.source ∩ s) = (↑e' : α → β) '' (e'.source ∩ s)
rw₂ : (↑e : α → β) '' (e.source ∩ s) = (↑e' : α → β) '' (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t
have rw₃ : (↑e' : α → β) '' (e.source ∩ s) = (↑e' : α → β) '' (e.source ∩ s)
Tactic: rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
⊢ EqOn (↑e.symm : β → α) (↑e'.symm : β → α) (e.target ∩ t)
have rw : EqOn (↑e.symm : β → α) (↑e'.symm : β → α) ((↑e : α → β) '' (e.source ∩ s))
Tactic: rw [← h.image_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ (↑e.symm : β → α) ((↑e : α → β) x) = (↑e'.symm : β → α) ((↑e : α → β) x)
have hx'₁ : x ∈ e'.source ∩ s
Tactic: rw [hs] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ (↑e.symm : β → α) ((↑e : α → β) x) = (↑e'.symm : β → α) ((↑e : α → β) x)
have rw : x = (↑e'.symm : β → α) ((↑e : α → β) x)
Tactic: rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
rw : x = (↑e'.symm : β → α) ((↑e : α → β) x)
⊢ (↑e.symm : β → α) ((↑e : α → β) x) = (↑e'.symm : β → α) ((↑e : α → β) x)
have rw₁ : x = (↑e'.symm : β → α) ((↑e' : α → β) x)
Tactic: rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
rw : x = (↑e'.symm : β → α) ((↑e : α → β) x)
rw₁ : x = (↑e'.symm : β → α) ((↑e' : α → β) x)
⊢ (↑e.symm : β → α) ((↑e : α → β) x) = (↑e'.symm : β → α) ((↑e : α → β) x)
have rw₂ : x = x
Tactic: rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ (↑e : α → β) '' (e.source ∩ e'.source) = e.target ∩ e'.target
have rw : (↑e : α → β) '' ∅ = e.target ∩ e'.target
Tactic: rw [hs.inter_eq, ht.inter_eq, image_empty]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
rw : (↑e : α → β) '' ∅ = e.target ∩ e'.target
⊢ (↑e : α → β) '' (e.source ∩ e'.source) = e.target ∩ e'.target
have rw₁ : (↑e : α → β) '' ∅ = ∅
Tactic: rw [hs.inter_eq, ht.inter_eq, image_empty]
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
rw : (↑e : α → β) '' ∅ = e.target ∩ e'.target
rw₁ : (↑e : α → β) '' ∅ = ∅
⊢ (↑e : α → β) '' (e.source ∩ e'.source) = e.target ∩ e'.target
have rw₂ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
Tactic: rw [hs.inter_eq, ht.inter_eq, image_empty]
-- 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 : β → α) ⁻¹' s
have rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' s
Tactic: rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]