awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
rwa :
  (e.extendDomain (p := fun (x : β) ↦
          Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) f.toEquivRange :
        (a : β) → β)
      b =
    b
rwa₁ : b = b
h₁ : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
rwa₂ : b = b
h₂ h₃ h₄ : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ (e.viaFintypeEmbedding f : (a : β) → β) b = b

Tactic:
rwa [Equiv.Perm.viaFintypeEmbedding, Equiv.Perm.extendDomain_apply_not_subtype]

Premises used: Equiv.Perm.extendDomain_apply_not_subtype, Equiv.Perm.viaFintypeEmbedding
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
x : α
⊢ x ∈ fs ↔ x ∈ s

Tactic:
simp [fs]
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
⊢ ∀ (x : α), x ∈ fs ↔ x ∈ s

Tactic:
have hs (x : α) : x ∈ fs ↔ x ∈ s := by simp [fs]
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
x : α
⊢ x ∈ ft ↔ x ∈ t

Tactic:
simp [ft]
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
⊢ ∀ (x : α), x ∈ ft ↔ x ∈ t

Tactic:
have ht (x : α) : x ∈ ft ↔ x ∈ t := by simp [ft]
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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
x : α
⊢ x ∈ fs \ ft ↔ x ∈ s \ t

Tactic:
simp [hs, ht]
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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
⊢ ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t

Tactic:
have hst (x : α) : x ∈ fs \ ft ↔ x ∈ s \ t := by simp [hs, ht]
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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
x : α
⊢ x ∈ ft \ fs ↔ x ∈ t \ s

Tactic:
simp [hs, ht]
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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
⊢ ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s

Tactic:
have hts (x : α) : x ∈ ft \ fs ↔ x ∈ t \ s := by simp [hs, ht]
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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
rw : Fintype.card.{u_1} { x : α // x ∈ s } = Fintype.card.{u_1} { x : α // x ∈ t }
⊢ fs.card = ft.card

Tactic:
rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]

Premises used: Fintype.subtype_card
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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
⊢ Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)

Tactic:
h
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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
⊢ Fintype.card.{u_1} { x : α // x ∈ s } = Fintype.card.{u_1} { x : α // x ∈ t }

Tactic:
convert! h
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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
⊢ fs.card = ft.card

Tactic:
have hc : fs.card = ft.card := by
    rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]; convert! h
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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
⊢ (fs \ ft).card = (ft \ fs).card

Tactic:
replace hc := Finset.card_sdiff_comm hc
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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 \ ft).card = (ft \ fs).card
⊢ Fintype.card.{u_1} { x : α // x ∈ s \ t } = Fintype.card.{u_1} { x : α // x ∈ t \ s }

Tactic:
rw [← Fintype.subtype_card (fs \ ft) hst, ← Fintype.subtype_card (ft \ fs) hts] at hc

Premises used: Fintype.subtype_card, SDiff.sdiff
-- Module: Mathlib.Logic.Equiv.Fintype
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)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
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 : Fintype.card.{u_1} { x : α // x ∈ s \ t } = Fintype.card.{u_1} { x : α // x ∈ t \ s }
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)

Tactic:
exact ((Fintype.card_eq (_F := (_)) (_G := (_))).mp hc).some

Premises used: Fintype.card_eq, Nonempty.some, Iff.mp
-- Module: Mathlib.Logic.Equiv.Fintype
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)
h₁ : ∀ (x : α), x ∈ spᶜ ↔ x ∈ sq \ sp ∪ (sp ∪ sq)ᶜ
⊢ spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Fintype
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 \ sp ∪ (sp ∪ sq)ᶜ

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fintype
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
h₁₄ : x ∉ sp → x ∈ sq → ¬x ∉ sp → False
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

