awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
x a : α
⊢ (∃ (a_1 : β), (f : (a : α) → Option β) x = some a_1 ∧ (f : (a : α) → Option β) a = some a_1) ↔
    a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_1 : β), (f : (a : α) → Option β) a = some a_1} a
have h : (∃ (a_1 : β), (f : (a : α) → Option β) x = some a_1 ∧ (f : (a : α) → Option β) a = some a_1) →
  a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_2 : β), (f : (a : α) → Option β) a = some a_2} a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
x a : α
h :
  (∃ (a_1 : β), (f : (a : α) → Option β) x = some a_1 ∧ (f : (a : α) → Option β) a = some a_1) →
    a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_2 : β), (f : (a : α) → Option β) a = some a_2} a
⊢ (∃ (a_1 : β), (f : (a : α) → Option β) x = some a_1 ∧ (f : (a : α) → Option β) a = some a_1) ↔
    a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_1 : β), (f : (a : α) → Option β) a = some a_1} a
have h₁ : a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_1 : β), (f : (a : α) → Option β) a = some a_1} a →
  ∃ (a_2 : β), (f : (a : α) → Option β) x = some a_2 ∧ (f : (a : α) → Option β) a = some a_2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
⊢ f.trans f.symm = PEquiv.refl α ↔ ∀ (a : α), isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true
have rw : (∀ (x : α), Membership.mem (γ := Set α) {a : α | isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true} x) ↔
  ∀ (a : α), isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true
