awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
rw : toPullbackDiag f '' univ = pullbackDiagonal f
rw₁ :
  pullbackDiagonal f ∩
      Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' SProd.sprod (α := Set X) (β := Set X) univ univ =
    pullbackDiagonal f
rw₂ : pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' univ = pullbackDiagonal f
rw₃ : pullbackDiagonal f ∩ univ = pullbackDiagonal f
⊢ range (toPullbackDiag f) = pullbackDiagonal f
have rw₄ : pullbackDiagonal f = pullbackDiagonal f
Tactic: rw [← image_univ, image_toPullbackDiag, univ_prod_univ, preimage_univ, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.offDiag = ∅ ↔ s.Subsingleton
have rw : ¬s.offDiag.Nonempty ↔ s.Subsingleton
Tactic: rw [← not_nonempty_iff_eq_empty, ← not_nontrivial_iff, offDiag_nonempty.not]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s : Set α
rw : ¬s.offDiag.Nonempty ↔ s.Subsingleton
⊢ s.offDiag = ∅ ↔ s.Subsingleton
have rw₁ : ¬s.offDiag.Nonempty ↔ ¬s.Nontrivial
Tactic: rw [← not_nonempty_iff_eq_empty, ← not_nontrivial_iff, offDiag_nonempty.not]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s : Set α
rw : ¬s.offDiag.Nonempty ↔ s.Subsingleton
rw₁ : ¬s.offDiag.Nonempty ↔ ¬s.Nontrivial
⊢ s.offDiag = ∅ ↔ s.Subsingleton
have rw₂ : ¬s.Nontrivial ↔ ¬s.Nontrivial
Tactic: rw [← not_nonempty_iff_eq_empty, ← not_nontrivial_iff, offDiag_nonempty.not]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mp : (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mpr : (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 → (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mp₁ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mp₆ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mp₆ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ t
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mp₇ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mp₆ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ t
mp₇ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ t
mp₈ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mpr₁ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mp₆ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ t
mp₇ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ t
mp₈ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mpr₁ mpr₂ :
  x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mpr₃ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mp₆ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ t
mp₇ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ t
mp₈ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mpr₁ mpr₂ :
  x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mpr₃ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ s
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mpr₄ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mp₆ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ t
mp₇ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ t
mp₈ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mpr₁ mpr₂ :
  x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mpr₃ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ s
mpr₄ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ t
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mpr₅ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.2 ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mp₆ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ t
mp₇ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ t
mp₈ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mpr₁ mpr₂ :
  x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mpr₃ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ s
mpr₄ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ t
mpr₅ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.2 ∈ s
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mpr₆ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.2 ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
x : α × α
mp :
  (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mpr :
  (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2 →
    (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mp₁ mp₂ :
  x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
mp₃ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ s
mp₄ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ s
mp₅ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mp₆ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ∈ t
mp₇ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.2 ∈ t
mp₈ : x.1 ∈ s → x.1 ∈ t → x.1 ≠ x.2 → x.2 ∈ s → x.2 ∈ t → x.1 ≠ x.2
mpr₁ mpr₂ :
  x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2
mpr₃ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ s
mpr₄ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ∈ t
mpr₅ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.2 ∈ s
mpr₆ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.2 ∈ t
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
have mpr₇ : x.1 ∈ s → x.1 ∈ t → x.2 ∈ s → x.1 ≠ x.2 → x.2 ∈ t → x.1 ≠ x.2 → x.1 ≠ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
have h₁ : ∀ (x : α × α), x ∈ (s ∪ t).offDiag ↔ x ∈ s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 ↔
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s
have h₁ : (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 →
  ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h₁ :
  (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 →
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 ↔
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s
have h₂ : ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s →
  (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2
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)
⊢ s.pi (α := α) t = ∅ ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
have rw : (¬∀ (i : ι), ∃ (x : α i), i ∈ s → x ∈ t i) ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
Tactic: rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (¬∀ (i : ι), ∃ (x : α i), i ∈ s → x ∈ t i) ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
have push : (∃ (i : ι), ∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
Tactic: push Not
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (∃ (i : ι), ∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
have refine : ∀ (i : ι), (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
Tactic: refine exists_congr fun 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 : ι
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
have inl : IsEmpty.{u_2 + 1} (α i) → ((∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅)
Tactic: cases isEmpty_or_nonempty (α 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 : ι
inl : IsEmpty.{u_2 + 1} (α i) → ((∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
have inr : Nonempty.{u_2 + 1} (α i) → ((∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅)
Tactic: cases isEmpty_or_nonempty (α i)
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Unique ι
t : (i : ι) → Set (α i)
⊢ Eq (α := Set (α default)) (uniqueElim (α := α) ⁻¹' pi (α := α) univ t) (t default)
have h : ∀ (x : α default),
  Membership.mem (γ := Set (α default)) (uniqueElim (α := α) ⁻¹' pi (α := α) univ t) x ↔
    Membership.mem (γ := Set (α default)) (t default) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) =
    pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
have h₁ : ∀ (f : (i : ι) → α i),
  Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f ↔
    f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
Tactic: ext f
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f ↔
    f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
have h₁ : ∀ (h : Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f),
  f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h₁ :
  ∀ (h : Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f),
    f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
⊢ Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f ↔
    f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
have h₂ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂ →
  Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h_1 : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f
⊢ f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
have h₁ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h_1 : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f
h₁ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁
⊢ f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
have h₂ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
⊢ Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)
have pos : p i → Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)
Tactic: by_cases p i
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
pos : p i → Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)
⊢ Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)
have neg : ¬p i → Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)
Tactic: by_cases p i
-- 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)
j : ι
hj : j ∈ s
⊢ t j (update (β := α) f i a j) = t j (f j)
have h : j ≠ i
Tactic: rw [update_of_ne]
-- 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)) (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))
  (({i} ∪ 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)]