awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
⊢ update (β := α) f i x j ∈ t j
have h : ∀ (hi : j ∈ s) (hf : ∀ (j_1 : ι), j_1 ∈ s → j_1 ≠ j → f j_1 ∈ t j_1) (x : α j) (hx : x ∈ t j),
  update (β := α) f j x j ∈ t j
Tactic: obtain rfl | h := eq_or_ne j i
Cleared hypotheses: i, hi, hf, x, hx
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h :
  ∀ (hi : j ∈ s) (hf : ∀ (j_1 : ι), j_1 ∈ s → j_1 ≠ j → f j_1 ∈ t j_1) (x : α j) (hx : x ∈ t j),
    update (β := α) f j x j ∈ t j
⊢ update (β := α) f i x j ∈ t j
have h₁ : ∀ (h : j ≠ i), update (β := α) f i x j ∈ t j
Tactic: obtain rfl | h := eq_or_ne j i
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ update (β := α) f i x j ∈ t j
have h₁ : f j ∈ t j
Tactic: rw [update_of_ne h]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
β : ι → Type u_3
inst : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
⊢ update (β := β) x i '' s = pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s)
have h : ∀ (y : (a : ι) → β a),
  y ∈ update (β := β) x i '' s ↔
    Membership.mem (γ := Set ((a : ι) → β a))
      (pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s)) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
β : ι → Type u_3
inst : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ y ∈ update (β := β) x i '' s ↔
    Membership.mem (γ := Set ((a : ι) → β a))
      (pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s)) y
have h : (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔
  ∀ (i_1 : ι),
    Membership.mem (γ := Set (β i_1))
      (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s i_1 : Set (β i_1)) (y i_1)
Tactic: simp only [mem_image, update_eq_iff, ne_eq, and_left_comm (a := _ ∈ s), exists_eq_left, mem_pi,
    mem_univ, true_implies]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
β : ι → Type u_3
inst : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔
    ∀ (i_1 : ι),
      Membership.mem (γ := Set (β i_1))
        (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s i_1 : Set (β i_1)) (y i_1)
have h : (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔
  y i ∈ s ∧ ∀ (x_1 : ι), x_1 ≠ i → Membership.mem (γ := Set (β x_1)) {x x_1} (y x_1)
Tactic: rw [forall_update_iff (p := fun x s => y x ∈ s)]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ preimage (β := (a : ι') → α ((f : (a : ι') → ι) a))
      (⇑(piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a))
      (s.pi (α := fun (a : ι') ↦ α ((f : (a : ι') → ι) a)) fun (i' : ι') ↦ t ((f : (a : ι') → ι) i')) =
    pi (α := α) ((⇑f : (a : ι') → ι) '' s) t
have h : ∀ (x : (b : ι) → α b),
  Membership.mem (γ := Set ((b : ι) → α b))
      (preimage (β := (a : ι') → α ((f : (a : ι') → ι) a))
        (⇑(piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a))
        (s.pi (α := fun (a : ι') ↦ α ((f : (a : ι') → ι) a)) fun (i' : ι') ↦ t ((f : (a : ι') → ι) i')))
      x ↔
    x ∈ pi (α := α) ((⇑f : (a : ι') → ι) '' s) t
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ Eq (α := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
    ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
      pi (α := α) ((⇑f : (a : ι') → ι) '' s) t)
    (s.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) fun (i : ι') ↦ t ((f : (a : ι') → ι) i))
have h : ∀ (x : (a : ι') → α ((f : (a : ι') → ι) a)),
  Membership.mem (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
      ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
        pi (α := α) ((⇑f : (a : ι') → ι) '' s) t)
      x ↔
    Membership.mem (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
      (s.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) fun (i : ι') ↦ t ((f : (a : ι') → ι) i)) x
Tactic: apply Set.ext
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ∀ (x : (a : ι') → α ((f : (a : ι') → ι) a)),
    Membership.mem (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
          pi (α := α) ((⇑f : (a : ι') → ι) '' s) t)
        x ↔
      Membership.mem (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
        (s.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) fun (i : ι') ↦ t ((f : (a : ι') → ι) i)) x
have h : ∀ (a : (b : ι) → α b),
  Membership.mem (α := (a : ι') → α ((f : (a : ι') → ι) a)) (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
      ((⇑(piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
        pi (α := α) ((⇑f : (a : ι') → ι) '' s) t)
      (((piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a)) a :
        (a : ι') → α ((f : (a : ι') → ι) a)) ↔
    Membership.mem (α := (a : ι') → α ((f : (a : ι') → ι) a)) (γ := Set ((a : ι') → α ((f : (a : ι') → ι) a)))
      (s.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) fun (i : ι') ↦ t ((f : (a : ι') → ι) i))
      (((piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a)) a :
        (a : ι') → α ((f : (a : ι') → ι) a))