Tactic:
tauto
-- Module: Mathlib.Logic.Equiv.Fintype
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)ᶜ
h₁ : ∀ (x : α), x ∈ sqᶜ ↔ x ∈ sp \ sq ∪ (sp ∪ sq)ᶜ
⊢ sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Fintype
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 \ sq ∪ (sp ∪ sq)ᶜ

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fintype
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
h₈ : x ∉ sp → x ∉ sq → x ∉ sq
h₉ : x ∈ sp → x ∉ sq → x ∉ sq
h₁₀ : x ∉ sp → x ∉ sq → x ∉ sq
h₁₁ : x ∈ sp → x ∉ sq → x ∈ sq → False
h₁₂ : x ∉ sp → x ∉ sq → x ∈ sq → False
h₁₃ : x ∉ sq → x ∈ sp → x ∉ sp → False
h₁₄ : x ∉ sq → x ∈ sp → ¬x ∉ sq → False
h₁₅ : x ∈ sp → x ∉ sq → x ∈ sq → False
h₁₆ : x ∉ sp → x ∉ sq → x ∈ sq → False
⊢ x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq

Tactic:
tauto
-- Module: Mathlib.Logic.Equiv.Fintype
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)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
simp : ∀ ⦃a : α⦄, a ∈ sq → a ∉ sp → a ∈ sq
⊢ Disjoint (sq \ sp) (sp ∪ sq)ᶜ

Tactic:
simp [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Logic.Equiv.Fintype
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)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ : ∀ ⦃a : α⦄, a ∈ sq → a ∉ sp → a ∈ sq
⊢ ∀ ⦃a : α⦄, a ∈ sq → a ∉ sp → a ∈ sq

Tactic:
tauto
-- Module: Mathlib.Logic.Equiv.Fintype
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)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
epc : (↑spᶜ : Type u_1) ≃ (↑(sq \ sp) : Type u_1) ⊕ (↑(sp ∪ sq)ᶜ : Type u_1) :=
  (setCongr (s := spᶜ) (t := sq \ sp ∪ (sp ∪ sq)ᶜ) hpc).trans (Set.union (s := sq \ sp) (t := (sp ∪ sq)ᶜ) ⋯)
simp : ∀ ⦃a : α⦄, a ∈ sp → a ∉ sq → a ∉ sp → a ∈ sq
⊢ Disjoint (sp \ sq) (sp ∪ sq)ᶜ

Tactic:
simp [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Logic.Equiv.Fintype
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)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
epc : (↑spᶜ : Type u_1) ≃ (↑(sq \ sp) : Type u_1) ⊕ (↑(sp ∪ sq)ᶜ : Type u_1) :=
  (setCongr (s := spᶜ) (t := sq \ sp ∪ (sp ∪ sq)ᶜ) hpc).trans (Set.union (s := sq \ sp) (t := (sp ∪ sq)ᶜ) ⋯)
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ : ∀ ⦃a : α⦄, a ∈ sp → a ∉ sq → a ∉ sp → a ∈ sq
⊢ ∀ ⦃a : α⦄, a ∈ sp → a ∉ sq → a ∉ sp → a ∈ sq

