awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
rw :
  Eq (α := Set ((i : ι) → β i)) (s.pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
    (({i} ∪ s).pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
⊢ Eq (α := Set ((i : ι) → β i)) (s.pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
    (({i} ∪ s \ {i}).pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
have rw₁ : Eq (α := Set ((i : ι) → β i)) (s.pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
  (s.pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
Tactic: rw [union_diff_self, union_eq_self_of_subset_left (singleton_subset_iff.2 hi)]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ Eq (α := Set ((i : ι) → β i)) (({i} ∪ s \ {i}).pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
    ({x : (i : ι) → β i | x i ∈ t i a} ∩ (s \ {i}).pi (α := β) fun (j : ι) ↦ t j (f j))
have hi₁ : ¬i ∈ s \ {i}
Tactic: rw [union_pi, singleton_pi', update_self, pi_update_of_notMem]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
β : ι → Type u_4
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ Eq (α := Set ((i : ι) → β i)) (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
    ({x : (i : ι) → β i | x i ∈ t i a} ∩ pi (α := β) {i}ᶜ fun (j : ι) ↦ t j (f j))
have rw : Eq (α := Set ((i : ι) → β i)) (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
  ({x : (i : ι) → β i | x i ∈ t i a} ∩ pi (α := β) (univ \ {i}) fun (j : ι) ↦ t j (f j))
Tactic: rw [compl_eq_univ_diff, ← pi_update_of_mem (mem_univ _)]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
β : ι → Type u_4
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
rw :
  Eq (α := Set ((i : ι) → β i)) (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
    ({x : (i : ι) → β i | x i ∈ t i a} ∩ pi (α := β) (univ \ {i}) fun (j : ι) ↦ t j (f j))
⊢ Eq (α := Set ((i : ι) → β i)) (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
    ({x : (i : ι) → β i | x i ∈ t i a} ∩ pi (α := β) {i}ᶜ fun (j : ι) ↦ t j (f j))
have rw₁ : Eq (α := Set ((i : ι) → β i)) (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
  (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
Tactic: rw [compl_eq_univ_diff, ← pi_update_of_mem (mem_univ _)]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
i : ι
s : Set (α i)
⊢ pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s) = eval (β := α) i ⁻¹' s
have rw : ({x : (i : ι) → α i | x i ∈ s} ∩ pi (α := α) {i}ᶜ fun (j : ι) ↦ univ) = eval (β := α) i ⁻¹' s
Tactic: rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
i : ι
s : Set (α i)
rw : ({x : (i : ι) → α i | x i ∈ s} ∩ pi (α := α) {i}ᶜ fun (j : ι) ↦ univ) = eval (β := α) i ⁻¹' s
⊢ pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s) = eval (β := α) i ⁻¹' s
have rw₁ : {x : (i : ι) → α i | x i ∈ s} ∩ univ = eval (β := α) i ⁻¹' s
Tactic: rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
i : ι
s : Set (α i)
rw : ({x : (i : ι) → α i | x i ∈ s} ∩ pi (α := α) {i}ᶜ fun (j : ι) ↦ univ) = eval (β := α) i ⁻¹' s
rw₁ : {x : (i : ι) → α i | x i ∈ s} ∩ univ = eval (β := α) i ⁻¹' s
⊢ pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s) = eval (β := α) i ⁻¹' s
have rw₂ : {x : (i : ι) → α i | x i ∈ s} = eval (β := α) i ⁻¹' s
Tactic: rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
i : ι
s : Set (α i)
rw : ({x : (i : ι) → α i | x i ∈ s} ∩ pi (α := α) {i}ᶜ fun (j : ι) ↦ univ) = eval (β := α) i ⁻¹' s
rw₁ : {x : (i : ι) → α i | x i ∈ s} ∩ univ = eval (β := α) i ⁻¹' s
rw₂ : {x : (i : ι) → α i | x i ∈ s} = eval (β := α) i ⁻¹' s
⊢ pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s) = eval (β := α) i ⁻¹' s
have rw₃ : Eq (α := Set ((i : ι) → α i)) {x : (i : ι) → α i | x i ∈ s} {x : (x : ι) → α x | eval (β := α) i x ∈ s}
Tactic: rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
ht : (s.pi (α := α) t).Nonempty
i : ι
⊢ t i ⊆ eval (β := α) i '' s.pi (α := α) t
have obtain : ∀ (f : (i : ι) → α i) (hf : f ∈ s.pi (α := α) t), t i ⊆ eval (β := α) i '' s.pi (α := α) t
Tactic: obtain ⟨f, hf⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi (α := α) t
⊢ t i ⊆ eval (β := α) i '' s.pi (α := α) t
have refine : ∀ (y : α i) (hy : y ∈ t i) (j : ι) (hj : j ∈ s), update (β := α) f i y j ∈ t j
Tactic: refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi (α := α) t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
⊢ update (β := α) f i y j ∈ t j
have inl : ∀ (y : α j) (hy : y ∈ t j), update (β := α) f j y j ∈ t j
Tactic: obtain rfl | hji := eq_or_ne j i
Cleared hypotheses: i, y, hy
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi (α := α) t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
inl : ∀ (y : α j) (hy : y ∈ t j), update (β := α) f j y j ∈ t j
⊢ update (β := α) f i y j ∈ t j
have inr : ∀ (hji : j ≠ i), update (β := α) f i y j ∈ t j
Tactic: obtain rfl | hji := 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)
ht : (s.pi (α := α) t).Nonempty
i : ι
⊢ t i ⊆ eval (β := α) i '' s.pi (α := α) t
have obtain : ∀ (f : (i : ι) → α i) (hf : f ∈ s.pi (α := α) t), t i ⊆ eval (β := α) i '' s.pi (α := α) t
Tactic: classical
  obtain ⟨f, hf⟩ := ht
  refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
  obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
ht : (s.pi (α := α) t).Nonempty
i : ι
obtain : ∀ (f : (i : ι) → α i) (hf : f ∈ s.pi (α := α) t), t i ⊆ eval (β := α) i '' s.pi (α := α) t
⊢ t i ⊆ eval (β := α) i '' s.pi (α := α) t
have obtain₁ : ∀ (f : (i : ι) → α i) (hf : f ∈ s.pi (α := α) t) (y : α i) (hy : y ∈ t i) (j : ι) (hj : j ∈ s),
  update (β := α) f i y j ∈ t j
Tactic: classical
  obtain ⟨f, hf⟩ := ht
  refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
  obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]
Cleared hypotheses: ht
-- 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 : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
⊢ eval (β := α) i '' s.pi (α := α) t = if (s.pi (α := α) t).Nonempty then univ else ∅
have h : ∀ (xᵢ : α i),
  xᵢ ∈ eval (β := α) i '' s.pi (α := α) t ↔
    Membership.mem (γ := Set (α i)) (if (s.pi (α := α) t).Nonempty then univ else ∅) xᵢ
Tactic: ext xᵢ
-- 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 : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ xᵢ ∈ eval (β := α) i '' s.pi (α := α) t ↔
    Membership.mem (γ := Set (α i)) (if (s.pi (α := α) t).Nonempty then univ else ∅) xᵢ
have h : (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔ ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
Tactic: simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
-- 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 : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔
    ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
have h : (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) → ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
Tactic: constructor
-- 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 : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
h :
  (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) →
    ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔
    ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
have h₁ : (∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i) → ∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ
Tactic: constructor
-- 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 : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
x : (i : ι) → α i
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ ∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ
have h : (∀ (i_1 : ι), i_1 ∈ s → update (β := α) x i xᵢ i_1 ∈ t i_1) ∧ update (β := α) x i xᵢ i = xᵢ
Tactic: refine ⟨Function.update x i xᵢ, ?_⟩
-- 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 : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
⊢ eval (β := α) i '' s.pi (α := α) t = if (s.pi (α := α) t).Nonempty then univ else ∅
have h : ∀ (xᵢ : α i),
  xᵢ ∈ eval (β := α) i '' s.pi (α := α) t ↔
    Membership.mem (γ := Set (α i)) (if (s.pi (α := α) t).Nonempty then univ else ∅) xᵢ
Tactic: classical
  ext xᵢ
  simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩
  · rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa +contextual [(ne_of_mem_of_not_mem · hi)]
-- 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 : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
h :
  ∀ (xᵢ : α i),
    xᵢ ∈ eval (β := α) i '' s.pi (α := α) t ↔
      Membership.mem (γ := Set (α i)) (if (s.pi (α := α) t).Nonempty then univ else ∅) xᵢ
⊢ eval (β := α) i '' s.pi (α := α) t = if (s.pi (α := α) t).Nonempty then univ else ∅
have h₁ : ∀ (xᵢ : α i),
  (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔
    ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
Tactic: classical
  ext xᵢ
  simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩
  · rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa +contextual [(ne_of_mem_of_not_mem · hi)]
-- 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 : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
h :
  ∀ (xᵢ : α i),
    xᵢ ∈ eval (β := α) i '' s.pi (α := α) t ↔
      Membership.mem (γ := Set (α i)) (if (s.pi (α := α) t).Nonempty then univ else ∅) xᵢ
h₁ :
  ∀ (xᵢ : α i),
    (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔
      ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ eval (β := α) i '' s.pi (α := α) t = if (s.pi (α := α) t).Nonempty then univ else ∅
have h₂ : ∀ (xᵢ : α i),
  (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) →
    ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
Tactic: classical
  ext xᵢ
  simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩
  · rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa +contextual [(ne_of_mem_of_not_mem · hi)]
-- 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 : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
h :
  ∀ (xᵢ : α i),
    xᵢ ∈ eval (β := α) i '' s.pi (α := α) t ↔
      Membership.mem (γ := Set (α i)) (if (s.pi (α := α) t).Nonempty then univ else ∅) xᵢ
h₁ :
  ∀ (xᵢ : α i),
    (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔
      ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
h₂ :
  ∀ (xᵢ : α i),
    (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) →
      ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ eval (β := α) i '' s.pi (α := α) t = if (s.pi (α := α) t).Nonempty then univ else ∅
have h₃ : ∀ (xᵢ : α i),
  (∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i) →
    ∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ
Tactic: classical
  ext xᵢ
  simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩
  · rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa +contextual [(ne_of_mem_of_not_mem · hi)]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
⊢ Pi.map (α := α) (β := β) f '' s.pi (α := α) t = s.pi (α := β) fun (i : ι) ↦ f i '' t i
have refine : ∀ (b : (i : ι) → β i) (hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b),
  b ∈ Pi.map (α := α) (β := β) f '' s.pi (α := α) t
Tactic: refine Subset.antisymm (piMap_image_pi_subset _) fun b hb => ?_
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
i : ι
⊢ ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
have if : ∀ (hi : i ∈ s), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
Tactic: if hi : i ∈ s then
      exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩
    else
      exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
i : ι
if : ∀ (hi : i ∈ s), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
⊢ ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
have if₁ : ∀ (hi : ¬i ∈ s), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
Tactic: if hi : i ∈ s then
      exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩
    else
      exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
⊢ b ∈ Pi.map (α := α) (β := β) f '' s.pi (α := α) t
have this : ∀ (i : ι), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
Tactic: have (i : ι) : ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i) := by
    if hi : i ∈ s then
      exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩
    else
      exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
this : ∀ (i : ι), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
⊢ b ∈ Pi.map (α := α) (β := β) f '' s.pi (α := α) t
have choose : ∀ (a : (i : ι) → α i) (hab : ∀ (i : ι), f i (a i) = b i) (hat : ∀ (i : ι), i ∈ s → a i ∈ t i),
  b ∈ Pi.map (α := α) (β := β) f '' s.pi (α := α) t
Tactic: choose a hab hat using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi (α := α) t
⊢ update (β := α) a i b ∈ s.pi (α := α) t ↔ i ∈ s → b ∈ t i
have rw : a ∈ (s \ {i}).pi (α := α) t
Tactic: rw [update_mem_pi_iff, and_iff_right]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ pi (α := α) univ t = {a} ↔ ∀ (i : ι), t i = {a i}
have simp : (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) ↔
  ∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i
Tactic: simp only [eq_singleton_iff_unique_mem]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) ↔
    ∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i
have refine : (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) →
  ∀ (i : ι) (h₁ : a ∈ pi (α := α) univ t) (h₂ : ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) (x : α i)
    (hx : x ∈ t i), x = a i
Tactic: refine ⟨fun ⟨h₁, h₂⟩ i => ⟨by grind, fun x hx => ?_⟩, by grind⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
h : a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a
i : ι
h₁ : a ∈ pi (α := α) univ t
h₂ : ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a
x : α i
hx : x ∈ t i
⊢ x = a i
have rw : x = update (β := α) a i x i
Tactic: rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
h : a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a
i : ι
h₁ : a ∈ pi (α := α) univ t
h₂ : ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a
x : α i
hx : x ∈ t i
rw : x = update (β := α) a i x i
⊢ x = a i
have rw₁ : x = x
Tactic: rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ pi (α := α) univ t = {a} ↔ ∀ (i : ι), t i = {a i}
have simp : (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) ↔
  ∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i
Tactic: classical
  simp only [eq_singleton_iff_unique_mem]
  refine ⟨fun ⟨h₁, h₂⟩ i => ⟨by grind, fun x hx => ?_⟩, by grind⟩
  rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
simp :
  (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) ↔
    ∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i
⊢ pi (α := α) univ t = {a} ↔ ∀ (i : ι), t i = {a i}
have simp₁ : (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) →
  ∀ (i : ι) (h₁ : a ∈ pi (α := α) univ t) (h₂ : ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) (x : α i)
    (hx : x ∈ t i), x = a i
Tactic: classical
  simp only [eq_singleton_iff_unique_mem]
  refine ⟨fun ⟨h₁, h₂⟩ i => ⟨by grind, fun x hx => ?_⟩, by grind⟩
  rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ s.pi (α := α) t₁ ⊆ s.pi (α := α) t₂ ↔ (∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i) ∨ s.pi (α := α) t₁ = ∅
have h : ∀ (h : s.pi (α := α) t₁ ⊆ s.pi (α := α) t₂), ¬s.pi (α := α) t₁ = ∅ → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
Tactic: refine
    ⟨fun h => or_iff_not_imp_right.2 ?_, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi (α := α) t₁ ⊆ s.pi (α := α) t₂
⊢ ¬s.pi (α := α) t₁ = ∅ → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
have rw : (s.pi (α := α) t₁).Nonempty → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
Tactic: rw [← Ne, ← nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
i : ι
inst : DecidableEq ι
s : Set (α i)
⊢ eval (β := α) i ⁻¹' s = pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)
have h : ∀ (x : (x : ι) → α x),
  x ∈ eval (β := α) i ⁻¹' s ↔
    Membership.mem (γ := Set ((x : ι) → α x))
      (pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
i : ι
inst : DecidableEq ι
s : Set (α i)
⊢ eval (β := α) i ⁻¹' s = pi (α := α) {i} (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)
have h : ∀ (x : (x : ι) → α x),
  x ∈ eval (β := α) i ⁻¹' s ↔
    Membership.mem (γ := Set ((x : ι) → α x))
      (pi (α := α) {i} (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)) x
Tactic: ext
-- 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
⊢ update (β := α) f i ⁻¹' s.pi (α := α) t = t i
have h : ∀ (x : α i), x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t ↔ x ∈ t i
Tactic: ext x
-- 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
⊢ x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t ↔ x ∈ t i
have h : ∀ (h : x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t), x ∈ t i
Tactic: refine ⟨fun h => ?_, fun hx j hj => ?_⟩
-- 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
h : ∀ (h : x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t), x ∈ t i
⊢ x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t ↔ x ∈ t i
have h₁ : ∀ (hx : x ∈ t i) (j : ι) (hj : j ∈ s), update (β := α) f i x j ∈ t j
Tactic: refine ⟨fun h => ?_, fun hx j hj => ?_⟩
-- 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
h : x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t
⊢ x ∈ t i
have h₁ : x = update (β := α) f i x i
Tactic: convert! h i hi