awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ ∀ (x : α × α), x ∈ s.toFinset.offDiag ↔ x ∈ s.offDiag

Tactic:
simp
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype (↑s : Type u_1)
ht : Fintype (↑t : Type u_2)
rw : Fintype (↑((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t) : Type u_3)
⊢ Fintype (↑(image2 f s t) : Type u_3)

Tactic:
rw [← image_prod]

Premises used: Set.image_prod
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype (↑s : Type u_1)
ht : Fintype (↑t : Type u_2)
⊢ Fintype (↑((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t) : Type u_3)

Tactic:
apply Set.fintypeImage

Premises used: Set.fintypeImage
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
inst : Finite.{u_1 + 1} (↑s : Type u_1)
inst_1 : Finite.{u_2 + 1} (↑t : Type u_2)
⊢ Finite (↑(s ×ˢ t) : Type (max u_1 u_2))

Tactic:
Finite.of_equiv _ (Equiv.Set.prod s t).symm

Premises used: Finite.of_equiv, Equiv.Set.prod, Equiv.symm
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst : Finite.{u_1 + 1} (↑s : Type u_1)
inst_1 : Finite.{u_2 + 1} (↑t : Type u_2)
rw : Finite.{u_3 + 1} (↑((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t) : Type u_3)
⊢ Finite.{u_3 + 1} (↑(image2 f s t) : Type u_3)

Tactic:
rw [← image_prod]

Premises used: Set.image_prod
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst : Finite.{u_1 + 1} (↑s : Type u_1)
inst_1 : Finite.{u_2 + 1} (↑t : Type u_2)
⊢ Finite.{u_3 + 1} (↑((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t) : Type u_3)

Tactic:
infer_instance
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Finite.{u_2 + 1} (↑t : Type u_2)

Tactic:
have := ht.to_subtype
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this_1 : Finite.{u_1 + 1} (↑s : Type u_1)
this : Finite.{u_2 + 1} (↑t : Type u_2)
⊢ (s ×ˢ t).Finite

Tactic:
apply toFinite

Premises used: Set.toFinite
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Finite
⊢ t.Nonempty → s.Finite

Tactic:
fun ⟨b, hb⟩ => (h.image Prod.fst).subset fun a ha => ⟨(a, b), ⟨ha, hb⟩, rfl⟩

Premises used: _private.0.Set.Finite.of_prod_left.match_1, Set.Finite, Prod.mk, Set.Finite.subset, Set.Finite.image, Prod.fst, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Finite
⊢ s.Nonempty → t.Finite

Tactic:
fun ⟨a, ha⟩ => (h.image Prod.snd).subset fun b hb => ⟨(a, b), ⟨ha, hb⟩, rfl⟩

Premises used: _private.0.Set.Finite.of_prod_left.match_1, Set.Finite, Prod.mk, Set.Finite.subset, Set.Finite.image, And.intro, Exists.intro, Prod.snd, rfl
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Infinite
ht : t.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
fun h => hs <| h.of_prod_left ht

Premises used: Set.Finite.of_prod_left, Not, Set.Infinite
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
ht : t.Infinite
hs : s.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
fun h => ht <| h.of_prod_right hs

Premises used: Set.Finite.of_prod_right, Not, Set.Infinite
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
refine_1 : ∀ (h : (s ×ˢ t).Infinite), s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
refine_2 : s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
refine_1 : ¬(t.Nonempty → s.Finite) ∨ ¬(s.Nonempty → t.Finite)
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
simp_rw [Set.Infinite, @and_comm ¬_, ← Classical.not_imp]

Premises used: and_comm, Classical.not_imp, Set.Infinite
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
refine_1 : ∀ (this : (t.Nonempty → s.Finite) ∧ (s.Nonempty → t.Finite)), False
⊢ ¬(t.Nonempty → s.Finite) ∨ ¬(s.Nonempty → t.Finite)

Tactic:
by_contra!
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
this : (t.Nonempty → s.Finite) ∧ (s.Nonempty → t.Finite)
⊢ False

Tactic:
h ((this.1 h.nonempty.snd).prod <| this.2 h.nonempty.fst)

Premises used: Set.Nonempty.snd, Set.Infinite.nonempty, And.right, Set.Finite.prod, And.left, Set.Nonempty.fst
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
this : (t.Nonempty → s.Finite) ∧ (s.Nonempty → t.Finite)
⊢ False

Tactic:
exact h ((this.1 h.nonempty.snd).prod <| this.2 h.nonempty.fst)

Premises used: Set.Nonempty.snd, Set.Infinite.nonempty, And.right, Set.Finite.prod, And.left, Set.Nonempty.fst
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s.Infinite ∧ t.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
h.1.prod_left h.2

Premises used: Set.Infinite.prod_left, And.right, And.left
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s.Infinite ∧ t.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
exact h.1.prod_left h.2

Premises used: Set.Infinite.prod_left, And.right, And.left
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
h.1.prod_right h.2

Premises used: Set.Infinite.prod_right, And.right, And.left
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
exact h.1.prod_right h.2

Premises used: Set.Infinite.prod_right, And.right, And.left
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
contrapose! : (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)

Tactic:
contrapose! +distrib
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
Set.infinite_prod

Premises used: Set.infinite_prod
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
exact Set.infinite_prod

Premises used: Set.infinite_prod
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.offDiag.Finite

Tactic:
(hs.prod hs).subset s.offDiag_subset_prod

Premises used: Set.offDiag_subset_prod, Set.Finite.subset, Set.Finite.prod
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Finite.{u_2 + 1} (↑t : Type u_2)

Tactic:
have := ht.to_subtype
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this_1 : Finite.{u_1 + 1} (↑s : Type u_1)
this : Finite.{u_2 + 1} (↑t : Type u_2)
⊢ (image2 f s t).Finite

Tactic:
apply toFinite

Premises used: Set.toFinite
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
⊢ ∀ (a : α × β), a ∈ hs.toFinset (s := s) ×ˢ ht.toFinset (s := t) ↔ a ∈ ⋯.toFinset (s := s ×ˢ t)

Tactic:
simp
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ ∀ (a : α × α), a ∈ ⋯.toFinset (s := s.offDiag) ↔ a ∈ hs.toFinset (s := s).offDiag

Tactic:
simp
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
⊢ (Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite

Tactic:
⟨fun h => (h.1.prod h.2).subset fun _ h => ⟨mem_image_of_mem _ h, mem_image_of_mem _ h⟩,
    fun h => ⟨h.image _, h.image _⟩⟩

Premises used: Set.Finite.subset, Set.Finite.image, Prod.fst, And.right, Set.Finite.prod, And.left, Set.mem_image_of_mem, And.intro, Iff.intro, Prod.snd
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
b : β
hs : s.Infinite
hb : b ∈ t
hf : InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
⊢ (image2 f s t).Infinite

Tactic:
(hs.image hf).mono <| image_subset_image2_left hb

Premises used: Set.Infinite.mono, Set.Infinite.image, Set.image_subset_image2_left
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
a : α
ht : t.Infinite
ha : a ∈ s
hf : InjOn (f a) t
⊢ (image2 f s t).Infinite

Tactic:
(ht.image hf).mono <| image_subset_image2_right ha

Premises used: Set.Infinite.mono, Set.Infinite.image, Set.image_subset_image2_right
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
⟨fun h => Set.infinite_prod.1 ?_, ?_⟩

Premises used: Set.infinite_prod, Iff.intro, Iff.mp
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
refine_1 : ∀ (h : (image2 f s t).Infinite), (s ×ˢ t).Infinite
refine_2 : s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite
⊢ (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
refine ⟨fun h => Set.infinite_prod.1 ?_, ?_⟩
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (image2 f s t).Infinite
⊢ (uncurry f '' s ×ˢ t).Infinite

Tactic:
rw [← image_uncurry_prod] at h

Premises used: Set.image_uncurry_prod
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (uncurry f '' s ×ˢ t).Infinite
⊢ (s ×ˢ t).Infinite

Tactic:
h.of_image _

Premises used: Set.Infinite.of_image
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (uncurry f '' s ×ˢ t).Infinite
⊢ (s ×ˢ t).Infinite

Tactic:
exact h.of_image _

Premises used: Set.Infinite.of_image
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
hs : s.Infinite
b : β
hb : b ∈ t
⊢ (image2 f s t).Infinite

Tactic:
hs.image2_left hb (hfs _ hb)

Premises used: Set.Infinite.image2_left
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
hs : s.Infinite
b : β
hb : b ∈ t
⊢ (image2 f s t).Infinite

Tactic:
exact hs.image2_left hb (hfs _ hb)

Premises used: Set.Infinite.image2_left
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
ht : t.Infinite
a : α
ha : a ∈ s
⊢ (image2 f s t).Infinite

Tactic:
ht.image2_right ha (hft _ ha)

Premises used: Set.Infinite.image2_right
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
ht : t.Infinite
a : α
ha : a ∈ s
⊢ (image2 f s t).Infinite

Tactic:
exact ht.image2_right ha (hft _ ha)

Premises used: Set.Infinite.image2_right
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (x : α) ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
contrapose! : (image2 f s t).Infinite ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty
⊢ (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
contrapose! +distrib
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (x : α) ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
rw : s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty
⊢ (image2 f s t).Infinite ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty

Tactic:
rw [Set.infinite_image2 hfs hft]

Premises used: Set.infinite_image2
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (x : α) ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty

Tactic:
grind only [Set.Infinite.nonempty]

Premises used: Set.Infinite.nonempty
-- Module: Mathlib.Data.Finite.Set
Goal:
α : Type u
β : Type v
s : Set α
f : α → β
h : InjOn f s
inst : Finite.{v + 1} (↑(f '' s) : Type v)
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
Finite.of_equiv _ (Equiv.ofBijective _ h.bijOn_image.bijective).symm

Premises used: Finite.of_equiv, Set.InjOn.bijOn_image, Equiv.ofBijective, Set.BijOn.bijective, Equiv.symm
-- Module: Mathlib.Data.Finite.Set
Goal:
α : Type u
ι : Sort w
f : ι → α
hf : Function.Injective f
inst : Finite.{u + 1} (↑(range f) : Type u)
⊢ Finite ι

Tactic:
Finite.of_injective (Set.rangeFactorization f) (hf.codRestrict _)

Premises used: Function.Injective.codRestrict, Set.rangeFactorization, Finite.of_injective
-- Module: Mathlib.Data.Finite.Sigma
Goal:
α : Type u_1
β : α → Type u_2
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_2 + 1} (β a)
this_1 : Fintype α := Fintype.ofFinite α
this : (a : α) → Fintype (β a) := fun (a : α) ↦ Fintype.ofFinite (β a)
⊢ Finite ((a : α) × β a)

Tactic:
infer_instance
-- Module: Mathlib.Data.Finite.Sigma
Goal:
α : Type u_1
ι : Sort u_2
π : ι → Sort u_3
inst : Finite ι
inst_1 : ∀ (i : ι), Finite.{u_3} (π i)
⊢ Finite ((i : ι) ×' π i)

Tactic:
of_equiv _ (Equiv.psigmaEquivSigmaPLift π).symm

Premises used: Finite.of_equiv, Equiv.psigmaEquivSigmaPLift, Equiv.symm
-- Module: Mathlib.Data.Finite.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
haveI : ∀ (this : Fintype α), Finite (α ⊕ β)
⊢ Finite (α ⊕ β)

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this : Fintype α
haveI : ∀ (this : Fintype β), Finite (α ⊕ β)
⊢ Finite (α ⊕ β)

Tactic:
haveI := Fintype.ofFinite β
-- Module: Mathlib.Data.Finite.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this_1 : Fintype α
this : Fintype β
⊢ Finite (α ⊕ β)

Tactic:
infer_instance
-- Module: Mathlib.Data.Finite.Sum
Goal:
α : Type u_1
β : Type u_3
inst : Finite (α ⊕ β)
⊢ Finite α

Tactic:
of_injective (Sum.inl : α → α ⊕ β) Sum.inl_injective

Premises used: Sum.inl_injective, Sum.inl, Finite.of_injective
-- Module: Mathlib.Data.Finite.Sum
Goal:
β : Type u_2
α : Type u_3
inst : Finite (α ⊕ β)
⊢ Finite β

Tactic:
of_injective (Sum.inr : β → α ⊕ β) Sum.inr_injective

Premises used: Sum.inr_injective, Sum.inr, Finite.of_injective
-- Module: Mathlib.Data.Finite.Sum
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite α
inst_1 : Finite β
⊢ Finite (α ⊕' β)

Tactic:
of_equiv _ ((Equiv.psumEquivSum _ _).symm.trans (Equiv.plift.psumCongr Equiv.plift))

Premises used: Finite.of_equiv, Equiv.psumEquivSum, Equiv.trans, Equiv.psumCongr, Equiv.plift, Equiv.symm
-- Module: Mathlib.Data.Finite.Sum
Goal:
α : Sort u_3
β : Sort u_4
inst : Finite (α ⊕' β)
⊢ Finite α

Tactic:
of_injective (PSum.inl : α → α ⊕' β) PSum.inl_injective

Premises used: PSum.inl_injective, PSum.inl, Finite.of_injective
-- Module: Mathlib.Data.Finite.Sum
Goal:
α : Sort u_3
β : Sort u_4
inst : Finite (α ⊕' β)
⊢ Finite β

Tactic:
of_injective (PSum.inr : β → α ⊕' β) PSum.inr_injective

Premises used: PSum.inr, PSum.inr_injective, Finite.of_injective
-- Module: Mathlib.Data.Finite.Vector
Goal:
α : Type u_1
inst : Finite α
n : ℕ
haveI : ∀ (this : Fintype α), Finite.{u_1 + 1} (Vector α n)
⊢ Finite.{u_1 + 1} (Vector α n)

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Vector
Goal:
α : Type u_1
inst : Finite α
n : ℕ
this : Fintype α
⊢ Finite.{u_1 + 1} (Vector α n)

Tactic:
infer_instance
-- Module: Mathlib.Data.Finite.Vector
Goal:
α : Type u_1
inst : Finite α
n : ℕ
haveI : ∀ (this : Fintype α), Finite.{u_1 + 1} (Sym α n)
⊢ Finite.{u_1 + 1} (Sym α n)

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Vector
Goal:
α : Type u_1
inst : Finite α
n : ℕ
this : Fintype α
⊢ Finite.{u_1 + 1} (Sym α n)

Tactic:
infer_instance
-- Module: Mathlib.Data.Finite.Vector
Goal:
α : Type u_1
inst : Finite α
n : ℕ
haveI haveI₁ haveI₂ : ∀ (this : Fintype α), Finite.{u_1 + 1} (Sym α n)
⊢ Finite.{u_1 + 1} (Sym α n)

Tactic:
classical
  haveI := Fintype.ofFinite α
  infer_instance
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
l : List (Sigma β)
⊢ (↑l : Multiset (Sigma β)).keys (β := β) = (↑(l.keys (β := β)) : Multiset α)

Tactic:
rfl

Premises used: Multiset.map, List.keys, Multiset.keys, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
⊢ Eq.{u + 1} (α := Multiset α) (keys (β := β) 0) 0

Tactic:
rfl

Premises used: Multiset.map, List.map, Multiset.zero, Multiset.ofList, Multiset.keys, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
a : α
b : β a
s : Multiset (Sigma β)
⊢ (Sigma.mk (β := β) a b ::ₘ s).keys (β := β) = a ::ₘ s.keys (β := β)

Tactic:
simp [keys]

Premises used: Multiset.keys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
a : α
b : β a
⊢ Eq (α := Multiset α) (keys (β := β) {Sigma.mk (β := β) a b}) {a}

Tactic:
rfl

Premises used: Multiset.map, List.map, Multiset.cons, Multiset.ofList, Multiset.keys, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
l : List (Sigma β)
⊢ (↑l : Multiset (Sigma β)).NodupKeys (β := β) ↔ l.NodupKeys (β := β)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiset.NodupKeys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
mk :
  ∀ (l : List ((a : α) × β a)),
    (keys (β := fun (a : α) ↦ β a)
          (Quot.mk (⇑(isSetoid ((a : α) × β a)) : List ((a : α) × β a) → List ((a : α) × β a) → Prop) l)).Nodup ↔
      NodupKeys (β := fun (a : α) ↦ β a)
        (Quot.mk (⇑(isSetoid ((a : α) × β a)) : List ((a : α) × β a) → List ((a : α) × β a) → Prop) l)
⊢ m.keys (β := fun (a : α) ↦ β a).Nodup ↔ m.NodupKeys (β := fun (a : α) ↦ β a)

Tactic:
rcases m with ⟨l⟩
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
l : List ((a : α) × β a)
⊢ (keys (β := fun (a : α) ↦ β a)
        (Quot.mk (⇑(isSetoid ((a : α) × β a)) : List ((a : α) × β a) → List ((a : α) × β a) → Prop) l)).Nodup ↔
    NodupKeys (β := fun (a : α) ↦ β a)
      (Quot.mk (⇑(isSetoid ((a : α) × β a)) : List ((a : α) × β a) → List ((a : α) × β a) → Prop) l)

Tactic:
rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
h : m.NodupKeys (β := fun (a : α) ↦ β a)
⊢ m.Nodup

Tactic:
h.nodup_keys.of_map _

Premises used: Multiset.Nodup.of_map, Multiset.NodupKeys.nodup_keys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
mk :
  ∀ (entries : List (Sigma β)) (nodupKeys : entries.NodupKeys (β := β)),
    (AList.mk (β := β) entries nodupKeys).toFinmap (β := β) = s₂.toFinmap (β := β) ↔
      (AList.mk (β := β) entries nodupKeys).entries (β := β) ~ s₂.entries (β := β)
⊢ s₁.toFinmap (β := β) = s₂.toFinmap (β := β) ↔ s₁.entries (β := β) ~ s₂.entries (β := β)

Tactic:
cases s₁
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
s₂ : AList β
entries : List (Sigma β)
nodupKeys : entries.NodupKeys (β := β)
mk :
  ∀ (entries_1 : List (Sigma β)) (nodupKeys_1 : entries_1.NodupKeys (β := β)),
    (AList.mk (β := β) entries nodupKeys).toFinmap (β := β) =
        (AList.mk (β := β) entries_1 nodupKeys_1).toFinmap (β := β) ↔
      (AList.mk (β := β) entries nodupKeys).entries (β := β) ~
        (AList.mk (β := β) entries_1 nodupKeys_1).entries (β := β)
⊢ (AList.mk (β := β) entries nodupKeys).toFinmap (β := β) = s₂.toFinmap (β := β) ↔
    (AList.mk (β := β) entries nodupKeys).entries (β := β) ~ s₂.entries (β := β)

Tactic:
cases s₂
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
entries : List (Sigma β)
nodupKeys : entries.NodupKeys (β := β)
entries_1 : List (Sigma β)
nodupKeys_1 : entries_1.NodupKeys (β := β)
⊢ (mk (β := β) entries nodupKeys).toFinmap (β := β) = (mk (β := β) entries_1 nodupKeys_1).toFinmap (β := β) ↔
    (mk (β := β) entries nodupKeys).entries (β := β) ~ (mk (β := β) entries_1 nodupKeys_1).entries (β := β)

Tactic:
simp [AList.toFinmap]

Premises used: AList.toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
s : AList β
⊢ s.toFinmap (β := β).entries (β := β) = (↑(s.entries (β := β)) : Multiset (Sigma β))

Tactic:
rfl

Premises used: Multiset.ofList, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
f : Finmap β
⊢ f.entries (β := β).Nodup

Tactic:
f.nodupKeys.nodup

Premises used: Finmap.nodupKeys, Multiset.NodupKeys.nodup
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
refine_1 :
  ∀ (l₁ l₂ : List (Sigma β)) (p : l₁ ≈ l₂)
    (h₁ :
      Part.Dom.{u_1} (α := γ)
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₁))
    (h₂ :
      Part.Dom.{u_1} (α := γ)
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₂)),
    Part.get
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₁)
        h₁ =
      Part.get
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₂)
        h₂
refine_2 :
  Part.Dom.{u_1} (α := γ)
    (Quotient.liftOn (s.entries (β := β))
      (fun (l : List (Sigma β)) ↦
        { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
      ⋯)
⊢ γ

Tactic:
refine
    (Quotient.liftOn s.entries
      (fun (l : List (Sigma β)) => (⟨_, fun nd => f ⟨l, nd⟩⟩ : Part γ))
      (fun l₁ l₂ p => Part.ext' (perm_nodupKeys p) ?_) : Part γ).get ?_

Premises used: Part.ext', Part.mk, AList.mk, List.perm_nodupKeys, Part.get, Finmap.entries, List.NodupKeys, Quotient.liftOn