Tactic: rw [← (f.piCongrLeft α).symm.forall_congr_right]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
⊢ (⇑(sumPiEquivProdPi π).symm : (a : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))) → (i : ι ⊕ ι') → π i) ⁻¹'
      pi (α := π) univ t =
    SProd.sprod (α := Set ((i : ι) → π (Sum.inl i))) (β := Set ((i : ι') → π (Sum.inr i)))
      (pi (α := fun (i : ι) ↦ π (Sum.inl i)) univ fun (i : ι) ↦ t (Sum.inl i))
      (pi (α := fun (i : ι') ↦ π (Sum.inr i)) univ fun (i : ι') ↦ t (Sum.inr i))
have h : ∀ (x : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))),
  Membership.mem (γ := Set (((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))))
      ((⇑(sumPiEquivProdPi π).symm :
          (a : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))) → (i : ι ⊕ ι') → π i) ⁻¹'
        pi (α := π) univ t)
      x ↔
    x ∈
      SProd.sprod (α := Set ((i : ι) → π (Sum.inl i))) (β := Set ((i : ι') → π (Sum.inr i)))
        (pi (α := fun (i : ι) ↦ π (Sum.inl i)) univ fun (i : ι) ↦ t (Sum.inl i))
        (pi (α := fun (i : ι') ↦ π (Sum.inr i)) univ fun (i : ι') ↦ t (Sum.inr i))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Prod.snd '' graphOn f s = f '' s
have h : ∀ (x : β), x ∈ Prod.snd '' graphOn f s ↔ x ∈ f '' s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ (f' : β → γ), range f = graphOn f' univ
have refine : range f = graphOn (fun (h : β) ↦ (f (sorry.choose (p := fun (a : α) ↦ (Prod.fst ∘ f) a = h))).2) univ
Tactic: refine ⟨fun h ↦ (f (hf₁ h).choose).snd, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ range f = graphOn (fun (h : β) ↦ (f (⋯.choose (p := fun (a : α) ↦ (Prod.fst ∘ f) a = h))).2) univ
have h : ∀ (x : β × γ),
  x ∈ range f ↔
    Membership.mem (γ := Set (β × γ))
      (graphOn (fun (h : β) ↦ (f (sorry.choose (p := fun (a : α) ↦ (Prod.fst ∘ f) a = h))).2) univ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ x ∈ range f ↔
    Membership.mem (γ := Set (β × γ))
      (graphOn (fun (h : β) ↦ (f (⋯.choose (p := fun (a : α) ↦ (Prod.fst ∘ f) a = h))).2) univ) x
have h : (∃ (y : α), f y = x) ↔ (f (Exists.choose (p := fun (a : α) ↦ (f a).1 = x.1) sorry)).2 = x.2
Tactic: simp only [mem_range, comp_apply, mem_graphOn, mem_univ, true_and]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ (∃ (y : α), f y = x) ↔ (f (Exists.choose (p := fun (a : α) ↦ (f a).1 = x.1) ⋯)).2 = x.2
have h : (∃ (y : α), f y = x) → (f (Exists.choose (p := fun (a : α) ↦ (f a).1 = x.1) sorry)).2 = x.2
Tactic: refine ⟨?_, fun hi ↦ ⟨(hf₁ x.1).choose, Prod.ext (hf₁ x.1).choose_spec hi⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
⊢ ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ
have obtain : ∀ (e₁ : β → γ) (he₁ : range f = graphOn e₁ univ), ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ
Tactic: obtain ⟨e₁, he₁⟩ := exists_range_eq_graphOn_univ hf₁ fun _ _ ↦ (hf _ _).1
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
⊢ ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ
have obtain : ∀ (e₂ : γ → β) (he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ),
  ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ
Tactic: obtain ⟨e₂, he₂⟩ := exists_range_eq_graphOn_univ (f := Equiv.prodComm _ _ ∘ f) (by simpa) <|
    by simp [hf]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h
have rw : ∀ (he₁ : ∀ (x : β × γ), x ∈ range f ↔ x ∈ graphOn e₁ univ) (e₂ : γ → β)
  (he₂ :
    ∀ (x : γ × β),
      Membership.mem (γ := Set (γ × β)) (range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f)) x ↔
        x ∈ graphOn e₂ univ)
  (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
Tactic: rw [Set.ext_iff] at he₁ he₂
Cleared hypotheses: he₁, e₂, he₂, h, i
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ
⊢ ∃ (e : β ≃ γ), range f = graphOn (⇑e : (a : β) → γ) univ
have he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
Tactic: have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    rw [Set.ext_iff] at he₁ he₂
    aesop (add simp [Prod.swap_eq_iff_eq_swap])
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
h : β
⊢ e₂ (e₁ h) = h
have rw : e₁ h = e₁ h
Tactic: rw [← he₁₂]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range ((⇑(Equiv.prodComm β γ) : (a : β × γ) → γ × β) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
i : γ
⊢ e₁ (e₂ i) = i
have rw : e₂ i = e₂ i
Tactic: rw [he₁₂]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ s.restrict (π := fun (a : α) ↦ β) f '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t = f '' (t ∩ s)
have rw : image (α := (↑s : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
  f '' (t ∩ s)
Tactic: rw [restrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
rw :
  image (α := (↑s : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
    f '' (t ∩ s)
⊢ s.restrict (π := fun (a : α) ↦ β) f '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t = f '' (t ∩ s)
have rw₁ : f ''
    image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
  f '' (t ∩ s)
Tactic: rw [restrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
rw :
  image (α := (↑s : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
    f '' (t ∩ s)
rw₁ :
  f ''
      image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
    f '' (t ∩ s)
⊢ s.restrict (π := fun (a : α) ↦ β) f '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t = f '' (t ∩ s)
have rw₂ : f '' (t ∩ range (ι := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) = f '' (t ∩ s)
Tactic: rw [restrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
rw :
  image (α := (↑s : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
    f '' (t ∩ s)
rw₁ :
  f ''
      image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
    f '' (t ∩ s)
rw₂ : f '' (t ∩ range (ι := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) = f '' (t ∩ s)
⊢ s.restrict (π := fun (a : α) ↦ β) f '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t = f '' (t ∩ s)
have rw₃ : f '' (t ∩ s) = f '' (t ∩ s)
Tactic: rw [restrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ (if h : ∃ (a : α), f a = y then g (Classical.choose (p := fun (x : α) ↦ f x = y) h) else g' y) ∈
    range g ∪ g' '' (range f)ᶜ
have pos : ∀ (h : ∃ (a : α), f a = y), g (Classical.choose (p := fun (x : α) ↦ f x = y) h) ∈ range g ∪ g' '' (range f)ᶜ
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
pos : ∀ (h : ∃ (a : α), f a = y), g (Classical.choose (p := fun (x : α) ↦ f x = y) h) ∈ range g ∪ g' '' (range f)ᶜ
⊢ (if h : ∃ (a : α), f a = y then g (Classical.choose (p := fun (x : α) ↦ f x = y) h) else g' y) ∈
    range g ∪ g' '' (range f)ᶜ
have neg : ∀ (h : ¬∃ (a : α), f a = y), g' y ∈ range g ∪ g' '' (range f)ᶜ
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ
have rintro : ∀ (y : β), extend f g g' y ∈ range g ∪ g' '' (range f)ᶜ
Tactic: classical
  rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
rintro : ∀ (y : β), extend f g g' y ∈ range g ∪ g' '' (range f)ᶜ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ
have rintro₁ : ∀ (y : β),
  (if h : ∃ (a : α), f a = y then g (Classical.choose (p := fun (x : α) ↦ f x = y) h) else g' y) ∈
    range g ∪ g' '' (range f)ᶜ
Tactic: classical
  rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
rintro : ∀ (y : β), extend f g g' y ∈ range g ∪ g' '' (range f)ᶜ
rintro₁ :
  ∀ (y : β),
    (if h : ∃ (a : α), f a = y then g (Classical.choose (p := fun (x : α) ↦ f x = y) h) else g' y) ∈
      range g ∪ g' '' (range f)ᶜ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ
have pos : ∀ (y : β) (h : ∃ (a : α), f a = y), g (Classical.choose (p := fun (x : α) ↦ f x = y) h) ∈ range g ∪ g' '' (range f)ᶜ
Tactic: classical
  rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
rintro : ∀ (y : β), extend f g g' y ∈ range g ∪ g' '' (range f)ᶜ
rintro₁ :
  ∀ (y : β),
    (if h : ∃ (a : α), f a = y then g (Classical.choose (p := fun (x : α) ↦ f x = y) h) else g' y) ∈
      range g ∪ g' '' (range f)ᶜ
pos :
  ∀ (y : β) (h : ∃ (a : α), f a = y), g (Classical.choose (p := fun (x : α) ↦ f x = y) h) ∈ range g ∪ g' '' (range f)ᶜ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ
have neg : ∀ (y : β) (h : ¬∃ (a : α), f a = y), g' y ∈ range g ∪ g' '' (range f)ᶜ
Tactic: classical
  rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range (extend f g g') = range g ∪ g' '' (range f)ᶜ
have refine : range g ∪ g' '' (range f)ᶜ ⊆ range (extend f g g')
Tactic: refine (range_extend_subset _ _ _).antisymm ?_
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ range (codRestrict f s h) = Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' range f
have h₁ : ∀ (x : (↑s : Type u_1)),
  x ∈ range (codRestrict f s h) ↔
    Membership.mem (γ := Set (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' range f) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : (↑s : Type u_1)
k : ℕ
⊢ (↑((restrict f s s h)^[k] x) : α) = f^[k] (↑x : α)
have zero : (↑((restrict f s s h)^[0] x) : α) = f^[0] (↑x : α)
Tactic: induction k with
  | zero => simp
  | succ k ih => simp only [iterate_succ', comp_apply, val_restrict_apply, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : (↑s : Type u_1)
k : ℕ
zero : (↑((restrict f s s h)^[0] x) : α) = f^[0] (↑x : α)
⊢ (↑((restrict f s s h)^[k] x) : α) = f^[k] (↑x : α)
have succ : ∀ (k : ℕ) (ih : (↑((restrict f s s h)^[k] x) : α) = f^[k] (↑x : α)),
  (↑((restrict f s s h)^[k + 1] x) : α) = f^[k + 1] (↑x : α)
Tactic: induction k with
  | zero => simp
  | succ k ih => simp only [iterate_succ', comp_apply, val_restrict_apply, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : ∃ (g : (↑s : Type u_1) → (↑t : Type u_2)), ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
x : α
hx : x ∈ s
g : (↑s : Type u_1) → (↑t : Type u_2)
hg : ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
⊢ f x ∈ t
have rw : (↑(g (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) : β) ∈ t
Tactic: rw [hg ⟨x, hx⟩]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s =
    Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
have rw : Eq (α := Set β)
  ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ''
    MapsTo.restrict f (f ⁻¹' t) t sorry '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
  ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
Tactic: rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
rw :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ''
      MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s =
    Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
have rw₁ : Eq (α := Set β)
  ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ∘ MapsTo.restrict f (f ⁻¹' t) t sorry ''
    Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
  ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
Tactic: rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Restrict (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
rw :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ''
      MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₁ :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ∘ MapsTo.restrict f (f ⁻¹' t) t ⋯ ''
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s =
    Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
have rw₂ : image (α := (↑(f ⁻¹' t) : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
    (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
  (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
Tactic: rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]