awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u
inst : Inhabited α
inst_1 : DecidableEq α
a : α
pos :
  a = default →
    Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default)) none = a
⊢ Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default))
      (if h : a = default then none else some (Subtype.mk (p := fun (a : α) ↦ a ≠ default) a h)) =
    a
have neg : ∀ (h : ¬a = default),
  Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default))
      (some (Subtype.mk (p := fun (a : α) ↦ a ≠ default) a h)) =
    a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst : DecidablePred p
x : α
hx : p x
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    ((fun (a : α) ↦
        (if h : p a then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)
          else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) :
          { a : α // p a } ⊕ { a : α // ¬p a }))
      (Sum.elim (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (Subtype.val (p := fun (a : α) ↦ ¬p a))
        (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))))
    (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
have inl : Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
  (if h : p x then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x h)
  else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h))
  (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst : DecidablePred p
x : α
hx : ¬p x
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    ((fun (a : α) ↦
        (if h : p a then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)
          else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) :
          { a : α // p a } ⊕ { a : α // ¬p a }))
      (Sum.elim (α := { a : α // p a }) (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a))
        (Subtype.val (p := fun (a : α) ↦ ¬p a)) (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))))
    (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
have inr : Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
  (if h : p x then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x h)
  else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h))
  (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst : DecidablePred p
x : α
hx : p x
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (if h : p x then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x h)
    else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h))
    (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
have inl : Eq (α := { a : α // p a } ⊕ { a : α // ¬p a }) (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
  (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
Tactic: rw [dif_pos]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst : DecidablePred p
x : α
hx : ¬p x
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (if h : p x then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x h)
    else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h))
    (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
have inr : Eq (α := { a : α // p a } ⊕ { a : α // ¬p a }) (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
  (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst : DecidablePred p
a : α
⊢ Sum.elim (α := { a : α // p a }) (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a))
      (Subtype.val (p := fun (a : α) ↦ ¬p a))
      (if h : p a then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)
      else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
    a
have pos : ∀ (h : p a),
  Sum.elim (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (Subtype.val (p := fun (a : α) ↦ ¬p a))
      (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)) =
    a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst : DecidablePred p
a : α
pos :
  ∀ (h : p a),
    Sum.elim (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (Subtype.val (p := fun (a : α) ↦ ¬p a))
        (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)) =
      a
⊢ Sum.elim (α := { a : α // p a }) (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a))
      (Subtype.val (p := fun (a : α) ↦ ¬p a))
      (if h : p a then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)
      else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
    a
have neg : ∀ (h : ¬p a),
  Sum.elim (α := { a : α // p a }) (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a))
      (Subtype.val (p := fun (a : α) ↦ ¬p a)) (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
    a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_11
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)
⊢ Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
      (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inl)
      (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        p) =
    p
have inl : ∀ (i : ι) (a : α i),
  Eq (α := (i : ι) × Sum.{u_9, u_10} (α i) (β i))
    (Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
      (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inl)
      (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (inl a))))
    (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (inl a))
Tactic: rcases p with ⟨i, a | b⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_11
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)
inl :
  ∀ (i : ι) (a : α i),
    Eq (α := (i : ι) × Sum.{u_9, u_10} (α i) (β i))
      (Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
        ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
            Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
              (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
              (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (Sum.inl a))))
      (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (Sum.inl a))
⊢ Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
      (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inl)
      (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        p) =
    p
have inr : ∀ (i : ι) (b : β i),
  Eq (α := (i : ι) × Sum.{u_9, u_10} (α i) (β i))
    (Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
      (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inl)
      (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (inr b))))
    (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (inr b))
Tactic: rcases p with ⟨i, a | b⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_11
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × α i ⊕ (i : ι) × β i
⊢ (fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
        Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
      (Sum.elim
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
        p) =
    p
have inl : ∀ (i : ι) (a : α i),
  Eq (α := (i : ι) × α i ⊕ (i : ι) × β i)
    ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
        Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
      (Sum.elim (β := (i : ι) × β i)
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
        (inl (Sigma.mk (β := fun (i : ι) ↦ α i) i a))))
    (inl (Sigma.mk (β := fun (i : ι) ↦ α i) i a))
Tactic: rcases p with (⟨i, a⟩ | ⟨i, b⟩)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_11
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × α i ⊕ (i : ι) × β i
inl :
  ∀ (i : ι) (a : α i),
    Eq (α := (i : ι) × α i ⊕ (i : ι) × β i)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        (Sum.elim (β := (i : ι) × β i)
          (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦
            Sum.inl)
          (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
          (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ α i) i a))))
      (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ α i) i a))
⊢ (fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
        Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
      (Sum.elim
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
        p) =
    p
have inr : ∀ (i : ι) (b : β i),
  Eq (α := (i : ι) × α i ⊕ (i : ι) × β i)
    ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
        Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
      (Sum.elim (α := (i : ι) × α i)
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
        (inr (Sigma.mk (β := fun (i : ι) ↦ β i) i b))))
    (inr (Sigma.mk (β := fun (i : ι) ↦ β i) i b))
Tactic: rcases p with (⟨i, a⟩ | ⟨i, b⟩)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Logic.ExistsUnique (hypothesis)
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
b : Prop
h₂ : ∃! x : α, ∃! h : p x, q x h
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
⊢ b
have h₃ : ∃! x : α, ∃ (h : p x), q x h
Tactic: simp only [existsUnique_iff_exists] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Logic.ExistsUnique (goal)
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x : α, ∃ (h : p x), q x h
⊢ b
have apply : ∀ (x : α), (∃ (h : p x), q x h) → (∀ (y : α), (∃ (h : p y), q y h) → y = x) → b
Tactic: apply h₂.elim
-- Lean 4 proof step from Mathlib.Logic.ExistsUnique (goal)
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x : α, ∃! hx : p x, q x hx
have simp : ∃! x : α, ∃ (hx : p x), q x hx
Tactic: simp only [existsUnique_iff_exists]
-- Lean 4 proof step from Mathlib.Logic.ExistsUnique (hypothesis)
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
h : ∃! x : α, ∃! hx : p x, q x hx
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
⊢ y₁ = y₂
have h₁ : ∃! x : α, ∃ (hx : p x), q x hx
Tactic: simp only [existsUnique_iff_exists] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α α' : Sort u
β : α → Sort v
β' : α' → Sort v
f : (a : α) → β a
f' : (a : α') → β' a
hα : α = α'
h : ∀ (a : α) (a' : α'), a ≍ a' → f a ≍ f' a'
⊢ f ≍ f'
have subst : ∀ {β' : α → Sort v} {f' : (a : α) → β' a} (h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'), f ≍ f'
Tactic: subst hα
Cleared hypotheses: α', β', f', hα, h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
⊢ f ≍ f'
have this : ∀ (a : α), f a ≍ f' a
Tactic: have : ∀ a, f a ≍ f' a := fun a ↦ h a a (HEq.refl a)
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
⊢ β = β'
have h₁ : ∀ (a : α), β a = β' a
Tactic: funext a
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
⊢ f ≍ f'
have this₁ : β = β'
Tactic: have : β = β' := by funext a; exact type_eq_of_heq (this a)
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this_1 : ∀ (a : α), f a ≍ f' a
this : β = β'
⊢ f ≍ f'
have subst : ∀ {f' : (a : α) → β a} (h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a') (this : ∀ (a : α), f a ≍ f' a), f ≍ f'
Tactic: subst this
Cleared hypotheses: β', f', h, this_1, this
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
⊢ f x = g y ↔ f = g
have refine_1 : ∀ (h : f x = g y) (z : α), f z = g z
Tactic: refine ⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
refine_1 : ∀ (h : f x = g y) (z : α), f z = g z
⊢ f x = g y ↔ f = g
have refine_2 : ∀ (h : f = g), f x = g y
Tactic: refine ⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
⊢ f z = g z
have refine_1 : ∀ (h : f z = g y), f z = g z
Tactic: rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
refine_1 : ∀ (h : f z = g y), f z = g z
⊢ f z = g z
have refine_1₁ : ∀ (h : f z = g z), f z = g z
Tactic: rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y
have refine_2 : g x = g y
Tactic: rw [h, Subsingleton.elim x y]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
g : α → β
x y : α
h : f = g
refine_2 : g x = g y
⊢ f x = g y
have refine_2₁ : g y = g y
Tactic: rw [h, Subsingleton.elim x y]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : Nontrivial α
b : β
⊢ ¬Injective.{u_4 + 1, u_5 + 1} (β := β) fun (x : α) ↦ b
have rw : ∃ (a : α), ∃ (b_1 : α), b = b ∧ a ≠ b_1
Tactic: rw [not_injective_iff]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : Nontrivial α
b : β
⊢ ∃ (a : α), ∃ (b_1 : α), b = b ∧ a ≠ b_1
have obtain : ∀ (a₁ a₂ : α) (h : a₁ ≠ a₂), ∃ (a : α), ∃ (b_1 : α), b = b ∧ a ≠ b_1
Tactic: obtain ⟨a₁, a₂, h⟩ := exists_pair_ne α
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : α
h : f x = f y
⊢ x = y
have obtain : ∀ (x : γ) (h : f (g x) = f y), g x = y
Tactic: obtain ⟨x, rfl⟩ := hg x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
y : α
x : γ
h : f (g x) = f y
⊢ g x = y
have obtain : ∀ (y : γ) (h : f (g x) = f (g y)), g x = g y
Tactic: obtain ⟨y, rfl⟩ := hg y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
⊢ (Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Surjective f
have refine : ∀ (not_surj : ¬Surjective f) (inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
Tactic: refine ⟨not_imp_not.mp fun not_surj inj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.injective_comp_right)⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
⊢ c = c'
have have : ∀ (b₀ : β) (hb : ¬∃ (a : α), f a = b₀), c = c'
Tactic: have ⟨b₀, hb⟩ := not_forall.mp not_surj
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
⊢ c = c'
have refine_2 : ∀ (this : Eq (α := β → γ) (fun (x : β) ↦ c) fun (x : β) ↦ if x = b₀ then c' else c), c = c'
Tactic: have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
refine_2 : ∀ (this : Eq (α := β → γ) (fun (x : β) ↦ c) fun (x : β) ↦ if x = b₀ then c' else c), c = c'
⊢ c = c'
have refine_1 : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ c)
  ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ if x = b₀ then c' else c)
Tactic: have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
⊢ c = c'
have refine_2 : ∀ (this : Eq (α := β → γ) (fun (x : β) ↦ c) fun (x : β) ↦ if x = b₀ then c' else c), c = c'
Tactic: classical have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
refine_2 : ∀ (this : Eq (α := β → γ) (fun (x : β) ↦ c) fun (x : β) ↦ if x = b₀ then c' else c), c = c'
⊢ c = c'
have refine_1 : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ c)
  ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ if x = b₀ then c' else c)
Tactic: classical have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ (a : α), f a = b₀
⊢ Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ c)
    ((fun (g : β → γ) ↦ g ∘ f) fun (x : β) ↦ if x = b₀ then c' else c)
have refine_1 : ∀ (a : α),
  Eq.{u_4 + 1} (α := γ) ((fun (g : β → γ) ↦ g ∘ f) (fun (x : β) ↦ c) a)
    ((fun (g : β → γ) ↦ g ∘ f) (fun (x : β) ↦ if x = b₀ then c' else c) a)
Tactic: ext a