awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
let let₁ let₂ let₃ : (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₄ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have let₅ : let fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
let ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
(hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
Tactic: classical
  let fs : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ s))
  let ft : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ t))
  have hs (x : α) : x ∈ fs ↔ x ∈ s := by simp [fs]
  have ht (x : α) : x ∈ ft ↔ x ∈ t := by simp [ft]
  have hst (x : α) : x ∈ fs \ ft ↔ x ∈ s \ t := by simp [hs, ht]
  have hts (x : α) : x ∈ ft \ fs ↔ x ∈ t \ s := by simp [hs, ht]
  have hc : fs.card = ft.card := by
    rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]; convert! h
  replace hc := Finset.card_sdiff_comm hc
  rw [← Fintype.subtype_card (fs \ ft) hst, ← Fintype.subtype_card (ft \ fs) hts] at hc
  exact ((Fintype.card_eq (_F := (_)) (_G := (_))).mp hc).some
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
let let₁ let₂ let₃ : (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₄ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₅ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have let₆ : let fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
let ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
(hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
  (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
    (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
Tactic: classical
  let fs : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ s))
  let ft : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ t))
  have hs (x : α) : x ∈ fs ↔ x ∈ s := by simp [fs]
  have ht (x : α) : x ∈ ft ↔ x ∈ t := by simp [ft]
  have hst (x : α) : x ∈ fs \ ft ↔ x ∈ s \ t := by simp [hs, ht]
  have hts (x : α) : x ∈ ft \ fs ↔ x ∈ t \ s := by simp [hs, ht]
  have hc : fs.card = ft.card := by
    rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]; convert! h
  replace hc := Finset.card_sdiff_comm hc
  rw [← Fintype.subtype_card (fs \ ft) hst, ← Fintype.subtype_card (ft \ fs) hts] at hc
  exact ((Fintype.card_eq (_F := (_)) (_G := (_))).mp hc).some
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
let let₁ let₂ let₃ : (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₄ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₅ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₆ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
    (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
      (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have let₇ : let fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
let ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
(hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
  (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
    (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) →
      (hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
Tactic: classical
  let fs : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ s))
  let ft : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ t))
  have hs (x : α) : x ∈ fs ↔ x ∈ s := by simp [fs]
  have ht (x : α) : x ∈ ft ↔ x ∈ t := by simp [ft]
  have hst (x : α) : x ∈ fs \ ft ↔ x ∈ s \ t := by simp [hs, ht]
  have hts (x : α) : x ∈ ft \ fs ↔ x ∈ t \ s := by simp [hs, ht]
  have hc : fs.card = ft.card := by
    rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]; convert! h
  replace hc := Finset.card_sdiff_comm hc
  rw [← Fintype.subtype_card (fs \ ft) hst, ← Fintype.subtype_card (ft \ fs) hts] at hc
  exact ((Fintype.card_eq (_F := (_)) (_G := (_))).mp hc).some
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
let let₁ let₂ let₃ : (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₄ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₅ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₆ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
    (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
      (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₇ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
    (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
      (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) →
        (hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have let₈ : let fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
let ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
(hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
  (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
    (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) →
      (hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s) →
        (hc : fs.card = ft.card) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
Tactic: classical
  let fs : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ s))
  let ft : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ t))
  have hs (x : α) : x ∈ fs ↔ x ∈ s := by simp [fs]
  have ht (x : α) : x ∈ ft ↔ x ∈ t := by simp [ft]
  have hst (x : α) : x ∈ fs \ ft ↔ x ∈ s \ t := by simp [hs, ht]
  have hts (x : α) : x ∈ ft \ fs ↔ x ∈ t \ s := by simp [hs, ht]
  have hc : fs.card = ft.card := by
    rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]; convert! h
  replace hc := Finset.card_sdiff_comm hc
  rw [← Fintype.subtype_card (fs \ ft) hst, ← Fintype.subtype_card (ft \ fs) hts] at hc
  exact ((Fintype.card_eq (_F := (_)) (_G := (_))).mp hc).some
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
⊢ spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
have h₁ : ∀ (x : α), x ∈ spᶜ ↔ x ∈ sq \ sp ∪ (sp ∪ sq)ᶜ
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
x : α
⊢ x ∈ spᶜ ↔ x ∈ sq \ sp ∪ (sp ∪ sq)ᶜ
have h₁ : x ∉ sp ↔ x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
Tactic: simp
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
x : α
⊢ x ∉ sp ↔ x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
have h₁ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
x : α
h₁ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
⊢ x ∉ sp ↔ x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
have h₂ : x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq → x ∉ sp
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
x : α
h₁ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq → x ∉ sp
h₃ h₄ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
⊢ x ∉ sp ↔ x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
have h₅ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sp
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
x : α
h₁ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq → x ∉ sp
h₃ h₄ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sp
⊢ x ∉ sp ↔ x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
have h₆ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sq
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
x : α
h₁ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq → x ∉ sp
h₃ h₄ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sp
h₆ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sq
⊢ x ∉ sp ↔ x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
have h₇ : x ∈ sq → x ∉ sp → x ∉ sp
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
x : α
h₁ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq → x ∉ sp
h₃ h₄ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sp
h₆ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sq
h₇ : x ∈ sq → x ∉ sp → x ∉ sp
⊢ x ∉ sp ↔ x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
have h₈ : x ∉ sp → x ∉ sq → x ∉ sp
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
x : α
h₁ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq → x ∉ sp
h₃ h₄ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sp
h₆ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sq
h₇ : x ∈ sq → x ∉ sp → x ∉ sp
h₈ : x ∉ sp → x ∉ sq → x ∉ sp
h₉ : x ∈ sq → x ∉ sp → x ∉ sp
h₁₀ : x ∉ sp → x ∉ sq → x ∉ sp
h₁₁ : x ∈ sq → x ∉ sp → x ∈ sp → False
h₁₂ : x ∉ sp → x ∉ sq → x ∈ sp → False
⊢ x ∉ sp ↔ x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
have h₁₃ : x ∉ sp → x ∈ sq → x ∉ sq → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
x : α
h₁ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq → x ∉ sp
h₃ h₄ : x ∉ sp → x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sp
h₆ : x ∉ sp → ¬(x ∈ sq ∧ x ∉ sp) → x ∉ sq
h₇ : x ∈ sq → x ∉ sp → x ∉ sp
h₈ : x ∉ sp → x ∉ sq → x ∉ sp
h₉ : x ∈ sq → x ∉ sp → x ∉ sp
h₁₀ : x ∉ sp → x ∉ sq → x ∉ sp
h₁₁ : x ∈ sq → x ∉ sp → x ∈ sp → False
h₁₂ : x ∉ sp → x ∉ sq → x ∈ sp → False
h₁₃ : x ∉ sp → x ∈ sq → x ∉ sq → False
⊢ x ∉ sp ↔ x ∈ sq ∧ x ∉ sp ∨ x ∉ sp ∧ x ∉ sq
have h₁₄ : x ∉ sp → x ∈ sq → ¬x ∉ sp → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
⊢ sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
have h₁ : ∀ (x : α), x ∈ sqᶜ ↔ x ∈ sp \ sq ∪ (sp ∪ sq)ᶜ
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x : α
⊢ x ∈ sqᶜ ↔ x ∈ sp \ sq ∪ (sp ∪ sq)ᶜ
have h₁ : x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
Tactic: simp
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x : α
⊢ x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
have h₁ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x : α
h₁ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
⊢ x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
have h₂ : x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq → x ∉ sq
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x : α
h₁ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq → x ∉ sq
h₃ h₄ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
⊢ x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
have h₅ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sp
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x : α
h₁ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq → x ∉ sq
h₃ h₄ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sp
⊢ x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
have h₆ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sq
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x : α
h₁ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq → x ∉ sq
h₃ h₄ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sp
h₆ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sq
⊢ x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
have h₇ : x ∈ sp → x ∉ sq → x ∉ sq
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x : α
h₁ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq → x ∉ sq
h₃ h₄ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sp
h₆ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sq
h₇ : x ∈ sp → x ∉ sq → x ∉ sq
⊢ x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
have h₈ : x ∉ sp → x ∉ sq → x ∉ sq
Tactic: tauto