Tactic: rw [self_trans_symm, ofSet_eq_refl, Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
⊢ Eq (α := α ≃. γ) (f.trans ⊥) ⊥
have h : ∀ (x : α) (a : γ), (f.trans ⊥ : (a : α) → Option γ) x = some a ↔ ((⊥ : α ≃. γ) : (a : α) → Option γ) x = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x : α
a : γ
⊢ (f.trans ⊥ : (a : α) → Option γ) x = some a ↔ ((⊥ : α ≃. γ) : (a : α) → Option γ) x = some a
have h : Option.bind.{v, w} (α := β) ((f : (a : α) → Option β) x) (⇑⊥ : (a : β) → Option γ) = some a ↔ none = some a
Tactic: dsimp [PEquiv.trans]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
⊢ Eq (α := α ≃. γ) (PEquiv.trans ⊥ f) ⊥
have h : ∀ (x : α) (a : γ), (PEquiv.trans ⊥ f : (a : α) → Option γ) x = some a ↔ ((⊥ : α ≃. γ) : (a : α) → Option γ) x = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
a : α
h : isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true
⊢ (f.symm : (a : β) → Option α) (Option.get ((f : (a : α) → Option β) a) h) = some a
have rw : (f : (a : α) → Option β) a = some (Option.get ((f : (a : α) → Option β) a) h)
Tactic: rw [f.eq_some_iff, some_get]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
a : α
h : isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true
rw : (f : (a : α) → Option β) a = some (Option.get ((f : (a : α) → Option β) a) h)
⊢ (f.symm : (a : β) → Option α) (Option.get ((f : (a : α) → Option β) a) h) = some a
have rw₁ : Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((f : (a : α) → Option β) a : Option β)
Tactic: rw [f.eq_some_iff, some_get]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
⊢ (if y = b then some a else none) = some x ↔ (if x = a then some b else none) = some y
have pos : ∀ (h1 : y = b) (h2 : x = a), some a = some x ↔ some b = some y
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
pos : ∀ (h1 : y = b) (h2 : x = a), some a = some x ↔ some b = some y
⊢ (if y = b then some a else none) = some x ↔ (if x = a then some b else none) = some y
have neg : ∀ (h1 : y = b) (h2 : ¬x = a), some a = some x ↔ False
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
pos : ∀ (h1 : y = b) (h2 : x = a), some a = some x ↔ some b = some y
neg : ∀ (h1 : y = b) (h2 : ¬x = a), some a = some x ↔ False
⊢ (if y = b then some a else none) = some x ↔ (if x = a then some b else none) = some y
have pos₁ : ∀ (h1 : ¬y = b), x = a → (False ↔ some b = some y)
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
pos : ∀ (h1 : y = b) (h2 : x = a), some a = some x ↔ some b = some y
neg : ∀ (h1 : y = b) (h2 : ¬x = a), some a = some x ↔ False
pos₁ : ∀ (h1 : ¬y = b), x = a → (False ↔ some b = some y)
⊢ (if y = b then some a else none) = some x ↔ (if x = a then some b else none) = some y
have neg₁ : ∀ (h1 : ¬y = b), ¬x = a → (False ↔ False)
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : ¬x = a
⊢ some a = some x ↔ False
have neg : ¬a = x
Tactic: simp only [some.injEq, iff_false] at *
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h : x = a
⊢ False ↔ some b = some y
have pos : ¬b = y
Tactic: simp only [some.injEq, false_iff] at *
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ Membership.mem (γ := Option β) ((single a₂ b₂ : (a : α) → Option β) a₁ : Option β) b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
have dsimp : (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂
Tactic: dsimp [single]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂
have pos : a₁ = a₂ → (b₁ ∈ some b₂ ↔ a₁ = a₂ ∧ b₁ = b₂)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
pos : a₁ = a₂ → (b₁ ∈ some b₂ ↔ a₁ = a₂ ∧ b₁ = b₂)
⊢ (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂
have neg : ¬a₁ = a₂ → (Membership.mem (γ := Option β) none b₁ ↔ a₁ = a₂ ∧ b₁ = b₂)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : Membership.mem (γ := Option γ) ((f : (a : β) → Option γ) b : Option γ) c
⊢ (single a b).trans f = single a c
have h₁ : ∀ (x : α) (a_1 : γ),
  ((single a b).trans f : (a : α) → Option γ) x = some a_1 ↔ (single a c : (a : α) → Option γ) x = some a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : Membership.mem (γ := Option γ) ((f : (a : β) → Option γ) b : Option γ) c
x : α
a_1 : γ
⊢ ((single a b).trans f : (a : α) → Option γ) x = some a_1 ↔ (single a c : (a : α) → Option γ) x = some a_1
have h₁ : (if x = a then some b else none).bind (⇑f : (a : β) → Option γ) = some a_1 ↔ (if x = a then some c else none) = some a_1
Tactic: dsimp [single, PEquiv.trans]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : Membership.mem (γ := Option γ) ((f : (a : β) → Option γ) b : Option γ) c
x : α
a_1 : γ
⊢ (if x = a then some b else none).bind (⇑f : (a : β) → Option γ) = some a_1 ↔
    (if x = a then some c else none) = some a_1
have pos : x = a → (((some b).bind fun (a : β) ↦ (f : (a : β) → Option γ) a) = some a_1 ↔ some c = some a_1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : Membership.mem (γ := Option γ) ((f : (a : β) → Option γ) b : Option γ) c
x : α
a_1 : γ
pos : x = a → (((some b).bind fun (a : β) ↦ (f : (a : β) → Option γ) a) = some a_1 ↔ some c = some a_1)
⊢ (if x = a then some b else none).bind (⇑f : (a : β) → Option γ) = some a_1 ↔
    (if x = a then some c else none) = some a_1
have neg : ¬x = a → ((Option.bind none fun (a : β) ↦ (f : (a : β) → Option γ) a) = some a_1 ↔ False)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Subsingleton α
a b : α
⊢ single a b = PEquiv.refl α
have h : ∀ (i j : α), (single a b : (a : α) → Option α) i = some j ↔ (PEquiv.refl α : (a : α) → Option α) i = some j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Subsingleton α
a b i j : α
⊢ (single a b : (a : α) → Option α) i = some j ↔ (PEquiv.refl α : (a : α) → Option α) i = some j
have h : (if i = a then some b else none) = some j ↔ some i = some j
Tactic: dsimp [single]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Subsingleton α
a b i j : α
⊢ (if i = a then some b else none) = some j ↔ some i = some j
have h : some b = some j ↔ some i = some j
Tactic: rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Subsingleton α
a b i j : α
h : some b = some j ↔ some i = some j
⊢ (if i = a then some b else none) = some j ↔ some i = some j
have h₁ : some b = some j ↔ some j = some j
Tactic: rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Subsingleton α
a b i j : α
h : some b = some j ↔ some i = some j
h₁ : some b = some j ↔ some j = some j
⊢ (if i = a then some b else none) = some j ↔ some i = some j
have h₂ : some j = some j ↔ some j = some j
Tactic: rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : Eq.{x + 1} (α := Option δ) ((f.symm : (a : β) → Option δ) b : Option δ) (none : Option δ)
⊢ f.trans (single b c) = ⊥
have h₁ : ∀ (x : δ) (a : γ),
  (f.trans (single b c) : (a : δ) → Option γ) x = some a ↔ ((⊥ : δ ≃. γ) : (a : δ) → Option γ) x = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : Eq.{x + 1} (α := Option δ) ((f.symm : (a : β) → Option δ) b : Option δ) (none : Option δ)
x : δ
a : γ
⊢ (f.trans (single b c) : (a : δ) → Option γ) x = some a ↔ ((⊥ : δ ≃. γ) : (a : δ) → Option γ) x = some a
have h₁ : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
Tactic: simp only [eq_none_iff_forall_not_mem, Option.mem_def, f.eq_some_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x : δ
a : γ
h : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
⊢ (f.trans (single b c) : (a : δ) → Option γ) x = some a ↔ ((⊥ : δ ≃. γ) : (a : δ) → Option γ) x = some a
have h₁ : (Option.bind ((f : (a : δ) → Option β) x) fun (x : β) ↦ if x = b then some c else none) = some a ↔ none = some a
Tactic: dsimp [PEquiv.trans, single]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x : δ
a : γ
h : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
⊢ (Option.bind ((f : (a : δ) → Option β) x) fun (x : β) ↦ if x = b then some c else none) = some a ↔ none = some a
have h₁ : ∀ (x_1 : β), (f : (a : δ) → Option β) x = some x_1 → ¬(if x_1 = b then some c else none) = some a
Tactic: simp only [bind_eq_some_iff, iff_false, not_exists, not_and, reduceCtorEq]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x : δ
a : γ
h : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
x_1 : β
h_1 : (f : (a : δ) → Option β) x = some x_1
⊢ ¬(if x_1 = b then some c else none) = some a
have pos : x_1 = b → ¬some c = some a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x : δ
a : γ
h : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
x_1 : β
h_1 : (f : (a : δ) → Option β) x = some x_1
pos : x_1 = b → ¬some c = some a
⊢ ¬(if x_1 = b then some c else none) = some a
have neg : ¬x_1 = b → ¬False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
gf :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
a : α
⊢ Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((g : (a : α) → Option β) a : Option β)
have none : ∀ (h : Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) (none : Option β)),
  Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) (none : Option β)
Tactic: rcases h : g a with _ | b
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
gf :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
a : α
none :
  ∀ (h : Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) (Option.none : Option β)),
    Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) (Option.none : Option β)
⊢ Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((g : (a : α) → Option β) a : Option β)
have some : ∀ (b : β) (h : (g : (a : α) → Option β) a = some b), (f : (a : α) → Option β) a = some b
Tactic: rcases h : g a with _ | b
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g : α ≃. β
a : α
b : β
⊢ (if
          Eq.{u + 1} (α := Option α) ((f.symm : (a : β) → Option α) b : Option α)
            ((g.symm : (a : β) → Option α) b : Option α) then
        (f.symm : (a : β) → Option α) b
      else none) =
      some a ↔
    (if Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((g : (a : α) → Option β) a : Option β) then
        (f : (a : α) → Option β) a
      else none) =
      some b
have hf : Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a ↔
  Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
Tactic: have hf := @mem_iff_mem _ _ f a b
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g : α ≃. β
a : α
b : β
hf :
  Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
⊢ (if
          Eq.{u + 1} (α := Option α) ((f.symm : (a : β) → Option α) b : Option α)
            ((g.symm : (a : β) → Option α) b : Option α) then
        (f.symm : (a : β) → Option α) b
      else none) =
      some a ↔
    (if Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((g : (a : α) → Option β) a : Option β) then
        (f : (a : α) → Option β) a
      else none) =
      some b
have hg : Membership.mem (γ := Option α) ((g.symm : (a : β) → Option α) b : Option α) a ↔
  Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
Tactic: have hg := @mem_iff_mem _ _ g a b
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g : α ≃. β
a : α
b : β
hf :
  Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
hg :
  Membership.mem (γ := Option α) ((g.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
⊢ (if
          Eq.{u + 1} (α := Option α) ((f.symm : (a : β) → Option α) b : Option α)
            ((g.symm : (a : β) → Option α) b : Option α) then
        (f.symm : (a : β) → Option α) b
      else none) =
      some a ↔
    (if Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((g : (a : α) → Option β) a : Option β) then
        (f : (a : α) → Option β) a
      else none) =
      some b
have hf₁ : (f.symm : (a : β) → Option α) b = some a ↔ (f : (a : α) → Option β) a = some b
Tactic: simp only [Option.mem_def] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g : α ≃. β
a : α
b : β
hf :
  Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
hg :
  Membership.mem (γ := Option α) ((g.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
hf₁ : (f.symm : (a : β) → Option α) b = some a ↔ (f : (a : α) → Option β) a = some b
⊢ (if
          Eq.{u + 1} (α := Option α) ((f.symm : (a : β) → Option α) b : Option α)
            ((g.symm : (a : β) → Option α) b : Option α) then
        (f.symm : (a : β) → Option α) b
      else none) =
      some a ↔
    (if Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((g : (a : α) → Option β) a : Option β) then
        (f : (a : α) → Option β) a
      else none) =
      some b
have hg₁ : (g.symm : (a : β) → Option α) b = some a ↔ (g : (a : α) → Option β) a = some b
Tactic: simp only [Option.mem_def] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
⊢ Membership.mem (γ := Option β)
      (({
              toFun := fun (a : α) ↦
                if
                    Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) a : Option β)
                      ((x_1 : (a : α) → Option β) a : Option β) then
                  (x : (a : α) → Option β) a
                else none,
              invFun := fun (b : β) ↦
                if
                    Eq.{u + 1} (α := Option α) ((x.symm : (a : β) → Option α) b : Option α)
                      ((x_1.symm : (a : β) → Option α) b : Option α) then
                  (x.symm : (a : β) → Option α) b
                else none,
              inv := ⋯ } :
            (a : α) → Option β)
          x_2 :
        Option β)
      x_3 →
    Membership.mem (γ := Option β) ((x : (a : α) → Option β) x_2 : Option β) x_3
have simp : (if
        Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
          ((x_1 : (a : α) → Option β) x_2 : Option β) then
      (x : (a : α) → Option β) x_2
    else none) =
    some x_3 →
  (x : (a : α) → Option β) x_2 = some x_3
Tactic: simp only [coe_mk, mem_def]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
⊢ (if
          Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
            ((x_1 : (a : α) → Option β) x_2 : Option β) then
        (x : (a : α) → Option β) x_2
      else none) =
      some x_3 →
    (x : (a : α) → Option β) x_2 = some x_3
have pos : Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
  (x : (a : α) → Option β) x_2 = some x_3 → (x : (a : α) → Option β) x_2 = some x_3
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
pos :
  Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
    (x : (a : α) → Option β) x_2 = some x_3 → (x : (a : α) → Option β) x_2 = some x_3
⊢ (if
          Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
            ((x_1 : (a : α) → Option β) x_2 : Option β) then
        (x : (a : α) → Option β) x_2
      else none) =
      some x_3 →
    (x : (a : α) → Option β) x_2 = some x_3
have neg : ¬Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
  False → (x : (a : α) → Option β) x_2 = some x_3
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
⊢ Membership.mem (γ := Option β)
      (({
              toFun := fun (a : α) ↦
                if
                    Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) a : Option β)
                      ((x_1 : (a : α) → Option β) a : Option β) then
                  (x : (a : α) → Option β) a
                else none,
              invFun := fun (b : β) ↦
                if
                    Eq.{u + 1} (α := Option α) ((x.symm : (a : β) → Option α) b : Option α)
                      ((x_1.symm : (a : β) → Option α) b : Option α) then
                  (x.symm : (a : β) → Option α) b
                else none,
              inv := ⋯ } :
            (a : α) → Option β)
          x_2 :
        Option β)
      x_3 →
    Membership.mem (γ := Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) x_3
have simp : (if
        Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
          ((x_1 : (a : α) → Option β) x_2 : Option β) then
      (x : (a : α) → Option β) x_2
    else none) =
    some x_3 →
  (x_1 : (a : α) → Option β) x_2 = some x_3
Tactic: simp only [coe_mk, mem_def]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
⊢ (if
          Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
            ((x_1 : (a : α) → Option β) x_2 : Option β) then
        (x : (a : α) → Option β) x_2
      else none) =
      some x_3 →
    (x_1 : (a : α) → Option β) x_2 = some x_3
have pos : Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
  (x : (a : α) → Option β) x_2 = some x_3 → (x_1 : (a : α) → Option β) x_2 = some x_3
Tactic: split_ifs