awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ Subset.{u_2} (α := Set β) ((⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x) (⋃ x ∈ s₁ \ s₂, t x)
have simp : Subset.{u_2} (α := Set β) (⋃ x ∈ s₁, t x) (⋃ x ∈ s₂ ∪ s₁ \ s₂, t x)
Tactic: simp only [diff_subset_iff, ← biUnion_union]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ Subset.{u_2} (α := Set β) (⋃ x ∈ s₁, t x) (⋃ x ∈ s₂ ∪ s₁ \ s₂, t x)
have h : s₁ ⊆ s₂ ∪ s₁ \ s₂
Tactic: apply biUnion_subset_biUnion_left
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂
have h : s₁ ⊆ s₂ ∪ s₁
Tactic: rw [union_diff_self]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
b₂ : β
h₂ : b₂ ∈ t a₂
eq :
  sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
    sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₂ h₂))
b_eq : b₁ = b₂
a_eq : a₁ = a₂
⊢ Eq.{u_2 + 1} (α := β)
    (↑(Eq.recOn (motive :=
          fun (x : α)
            (x_1 :
              Sigma.fst (β := fun (a : α) ↦ (↑(t a) : Type u_2))
                  (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                    (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
                x) ↦
          (↑(t x) : Type u_2)) a_eq
          (Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
            (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)))) :
      β)
    (↑(Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₂ h₂))) :
      β)
have subst : ∀ (h₂ : b₁ ∈ t a₂)
  (eq :
    sigmaToiUnion t
        (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
      sigmaToiUnion t
        (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₁ h₂))),
  Eq.{u_2 + 1} (α := β)
    (↑(Eq.recOn (motive :=
          fun (x : α)
            (x_1 :
              Sigma.fst (β := fun (a : α) ↦ (↑(t a) : Type u_2))
                  (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                    (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
                x) ↦
          (↑(t x) : Type u_2)) a_eq
          (Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
            (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)))) :
      β)
    (↑(Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₁ h₂))) :
      β)
Tactic: subst b_eq
Cleared hypotheses: b₂, h₂, eq, b_eq
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq :
  sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
    sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₁ h₂))
⊢ Eq.{u_2 + 1} (α := β)
    (↑(Eq.recOn (motive :=
          fun (x : α)
            (x_1 :
              Sigma.fst (β := fun (a : α) ↦ (↑(t a) : Type u_2))
                  (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                    (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
                x) ↦
          (↑(t x) : Type u_2)) a_eq
          (Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
            (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)))) :
      β)
    (↑(Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₁ h₂))) :
      β)
have subst : ∀ (h₂ : b₁ ∈ t a₁)
  (eq :
    sigmaToiUnion t
        (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
      sigmaToiUnion t
        (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₂))),
  Eq.{u_2 + 1} (α := β)
    (↑(Eq.recOn (motive :=
          fun (x : α)
            (x_1 :
              Sigma.fst (β := fun (a : α) ↦ (↑(t a) : Type u_2))
                  (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                    (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
                x) ↦
          (↑(t x) : Type u_2)) sorry
          (Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
            (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)))) :
      β)
    (↑(Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₂))) :
      β)