Tactic:
tauto
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : { x : α // p x } ≃ { x : α // q x }
x : α
hx : p x
⊢ Eq (α := α) ((e.extendSubtype (p := p) (q := q) : (a : α) → α) x : α)
    ((↑((e : (a : { x : α // p x }) → { x : α // q x }) (Subtype.mk (p := fun (x : α) ↦ p x) x hx)) : α) : α)

Tactic:
simp [extendSubtype, subtypeCongr, sumCompl_symm_apply_of_pos hx]

Premises used: Equiv.extendSubtype, Equiv.subtypeCongr, Equiv.sumCompl_symm_apply_of_pos
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : { x : α // p x } ≃ { x : α // q x }
x : α
hx : p x
⊢ q ((e.extendSubtype (p := p) (q := q) : (a : α) → α) x)

Tactic:
(e.extendSubtype_apply_of_mem _ hx).symm ▸ (e ⟨x, hx⟩).2

Premises used: Eq.rec, Subtype.mk, Eq.symm, Equiv.extendSubtype_apply_of_mem, DFunLike.coe, Subtype.property
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : { x : α // p x } ≃ { x : α // q x }
x : α
hx : ¬p x
simp :
  Eq.{u_1 + 1} (α := α)
    (↑((e.toCompl (p := p) (q := q) : (a : { x : α // ¬p x }) → { x : α // ¬q x })
          (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx)) :
      α)
    (↑((e.toCompl (p := p) (q := q) : (a : (↑{x : α | ¬p x} : Type u_1)) → (↑{x : α | ¬q x} : Type u_1))
          (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {x : α | ¬p x} x) x hx)) :
      α)
⊢ Eq (α := α) ((e.extendSubtype (p := p) (q := q) : (a : α) → α) x : α)
    ((↑((e.toCompl (p := p) (q := q) : (a : (↑{x : α | ¬p x} : Type u_1)) → (↑{x : α | ¬q x} : Type u_1))
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {x : α | ¬p x} x) x hx)) :
        α) :
      α)

Tactic:
simp only [extendSubtype, subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply,
    sumCompl_symm_apply_of_neg hx, Sum.map_inr, sumCompl_apply_inr]

Premises used: Equiv.trans_apply, Equiv.sumCompl_apply_inr, Equiv.extendSubtype, Equiv.sumCongr_apply, Sum.map_inr, Equiv.subtypeCongr, Equiv.sumCompl_symm_apply_of_neg
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : { x : α // p x } ≃ { x : α // q x }
x : α
hx : ¬p x
⊢ Eq.{u_1 + 1} (α := α)
    (↑((e.toCompl (p := p) (q := q) : (a : { x : α // ¬p x }) → { x : α // ¬q x })
          (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx)) :
      α)
    (↑((e.toCompl (p := p) (q := q) : (a : (↑{x : α | ¬p x} : Type u_1)) → (↑{x : α | ¬q x} : Type u_1))
          (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {x : α | ¬p x} x) x hx)) :
      α)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : { x : α // p x } ≃ { x : α // q x }
x : α
hx : ¬p x
⊢ ¬q ((e.extendSubtype (p := p) (q := q) : (a : α) → α) x)

Tactic:
e.extendSubtype_apply_of_not_mem _ hx ▸ (e.toCompl ⟨x, hx⟩).2

Premises used: Eq.rec, Subtype.mk, Eq.symm, DFunLike.coe, Equiv.toCompl, Equiv.extendSubtype_apply_of_not_mem, Subtype.property
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
⊢ Finite.{u_2 + 1} (↑{x : β | x ∈ Set.range f} : Type u_2)

Tactic:
have : Finite {x | x ∈ Set.range f} := .of_surjective _ (Set.codRestrict_range_surjective f)
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
this : Finite.{u_2 + 1} (↑{x : β | x ∈ Set.range f} : Type u_2)
⊢ ∃ (σ : Perm β), ∀ (a : α), (σ : (a : β) → β) (f a) = g a

Tactic:
⟨((Equiv.ofInjective f hf).symm.trans (Equiv.ofInjective g hg)).extendSubtype, ?_⟩

Premises used: Equiv.trans, Equiv.extendSubtype, Equiv.ofInjective, Exists.intro, Equiv.symm
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
this : Finite.{u_2 + 1} (↑{x : β | x ∈ Set.range f} : Type u_2)
refine :
  ∀ (a : α),
    (((ofInjective f hf).symm.trans (ofInjective g hg)).extendSubtype (p := Membership.mem (Set.range f)) (q :=
            Membership.mem (Set.range g)) :
          (a : β) → β)
        (f a) =
      g a
⊢ ∃ (σ : Perm β), ∀ (a : α), (σ : (a : β) → β) (f a) = g a

Tactic:
refine ⟨((Equiv.ofInjective f hf).symm.trans (Equiv.ofInjective g hg)).extendSubtype, ?_⟩
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
this : Finite.{u_2 + 1} (↑{x : β | x ∈ Set.range f} : Type u_2)
⊢ ∀ (a : α),
    (((ofInjective f hf).symm.trans (ofInjective g hg)).extendSubtype (p := Membership.mem (Set.range f)) (q :=
            Membership.mem (Set.range g)) :
          (a : β) → β)
        (f a) =
      g a

Tactic:
simp [Equiv.extendSubtype_apply_of_mem]

Premises used: Equiv.extendSubtype_apply_of_mem