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 s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
inr : ∀ (H : s ×ˢ t ⊆ s₁ ×ˢ t₁), s ⊆ s₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
have inr₁ : ∀ (H : s ×ˢ t ⊆ s₁ ×ˢ t₁), t ⊆ t₁
Tactic: refine ⟨fun H => Or.inl ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
inr : ∀ (H : s ×ˢ t ⊆ s₁ ×ˢ t₁), s ⊆ s₁
inr₁ : ∀ (H : s ×ˢ t ⊆ s₁ ×ˢ t₁), t ⊆ t₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
have inr₂ : s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ → s ×ˢ t ⊆ s₁ ×ˢ t₁
Tactic: refine ⟨fun H => Or.inl ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ s ⊆ s₁
have this : Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁
Tactic: have := image_mono (f := Prod.fst) H
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁
⊢ s ⊆ s₁
have inr : ∀ (this : s ⊆ Prod.fst '' s₁ ×ˢ t₁), s ⊆ s₁
Tactic: rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁
inr : ∀ (this : s ⊆ Prod.fst '' s₁ ×ˢ t₁), s ⊆ s₁
⊢ s ⊆ s₁
have inr₁ : ∀ (this : s ⊆ s₁), s ⊆ s₁
Tactic: rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ t ⊆ t₁
have this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
Tactic: have := image_mono (f := Prod.snd) H
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
⊢ t ⊆ t₁
have inr : ∀ (this : t ⊆ Prod.snd '' s₁ ×ˢ t₁), t ⊆ t₁
Tactic: rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
inr : ∀ (this : t ⊆ Prod.snd '' s₁ ×ˢ t₁), t ⊆ t₁
⊢ t ⊆ t₁
have inr₁ : ∀ (this : t ⊆ t₁), t ⊆ t₁
Tactic: rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁
have H₁ : s ⊆ s₁ ∧ t ⊆ t₁
Tactic: simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁
have rw : ¬(s = ∅ ∨ t = ∅)
Tactic: rw [prod_subset_prod_iff, or_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ ¬(s = ∅ ∨ t = ∅)
have rw : ¬s ×ˢ t = ∅
Tactic: rw [← Set.prod_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁
have mp : s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
mp : s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁
have mpr : s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁
have h₁ : (s₁ ×ˢ t₁).Nonempty
Tactic: have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : (s₁ ×ˢ t₁).Nonempty
⊢ s = s₁ ∧ t = t₁
have h₂ : s.Nonempty ∧ t.Nonempty
Tactic: rw [prod_nonempty_iff] at h h₁
Cleared hypotheses: h, heq, h₁
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : (s₁ ×ˢ t₁).Nonempty
h₂ : s.Nonempty ∧ t.Nonempty
heq₁ : s ×ˢ t = s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁
have h₃ : s₁.Nonempty ∧ t₁.Nonempty
Tactic: rw [prod_nonempty_iff] at h h₁
Cleared hypotheses: h, heq, h₁
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ s = s₁ ∧ t = t₁
have mp : Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
Tactic: rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
mp : Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
⊢ s = s₁ ∧ t = t₁
have mp₁ : Prod.fst '' s ×ˢ t = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
Tactic: rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
mp : Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
mp₁ : Prod.fst '' s ×ˢ t = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
⊢ s = s₁ ∧ t = t₁
have mp₂ : Prod.fst '' s₁ ×ˢ t₁ = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
Tactic: rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
mp : Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
mp₁ : Prod.fst '' s ×ˢ t = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₂ : Prod.fst '' s₁ ×ˢ t₁ = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
⊢ s = s₁ ∧ t = t₁
have mp₃ : True ∧ t = t₁
Tactic: rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
mp : Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
mp₁ : Prod.fst '' s ×ˢ t = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₂ : Prod.fst '' s₁ ×ˢ t₁ = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₃ : True ∧ t = t₁
⊢ s = s₁ ∧ t = t₁
have mp₄ : t = t₁
Tactic: rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
mp : Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
mp₁ : Prod.fst '' s ×ˢ t = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₂ : Prod.fst '' s₁ ×ˢ t₁ = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₃ : True ∧ t = t₁
mp₄ : t = t₁
⊢ s = s₁ ∧ t = t₁
have mp₅ : Prod.snd '' s ×ˢ t = t₁
Tactic: rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
mp : Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
mp₁ : Prod.fst '' s ×ˢ t = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₂ : Prod.fst '' s₁ ×ˢ t₁ = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₃ : True ∧ t = t₁
mp₄ : t = t₁
mp₅ : Prod.snd '' s ×ˢ t = t₁
⊢ s = s₁ ∧ t = t₁
have mp₆ : Prod.snd '' s ×ˢ t = Prod.snd '' s₁ ×ˢ t₁
Tactic: rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
mp : Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
mp₁ : Prod.fst '' s ×ˢ t = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₂ : Prod.fst '' s₁ ×ˢ t₁ = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₃ : True ∧ t = t₁
mp₄ : t = t₁
mp₅ : Prod.snd '' s ×ˢ t = t₁
mp₆ : Prod.snd '' s ×ˢ t = Prod.snd '' s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁
have mp₇ : Prod.snd '' s₁ ×ˢ t₁ = Prod.snd '' s₁ ×ˢ t₁
Tactic: rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)
have symm : s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
have inl : ∀ (h : s ×ˢ t = ∅), s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
Tactic: rcases eq_empty_or_nonempty (s ×ˢ t) with h | h
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
inl : ∀ (h : s ×ˢ t = ∅), s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
have inr : ∀ (h : (s ×ˢ t).Nonempty), s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
Tactic: rcases eq_empty_or_nonempty (s ×ˢ t) with h | h
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
have inl : s = s₁ ∧ t = t₁ → s₁ = ∅ ∨ t₁ = ∅
Tactic: simp_rw [h, @eq_comm _ ∅, prod_eq_empty_iff, prod_eq_empty_iff.mp h, true_and,
      or_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
have inr : s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
Tactic: rw [prod_eq_prod_iff_of_nonempty h]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
have h₁ : ¬(s = ∅ ∨ t = ∅)
Tactic: rw [nonempty_iff_ne_empty, Ne, prod_eq_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
have inr : s = s₁ ∧ t = t₁ ∨ False ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
Tactic: simp_rw [h, false_and, or_false]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
inr : s = s₁ ∧ t = t₁ ∨ False ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
have inr₁ : s = s₁ ∧ t = t₁ ∨ False ↔ s = s₁ ∧ t = t₁
Tactic: simp_rw [h, false_and, or_false]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁
have simp_rw : s = ∅ ∧ s₁ = ∅ → s = s₁
Tactic: simp_rw [prod_eq_prod_iff, ht.ne_empty, and_true, or_iff_left_iff_imp, or_false]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
ht : t.Nonempty
⊢ EqOn f f' s
have obtain : ∀ (x : β) (hxt : x ∈ t), EqOn f f' s
Tactic: obtain ⟨x, hxt⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x_1 : β
hxt : x_1 ∈ t
x : α
hxs : x ∈ s
⊢ f x = f' x
have h' : Prod.map f g (x, x_1) = Prod.map f' g' (x, x_1)
Tactic: have h' := h <| mk_mem_prod hxs hxt
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
hs : s.Nonempty
⊢ EqOn g g' t
have obtain : ∀ (x : α) (hxs : x ∈ s), EqOn g g' t
Tactic: obtain ⟨x, hxs⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x_1 : α
hxs : x_1 ∈ s
x : β
hxt : x ∈ t
⊢ g x = g' x
have h' : Prod.map f g (x_1, x) = Prod.map f' g' (x_1, x)
Tactic: have h' := h <| mk_mem_prod hxs hxt
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s : Set α
⊢ Eq (α := Set ((↑s : Type u_1) × (↑s : Type u_1)))
    ((Prod.map (fun (x : (↑s : Type u_1)) ↦ (↑x : α)) fun (x : (↑s : Type u_1)) ↦ (↑x : α)) ⁻¹' diagonal α)
    (diagonal (↑s : Type u_1))
have h : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s),
  Membership.mem (γ := Set ((↑s : Type u_1) × (↑s : Type u_1)))
      ((Prod.map (fun (x : (↑s : Type u_1)) ↦ (↑x : α)) fun (x : (↑s : Type u_1)) ↦ (↑x : α)) ⁻¹' diagonal α)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx, Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy) ↔
    Membership.mem (γ := Set ((↑s : Type u_1) × (↑s : Type u_1))) (diagonal (↑s : Type u_1))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx, Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
Tactic: ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
⊢ (range fun (x : α) ↦ (x, x)) = diagonal α
have h : ∀ (x y : α), Membership.mem (γ := Set (α × α)) (range fun (x : α) ↦ (x, x)) (x, y) ↔ (x, y) ∈ diagonal α
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s : Set (α × α)
⊢ diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
have rw : (range fun (x : α) ↦ (x, x)) ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
Tactic: rw [← range_diag, range_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s : Set (α × α)
rw : (range fun (x : α) ↦ (x, x)) ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
⊢ diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
have rw₁ : (∀ (y : α), (y, y) ∈ s) ↔ ∀ (x : α), (x, x) ∈ s
Tactic: rw [← range_diag, range_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s : Set α
⊢ (fun (x : α) ↦ (x, x)) '' s = diagonal α ∩ s ×ˢ s
have rw : (fun (x : α) ↦ (x, x)) '' s = (range fun (x : α) ↦ (x, x)) ∩ s ×ˢ s
Tactic: rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s : Set α
rw : (fun (x : α) ↦ (x, x)) '' s = (range fun (x : α) ↦ (x, x)) ∩ s ×ˢ s
⊢ (fun (x : α) ↦ (x, x)) '' s = diagonal α ∩ s ×ˢ s
have rw₁ : Eq (α := Set (α × α)) ((fun (x : α) ↦ (x, x)) '' s) ((fun (x : α) ↦ (x, x)) '' (fun (x : α) ↦ (x, x)) ⁻¹' s ×ˢ s)
Tactic: rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
s : Set α
rw : (fun (x : α) ↦ (x, x)) '' s = (range fun (x : α) ↦ (x, x)) ∩ s ×ˢ s
rw₁ : Eq (α := Set (α × α)) ((fun (x : α) ↦ (x, x)) '' s) ((fun (x : α) ↦ (x, x)) '' (fun (x : α) ↦ (x, x)) ⁻¹' s ×ˢ s)
⊢ (fun (x : α) ↦ (x, x)) '' s = diagonal α ∩ s ×ˢ s
have rw₂ : Eq (α := Set (α × α)) ((fun (x : α) ↦ (x, x)) '' s) ((fun (x : α) ↦ (x, x)) '' s)
Tactic: rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
⊢ Eq (α := Set (α → β)) (range (const α)) {f : α → β | ∀ (x y : α), f x = f y}
have refine : ∀ (f : α → β) (hf : Membership.mem (γ := Set (α → β)) {f : α → β | ∀ (x y : α), f x = f y} f), ∃ (a : β), const α a = f
Tactic: refine (range_eq_iff _ _).mpr ⟨fun _ _ _ ↦ rfl, fun f hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : Membership.mem (γ := Set (α → β)) {f : α → β | ∀ (x y : α), f x = f y} f
⊢ ∃ (a : β), const α a = f
have inl : ∀ (h : IsEmpty α), ∃ (a : β), const α a = f
Tactic: rcases isEmpty_or_nonempty α with h | ⟨⟨a⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : Membership.mem (γ := Set (α → β)) {f : α → β | ∀ (x y : α), f x = f y} f
inl : ∀ (h : IsEmpty α), ∃ (a : β), const α a = f
⊢ ∃ (a : β), const α a = f
have inr : ∀ (a : α), ∃ (a : β), const α a = f
Tactic: rcases isEmpty_or_nonempty α with h | ⟨⟨a⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
⊢ Eq (α := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' pullbackDiagonal f) (pullbackDiagonal snd)
have h : ∀ (p₁ p₂ : Pullback f g) (he : (p₁, p₂).1.snd = (p₁, p₂).2.snd),
  Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' pullbackDiagonal f)
      (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he) ↔
    Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (pullbackDiagonal snd)
      (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)
Tactic: ext ⟨⟨p₁, p₂⟩, he⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' pullbackDiagonal f)
      (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he) ↔
    Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (pullbackDiagonal snd)
      (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)
have h : Membership.mem (γ := Set (PullbackSelf (X := Pullback f g) snd)) (map_fst ⁻¹' {p : Pullback f f | p.fst = p.snd})
    (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he) ↔
  (↑(fst (Y := Z) (f := snd) (g := snd)
              (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
          X × Z).1 =
      (↑(snd (Y := Z) (f := snd) (g := snd)
              (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
          X × Z).1 ∧
    (↑(fst (Y := Z) (f := snd) (g := snd)
              (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
          X × Z).2 =
      (↑(snd (Y := Z) (f := snd) (g := snd)
              (Subtype.mk (p := fun (p : Pullback f g × Pullback f g) ↦ p.1.snd = p.2.snd) (p₁, p₂) he)) :
          X × Z).2
Tactic: simp_rw [pullbackDiagonal, mem_setOf, Subtype.ext_iff, Prod.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
⊢ toPullbackDiag f '' s = pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s
have h : ∀ (x : Pullback f f),
  x ∈ toPullbackDiag f '' s ↔ x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ toPullbackDiag f '' s ↔ x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s
have h : x ∈ toPullbackDiag f '' s → x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
h : x ∈ toPullbackDiag f '' s → x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s
⊢ x ∈ toPullbackDiag f '' s ↔ x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s
have h₁ : x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s → x ∈ toPullbackDiag f '' s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s → x ∈ toPullbackDiag f '' s
have h : ∀ (x y : X) (h : f (x, y).1 = f (x, y).2),
  Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (x, y) h ∈
      pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' s ×ˢ s →
    Subtype.mk (p := fun (p : X × X) ↦ f p.1 = f p.2) (x, y) h ∈ toPullbackDiag f '' s
Tactic: obtain ⟨⟨x, y⟩, h⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
X : Type u_1
Y : Sort u_2
f : X → Y
⊢ range (toPullbackDiag f) = pullbackDiagonal f
have rw : toPullbackDiag f '' univ = 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:
X : Type u_1
Y : Sort u_2
f : X → Y
rw : toPullbackDiag f '' univ = pullbackDiagonal f
⊢ range (toPullbackDiag f) = pullbackDiagonal f
have 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
Tactic: rw [← image_univ, image_toPullbackDiag, univ_prod_univ, preimage_univ, inter_univ]
-- 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
⊢ range (toPullbackDiag f) = pullbackDiagonal f
have rw₂ : pullbackDiagonal f ∩ Subtype.val (p := fun (p : X × X) ↦ f p.1 = f p.2) ⁻¹' univ = 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:
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
⊢ range (toPullbackDiag f) = pullbackDiagonal f
have rw₃ : pullbackDiagonal f ∩ univ = pullbackDiagonal f
Tactic: rw [← image_univ, image_toPullbackDiag, univ_prod_univ, preimage_univ, inter_univ]