Tactic: subst a_eq
Cleared hypotheses: a₂, a_eq, h₂, eq
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (↑(⋃ (i : α), t i) : Type u_13)
| (↑(Sigma.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))
            ((unionEqSigmaOfDisjoint (t := t) h :
                (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
              x) :
          (↑(t
                (Sigma.fst (β := fun (i : α) ↦ (↑(t i) : Type u_13))
                  ((unionEqSigmaOfDisjoint (t := t) h :
                      (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
                    x))) :
            Type u_13)) :
      β) =
    (↑x : β)
have right : (↑x : β)
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (↑(⋃ (i : α), t i) : Type u_13)
| (↑x : β)
have rw : (↑(((unionEqSigmaOfDisjoint (t := t) h).symm : (a : (i : α) × (↑(t i) : Type u_13)) → (↑(⋃ (i : α), t i) : Type u_13))
      ((unionEqSigmaOfDisjoint (t := t) h : (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
        x)) :
  β)
Tactic: rw [← unionEqSigmaOfDisjoint h |>.symm_apply_apply x]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (↑(⋃ (i : α), t i) : Type u_13)
| (↑(Sigma.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))
            ((unionEqSigmaOfDisjoint (t := t) h :
                (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
              x) :
          (↑(t
                (Sigma.fst (β := fun (i : α) ↦ (↑(t i) : Type u_13))
                  ((unionEqSigmaOfDisjoint (t := t) h :
                      (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
                    x))) :
            Type u_13)) :
      β) =
    (↑x : β)
have rw : (↑(((unionEqSigmaOfDisjoint (t := t) h).symm : (a : (i : α) × (↑(t i) : Type u_13)) → (↑(⋃ (i : α), t i) : Type u_13))
      ((unionEqSigmaOfDisjoint (t := t) h : (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
        x)) :
  β)
Tactic: right; rw [← unionEqSigmaOfDisjoint h |>.symm_apply_apply x]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (↑(⋃ (i : α), t i) : Type u_13)
⊢ (↑(Sigma.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))
            ((unionEqSigmaOfDisjoint (t := t) h :
                (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
              x) :
          (↑(t
                (Sigma.fst (β := fun (i : α) ↦ (↑(t i) : Type u_13))
                  ((unionEqSigmaOfDisjoint (t := t) h :
                      (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
                    x))) :
            Type u_13)) :
      β) =
    (↑x : β)
have conv : Eq.{u_13 + 1} (α := β)
  (↑(Sigma.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))
          ((unionEqSigmaOfDisjoint (t := t) h : (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
            x) :
        (↑(t
              (Sigma.fst (β := fun (i : α) ↦ (↑(t i) : Type u_13))
                ((unionEqSigmaOfDisjoint (t := t) h :
                    (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
                  x))) :
          Type u_13)) :
    β)
  (↑(((unionEqSigmaOfDisjoint (t := t) h).symm : (a : (i : α) × (↑(t i) : Type u_13)) → (↑(⋃ (i : α), t i) : Type u_13))
        ((unionEqSigmaOfDisjoint (t := t) h : (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
          x)) :
    β)
Tactic: conv => right; rw [← unionEqSigmaOfDisjoint h |>.symm_apply_apply x]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : CompleteLattice β
s : ι → Set α
f : α → β
⊢ Eq.{u_2 + 1} (α := β) (⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a), f a)
    (⨆ (i : ι), ⨆ a ∈ s i, f a)
have rw : Eq.{u_2 + 1} (α := β) (⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a), f a)
  (⨆ (j : α), ⨆ (i : ι), ⨆ (_ : j ∈ s i), f j)
Tactic: rw [iSup_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : CompleteLattice β
s : ι → Set α
f : α → β
⊢ Eq.{u_2 + 1} (α := β) (⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a), f a)
    (⨆ (j : α), ⨆ (i : ι), ⨆ (_ : j ∈ s i), f j)
have simp_rw : Eq.{u_2 + 1} (α := β) (⨆ (a : α), ⨆ (_ : ∃ (i : ι), a ∈ s i), f a) (⨆ (j : α), ⨆ (i : ι), ⨆ (_ : j ∈ s i), f j)
Tactic: simp_rw [mem_iUnion, iSup_exists]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
β : Type u_2
ι : Sort u_5
inst : CompleteLattice β
t : ι → Set β
⊢ Eq.{u_2 + 1} (α := β) (sSup (⋃ (i : ι), t i)) (⨆ (i : ι), sSup (t i))
have simp_rw : Eq.{u_2 + 1} (α := β) (⨆ (a : β), ⨆ (_ : Membership.mem (γ := Set β) (⋃ (i : ι), t i) a), a) (⨆ (i : ι), ⨆ a ∈ t i, a)
Tactic: simp_rw [sSup_eq_iSup, iSup_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ Eq.{u_2 + 1} (α := β) (⨆ x ∈ ⋃₀ S, f x) (⨆ s ∈ S, ⨆ x ∈ s, f x)
have rw : Eq.{u_2 + 1} (α := β) (⨆ (x : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : (↑S : Type u_1)), (↑i : Set α)) x), f x)
  (⨆ s ∈ S, ⨆ x ∈ s, f x)
Tactic: rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
S : Set (Set α)
f : α → β
rw :
  Eq.{u_2 + 1} (α := β) (⨆ (x : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : (↑S : Type u_1)), (↑i : Set α)) x), f x)
    (⨆ s ∈ S, ⨆ x ∈ s, f x)
⊢ Eq.{u_2 + 1} (α := β) (⨆ x ∈ ⋃₀ S, f x) (⨆ s ∈ S, ⨆ x ∈ s, f x)
have rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (i : (↑S : Type u_1)), ⨆ a ∈ (↑i : Set α), f a) (⨆ s ∈ S, ⨆ x ∈ s, f x)
Tactic: rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
S : Set (Set α)
f : α → β
rw :
  Eq.{u_2 + 1} (α := β) (⨆ (x : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : (↑S : Type u_1)), (↑i : Set α)) x), f x)
    (⨆ s ∈ S, ⨆ x ∈ s, f x)
rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (i : (↑S : Type u_1)), ⨆ a ∈ (↑i : Set α), f a) (⨆ s ∈ S, ⨆ x ∈ s, f x)
⊢ Eq.{u_2 + 1} (α := β) (⨆ x ∈ ⋃₀ S, f x) (⨆ s ∈ S, ⨆ x ∈ s, f x)
have rw₂ : Eq.{u_2 + 1} (α := β) (⨆ (i : (↑S : Type u_1)), ⨆ a ∈ (↑i : Set α), f a)
  (⨆ (i : (↑S : Type u_1)), ⨆ x ∈ (↑i : Set α), f x)
Tactic: rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ Eq.{u_2 + 1} (α := β) (⨅ x ∈ ⋃₀ S, f x) (⨅ s ∈ S, ⨅ x ∈ s, f x)
have rw : Eq.{u_2 + 1} (α := β) (⨅ (x : α), ⨅ (_ : Membership.mem (γ := Set α) (⋃ (i : (↑S : Type u_1)), (↑i : Set α)) x), f x)
  (⨅ s ∈ S, ⨅ x ∈ s, f x)
Tactic: rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
S : Set (Set α)
f : α → β
rw :
  Eq.{u_2 + 1} (α := β) (⨅ (x : α), ⨅ (_ : Membership.mem (γ := Set α) (⋃ (i : (↑S : Type u_1)), (↑i : Set α)) x), f x)
    (⨅ s ∈ S, ⨅ x ∈ s, f x)
⊢ Eq.{u_2 + 1} (α := β) (⨅ x ∈ ⋃₀ S, f x) (⨅ s ∈ S, ⨅ x ∈ s, f x)
have rw₁ : Eq.{u_2 + 1} (α := β) (⨅ (i : (↑S : Type u_1)), ⨅ a ∈ (↑i : Set α), f a) (⨅ s ∈ S, ⨅ x ∈ s, f x)
Tactic: rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
S : Set (Set α)
f : α → β
rw :
  Eq.{u_2 + 1} (α := β) (⨅ (x : α), ⨅ (_ : Membership.mem (γ := Set α) (⋃ (i : (↑S : Type u_1)), (↑i : Set α)) x), f x)
    (⨅ s ∈ S, ⨅ x ∈ s, f x)
rw₁ : Eq.{u_2 + 1} (α := β) (⨅ (i : (↑S : Type u_1)), ⨅ a ∈ (↑i : Set α), f a) (⨅ s ∈ S, ⨅ x ∈ s, f x)
⊢ Eq.{u_2 + 1} (α := β) (⨅ x ∈ ⋃₀ S, f x) (⨅ s ∈ S, ⨅ x ∈ s, f x)
have rw₂ : Eq.{u_2 + 1} (α := β) (⨅ (i : (↑S : Type u_1)), ⨅ a ∈ (↑i : Set α), f a)
  (⨅ (i : (↑S : Type u_1)), ⨅ x ∈ (↑i : Set α), f x)
Tactic: rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x
have simp_rw : ⨅ i ∈ ⋃₀ S, p i ↔ ⨅ i ∈ S, ⨅ i_2 ∈ i, p i_2
Tactic: simp_rw [← iInf_Prop_eq, iInf_sUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x
have simp_rw : (∃ (x : α) (_ : x ∈ ⋃₀ S), p x) ↔ ∃ (s : Set α) (_ : s ∈ S) (x : α) (_ : x ∈ s), p x
Tactic: simp_rw [← exists_prop, ← iSup_Prop_eq, iSup_sUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
S : Set (Set α)
p : α → Prop
simp_rw : (∃ (x : α) (_ : x ∈ ⋃₀ S), p x) ↔ ∃ (s : Set α) (_ : s ∈ S) (x : α) (_ : x ∈ s), p x
⊢ (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x
have simp_rw₁ : ⨆ x ∈ ⋃₀ S, p x ↔ ⨆ s ∈ S, ⨆ x ∈ s, p x
Tactic: simp_rw [← exists_prop, ← iSup_Prop_eq, iSup_sUnion]
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ range (map f) = {l : List β | ∀ (x : β), x ∈ l → x ∈ range f}
have refine : ∀ (l : List β) (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} l),
  l ∈ range (map f)
Tactic: refine antisymm (range_subset_iff.2 fun l => forall_mem_map.2 fun y _ => mem_range_self _)
      fun l hl => ?_
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List β
ihl : ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} l), l ∈ range (map f)
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (a :: l)
⊢ a :: l ∈ range (map f)
have cons : ∀ (l : List α)
  (ihl :
    ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (map f l)),
      map f l ∈ range (map f))
  (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (a :: map f l)),
  a :: map f l ∈ range (map f)
Tactic: rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩
Cleared hypotheses: l, ihl, hl
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List α
ihl :
  ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (map f l)),
    map f l ∈ range (map f)
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (a :: map f l)
⊢ a :: map f l ∈ range (map f)
have cons : ∀ (a : α) (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (f a :: map f l)),
  f a :: map f l ∈ range (map f)
Tactic: rcases hl a mem_cons_self with ⟨a, rfl⟩
Cleared hypotheses: a, hl
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : List β
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} l
⊢ l ∈ range (map f)
have nil : ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} []), [] ∈ range (map f)
Tactic: induction l with
  | nil => exact ⟨[], rfl⟩
  | cons a l ihl =>
    rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩
    rcases hl a mem_cons_self with ⟨a, rfl⟩
    exact ⟨a :: l, map_cons⟩
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : List β
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} l
nil : ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} []), [] ∈ range (map f)
⊢ l ∈ range (map f)
have cons : ∀ (a : β) (l : List β)
  (ihl : ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} l), l ∈ range (map f))
  (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (a :: l)),
  a :: l ∈ range (map f)
Tactic: induction l with
  | nil => exact ⟨[], rfl⟩
  | cons a l ihl =>
    rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩
    rcases hl a mem_cons_self with ⟨a, rfl⟩
    exact ⟨a :: l, map_cons⟩
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
s : Set α
⊢ Eq.{u_1 + 1} (α := Set (List α)) (range (ι := List { x : α // x ∈ s }) (map (Subtype.val (p := fun (x : α) ↦ x ∈ s))))
    {l : List α | ∀ (x : α), x ∈ l → x ∈ s}
have rw : Eq.{u_1 + 1} (α := Set (List α))
  {l : List α |
    ∀ (x : α),
      x ∈ l → Membership.mem (γ := Set α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) x}
  {l : List α | ∀ (x : α), x ∈ l → x ∈ s}
Tactic: rw [range_list_map, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
s : Set α
rw :
  Eq.{u_1 + 1} (α := Set (List α))
    {l : List α |
      ∀ (x : α),
        x ∈ l →
          Membership.mem (γ := Set α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) x}
    {l : List α | ∀ (x : α), x ∈ l → x ∈ s}
⊢ Eq.{u_1 + 1} (α := Set (List α)) (range (ι := List { x : α // x ∈ s }) (map (Subtype.val (p := fun (x : α) ↦ x ∈ s))))
    {l : List α | ∀ (x : α), x ∈ l → x ∈ s}
have rw₁ : Eq.{u_1 + 1} (α := Set (List α)) {l : List α | ∀ (x : α), x ∈ l → x ∈ s} {l : List α | ∀ (x : α), x ∈ l → x ∈ s}
Tactic: rw [range_list_map, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
l : List α
⊢ range l.get = {x : α | x ∈ l}
have h : ∀ (x : α), x ∈ range l.get ↔ Membership.mem (γ := Set α) {x : α | x ∈ l} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ Membership.mem (γ := Set α) {x : α | x ∈ l} x
have h : x ∈ range l.get ↔ x ∈ l
Tactic: rw [mem_setOf_eq, mem_iff_get, mem_range]
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
l : List α
x : α
h : x ∈ range l.get ↔ x ∈ l
⊢ x ∈ range l.get ↔ Membership.mem (γ := Set α) {x : α | x ∈ l} x
have h₁ : x ∈ range l.get ↔ ∃ (n : Fin l.length), l.get n = x
Tactic: rw [mem_setOf_eq, mem_iff_get, mem_range]
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
l : List α
x : α
h : x ∈ range l.get ↔ x ∈ l
h₁ : x ∈ range l.get ↔ ∃ (n : Fin l.length), l.get n = x
⊢ x ∈ range l.get ↔ Membership.mem (γ := Set α) {x : α | x ∈ l} x
have h₂ : (∃ (y : Fin l.length), l.get y = x) ↔ ∃ (n : Fin l.length), l.get n = x
Tactic: rw [mem_setOf_eq, mem_iff_get, mem_range]
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
l : List α
⊢ Eq (α := Set (Option α)) (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x)
    (insert none (some '' {x : α | x ∈ l}))
have rw : (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) =
  insert none (range (some ∘ l.get))
Tactic: rw [← range_list_get, ← range_comp]
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
l : List α
⊢ (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) =
    insert none (range (some ∘ l.get))
have refine_1 : ∀ (n : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ∈ insert none (range (some ∘ l.get))
Tactic: refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
l : List α
refine_1 :
  ∀ (n : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ∈ insert none (range (some ∘ l.get))
⊢ (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) =
    insert none (range (some ∘ l.get))
have refine_2 : Membership.mem (γ := Set (Option α))
  (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) none
Tactic: refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
l : List α
refine_1 :
  ∀ (n : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ∈ insert none (range (some ∘ l.get))
refine_2 :
  Membership.mem (γ := Set (Option α))
    (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) none
⊢ (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) =
    insert none (range (some ∘ l.get))
have refine_3 : range (some ∘ l.get) ⊆ range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x
Tactic: refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
l : List α
d : α
⊢ Eq.{u_1 + 1} (α := Set α)
    (range fun (n : ℕ) ↦ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD d)
    ((fun (o : Option α) ↦ o.getD d) ''
      range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x)
have simp : Eq.{u_1 + 1} (α := Set α)
  (range fun (n : ℕ) ↦ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD d)
  (range fun (x : ℕ) ↦ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x).getD d)
Tactic: simp only [← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.Set.List (goal)
Goal:
α : Type u_1
β : Type u_2
l_1 : List α
c : β → α
p : α → Prop
inst : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ ∃ (y : List β), map c y = l
have rw : Membership.mem (γ := Set (List α)) {l : List α | ∀ (x : α), x ∈ l → x ∈ Set.range c} l
Tactic: rw [← Set.mem_range, Set.range_list_map]
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
u v : Set α
hu : u ∈ memPartition f n
hv : v ∈ memPartition f n
huv : u ≠ v
⊢ Disjoint u v
have revert : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
Tactic: revert u v
Cleared hypotheses: u, v, hu, hv, huv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (hypothesis)
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
hv : v ∈ memPartition f 0
huv : u ≠ v
⊢ Disjoint u v
have hu₁ : u = univ
Tactic: simp only [memPartition_zero, mem_singleton_iff] at hu hv
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (hypothesis)
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
hv : v ∈ memPartition f 0
huv : u ≠ v
hu₁ : u = univ
⊢ Disjoint u v
have hv₁ : v = univ
Tactic: simp only [memPartition_zero, mem_singleton_iff] at hu hv
Cleared hypotheses: hu, hv