awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
a : (powersetCard n.succ u).sup id ≤ u
a₁ : u ≤ (powersetCard n.succ u).sup id
⊢ (powersetCard n.succ u).sup id = u

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
a : ∀ (b : Finset α), b ⊆ u ∧ #b = n.succ → id b ≤ u
⊢ (powersetCard n.succ u).sup id ≤ u

Tactic:
simp_rw [Finset.sup_le_iff, mem_powersetCard]

Premises used: Finset.mem_powersetCard, Finset.sup_le_iff
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : Finset α
h : x ⊆ u
⊢ id x ≤ u

Tactic:
h

Premises used: Set.Mem, setOf
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : Finset α
h : x ⊆ u
⊢ id x ≤ u

Tactic:
exact h
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
a : ∀ ⦃x : α⦄, x ∈ u → x ∈ (powersetCard n.succ u).biUnion id
⊢ u ≤ (powersetCard n.succ u).sup id

Tactic:
rw [sup_eq_biUnion, le_iff_subset, subset_iff]

Premises used: Finset.sup_eq_biUnion, Finset.subset_iff, Finset.le_iff_subset
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
a : ∃ a ∈ powersetCard n.succ u, x ∈ a
⊢ x ∈ (powersetCard n.succ u).biUnion id

Tactic:
simp only [mem_biUnion, id]

Premises used: id, Finset.mem_biUnion
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ ∃ (t : Finset α), t ∈ powersetCard n (u.erase x)

Tactic:
powersetCard_nonempty.2
      (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase)

Premises used: Iff.mpr, Finset.pred_card_le_card_erase, Nat.le_sub_one_of_lt, Finset.Nonempty, Finset.powersetCard_nonempty, le_trans
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
a : ∀ (t : Finset α) (ht : t ∈ powersetCard n (u.erase x)), ∃ a ∈ powersetCard n.succ u, x ∈ a
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a

Tactic:
obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty.2
      (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase)

Premises used: Iff.mpr, Finset.pred_card_le_card_erase, Nat.le_sub_one_of_lt, Finset.powersetCard, Finset.powersetCard_nonempty, Finset.erase, le_trans
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a

Tactic:
⟨insert x t, ?_, mem_insert_self _ _⟩

Premises used: Finset.mem_insert_self, Insert.insert, And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
a : insert x t ∈ powersetCard n.succ u
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a

Tactic:
refine ⟨insert x t, ?_, mem_insert_self _ _⟩
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
a : insert x t ∈ powersetCard n.succ (u.erase x) ∪ image (insert x) (powersetCard n (u.erase x))
⊢ insert x t ∈ powersetCard n.succ u

Tactic:
rw [← insert_erase hx, powersetCard_succ_insert (notMem_erase _ _)]

Premises used: Finset.notMem_erase, Finset.insert_erase, Finset.powersetCard_succ_insert
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ (u.erase x) ∪ image (insert x) (powersetCard n (u.erase x))

Tactic:
mem_union_right _ (mem_image_of_mem _ ht)

Premises used: Finset.mem_union_right, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ (u.erase x) ∪ image (insert x) (powersetCard n (u.erase x))

Tactic:
exact mem_union_right _ (mem_image_of_mem _ ht)

Premises used: Finset.mem_union_right, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
simp : t ⊆ map f s ∧ #t = n ↔ ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
⊢ t ∈ powersetCard n (map f s) ↔
    t ∈
      map ((mapEmbedding f).toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Finset β) ↦ x1 ≤ x2))
        (powersetCard n s)

Tactic:
simp only [mem_powersetCard, mem_map, RelEmbedding.coe_toEmbedding, mapEmbedding_apply]

Premises used: RelEmbedding.coe_toEmbedding, Finset.mem_powersetCard, Finset.mapEmbedding_apply, Finset.mem_map
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
mp : t ⊆ map f s ∧ #t = n → ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
mpr : (∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t) → t ⊆ map f s ∧ #t = n
⊢ t ⊆ map f s ∧ #t = n ↔ ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
⊢ map f ({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
⊢ map f ({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = t

Tactic:
have : map f (filter (fun x => (f x ∈ t)) s) = t := by grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = t
⊢ ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t

Tactic:
⟨_, ?_, this⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = t
mp :
  {x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)} ⊆ s ∧
    #({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = n
⊢ ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t

Tactic:
refine ⟨_, ?_, this⟩
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = t
mp : {x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)} ⊆ s ∧ n = n
⊢ {x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)} ⊆ s ∧
    #({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = n

Tactic:
rw [← card_map f, this, h.2]

Premises used: Finset.card_map, And.right
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = t
⊢ {x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)} ⊆ s ∧ n = n

Tactic:
simp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
mp : ∀ (h : t ⊆ map f s ∧ #t = n), ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
mp₁ :
  ∀ (h : t ⊆ map f s ∧ #t = n) (this : map f ({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = t),
    ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
mp₂ :
  ∀ (h : t ⊆ map f s ∧ #t = n) (this : map f ({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = t),
    {x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)} ⊆ s ∧
      #({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = n
mp₃ mp₄ :
  ∀ (h : t ⊆ map f s ∧ #t = n) (this : map f ({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = t),
    {x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)} ⊆ s ∧ n = n
⊢ t ⊆ map f s ∧ #t = n → ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t

Tactic:
classical
      intro h
      have : map f (filter (fun x => (f x ∈ t)) s) = t := by grind
      refine ⟨_, ?_, this⟩
      rw [← card_map f, this, h.2]; simp

Premises used: Finset.card_map
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ map f a ⊆ map f s ∧ #(map f a) = #a

Tactic:
simp only [map_subset_map, has, card_map, and_self]

Premises used: and_self, Finset.card_map, Finset.map_subset_map
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α → β
s : Finset β
hf : InjOn f (f ⁻¹' (↑s : Set β))
x : α
⊢ x ∈ s.preimage f hf ↔ f x ∈ s

Tactic:
Set.Finite.mem_toFinset _

Premises used: Set.Mem, Set.Finite.mem_toFinset, setOf, Multiset.Mem, Set.preimage
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α → β
s : Finset β
hf : InjOn f (f ⁻¹' (↑s : Set β))
⊢ (↑(s.preimage f hf) : Set α) = f ⁻¹' (↑s : Set β)

Tactic:
Set.Finite.coe_toFinset _

Premises used: setOf, Set.Finite.coe_toFinset
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
⊢ InjOn f (f ⁻¹' (↑∅ : Set β))

Tactic:
simp [InjOn]

Premises used: Set.InjOn
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α → β
⊢ (↑(preimage ∅ f ⋯) : Set α) = (↑∅ : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α → β
inst : Fintype α
inst_1 : Fintype β
hf : InjOn f (f ⁻¹' (↑univ : Set β))
⊢ (↑(preimage univ f hf) : Set α) = (↑univ : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α → β
s t : Finset β
hs : InjOn f (f ⁻¹' (↑s : Set β))
ht : InjOn f (f ⁻¹' (↑t : Set β))
hd : Disjoint s t
⊢ Disjoint (s.preimage f hs) (t.preimage f ht)

Tactic:
grind [not_disjoint_iff, mem_preimage]

Premises used: Finset.mem_preimage, Finset.not_disjoint_iff
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s t : Finset β
hs : InjOn f (f ⁻¹' (↑s : Set β))
ht : InjOn f (f ⁻¹' (↑t : Set β))
⊢ (↑((s ∩ t).preimage f ⋯) : Set α) = (↑(s.preimage f hs ∩ t.preimage f ht) : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s t : Finset β
hst : InjOn f (f ⁻¹' (↑(s ∪ t) : Set β))
⊢ (↑((s ∪ t).preimage f hst) : Set α) = (↑(s.preimage f ⋯ ∪ t.preimage f ⋯) : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α → β
s : Finset β
hfc : InjOn f (f ⁻¹' (↑sᶜ : Set β))
hf : InjOn f (f ⁻¹' (↑s : Set β))
⊢ (↑(sᶜ.preimage f hfc) : Set α) = (↑(s.preimage f hf)ᶜ : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α → β
s : Finset β
hf : Injective f
⊢ sᶜ.preimage f ⋯ = (s.preimage f ⋯)ᶜ

Tactic:
preimage_compl' _ _ _

Premises used: Finset.preimage_compl'
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
⊢ (↑((map f s).preimage (⇑f : (a : α) → β) ⋯) : Set α) = (↑s : Set α)

Tactic:
simp only [coe_preimage, coe_map, Set.preimage_image_eq _ f.injective]

Premises used: Finset.coe_preimage, Function.Embedding.injective, Set.preimage_image_eq, Finset.coe_map
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α → β
h : Injective f
⊢ Monotone.{v, u} (β := Finset α) fun (s : Finset β) ↦ s.preimage f ⋯

Tactic:
fun _ _ H _ hx =>
  mem_preimage.2 (H <| mem_preimage.1 hx)

Premises used: Iff.mpr, Set.Mem, Monotone, setOf, Finset.mem_preimage, Iff.mp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
hf : InjOn f (f ⁻¹' (↑t : Set β))
⊢ (∀ x ∈ s, f x ∈ t) ↔ s ⊆ t.preimage f hf

Tactic:
simp only [subset_iff, mem_preimage]

Premises used: Finset.mem_preimage, Finset.subset_iff
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
rw : image (⇑f : (a : α) → β) s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
rw₁ : s ⊆ t.preimage (⇑f : (a : α) → β) ⋯ ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
rw₂ : InjOn.{u, v} (α := α) (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' (↑t : Set β))
rw₃ : s ⊆ t.preimage (⇑f : (a : α) → β) ⋯ ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
rw₄ : InjOn.{u, v} (α := α) (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' (↑t : Set β))
⊢ map f s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯

Tactic:
rw [map_eq_image, image_subset_iff_subset_preimage]

Premises used: Finset.image_subset_iff_subset_preimage, Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
classical : image (⇑f : (a : α) → β) s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
classical₁ : s ⊆ t.preimage (⇑f : (a : α) → β) ⋯ ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
classical₂ : InjOn.{u, v} (α := α) (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' (↑t : Set β))
classical₃ : s ⊆ t.preimage (⇑f : (a : α) → β) ⋯ ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
classical₄ : InjOn.{u, v} (α := α) (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' (↑t : Set β))
⊢ map f s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯

Tactic:
classical rw [map_eq_image, image_subset_iff_subset_preimage]

Premises used: Finset.image_subset_iff_subset_preimage, Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' (↑s : Set β))
inst : DecidablePred fun (x : β) ↦ x ∈ Set.range f
⊢ MapsTo f (↑(s.preimage f hf) : Set α) (↑({x ∈ s | x ∈ Set.range f}) : Set β)

Tactic:
simp [Set.MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' (↑s : Set β))
inst : DecidablePred fun (x : β) ↦ x ∈ Set.range f
⊢ InjOn f (↑(s.preimage f hf) : Set α)

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' (↑s : Set β))
inst : DecidablePred fun (x : β) ↦ x ∈ Set.range f
b : β
hb : b ∈ (↑({x ∈ s | x ∈ Set.range f}) : Set β)
⊢ b ∈ f '' (↑(s.preimage f hf) : Set α)

Tactic:
aesop
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset β
inst_1 : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' (↑s : Set β))
simp : Eq.{v + 1} (α := Set β) {x : β | x ∈ (↑s : Set β) ∧ x ∈ Set.range f} {x : β | x ∈ s ∧ x ∈ Set.range f}
⊢ (↑(image f (s.preimage f hf)) : Set β) = (↑({x ∈ s | x ∈ Set.range f}) : Set β)

Tactic:
simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range,
      ← Set.sep_mem_eq]

Premises used: Finset.coe_filter, Finset.coe_image, Set.sep_mem_eq, Set.image_preimage_eq_inter_range, Finset.coe_preimage
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset β
inst_1 : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' (↑s : Set β))
⊢ Eq.{v + 1} (α := Set β) {x : β | x ∈ (↑s : Set β) ∧ x ∈ Set.range f} {x : β | x ∈ s ∧ x ∈ Set.range f}

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
g : β → α
s : Finset α
hgf : LeftInvOn g f (↑s : Set α)
ginj : InjOn g (g ⁻¹' (↑s : Set α))
simp : f '' (↑s : Set α) = g ⁻¹' (↑s : Set α)
⊢ image f s = s.preimage g ginj

Tactic:
simp only [SetLike.ext'_iff, coe_preimage, coe_image]

Premises used: Finset.coe_image, Finset.coe_preimage, SetLike.ext'_iff
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
g : β → α
s : Finset α
hgf : LeftInvOn g f (↑s : Set α)
ginj : InjOn g (g ⁻¹' (↑s : Set α))
rw rw₁ : g ⁻¹' (↑s : Set α) = g ⁻¹' (↑s : Set α)
⊢ f '' (↑s : Set α) = g ⁻¹' (↑s : Set α)

Tactic:
rw [Set.image_eq_preimage_of_leftInvOn_injOn hgf ginj]

Premises used: Set.image_eq_preimage_of_leftInvOn_injOn
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset β
hf : BijOn f (f ⁻¹' (↑s : Set β)) (↑s : Set β)
⊢ (↑(image f (s.preimage f ⋯)) : Set β) = (↑s : Set β)

Tactic:
simpa using hf.image_eq

Premises used: Set.BijOn.image_eq
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset β
hf : Bijective f
⊢ image f (s.preimage f ⋯) = s

Tactic:
image_preimage_of_bij f s hf.bijOn_preimage

Premises used: Function.Bijective.bijOn_preimage, Finset.image_preimage_of_bij
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' (↑s : Set β))
rw : f ⁻¹' (↑s : Set β) ⊆ (↑t : Set α)
⊢ s.preimage f hf ⊆ t

Tactic:
rw [← coe_subset, coe_preimage]

Premises used: Finset.coe_preimage, Finset.coe_subset
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' (↑s : Set β))
⊢ f ⁻¹' (↑s : Set β) ⊆ (↑t : Set α)

Tactic:
Set.preimage_subset (mod_cast hs) hf

Premises used: SetLike.coe_subset_coe._simp_1, congrArg, cast, Finset.coe_image._simp_1, HasSubset.Subset, SetLike.coe, Eq.symm, Eq.trans, Set.preimage_subset
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' (↑s : Set β))
⊢ f ⁻¹' (↑s : Set β) ⊆ (↑t : Set α)

Tactic:
exact Set.preimage_subset (mod_cast hs) hf

Premises used: Set.preimage_subset
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
hs : s ⊆ map f t
⊢ s.preimage (⇑f : (a : α) → β) ⋯ ⊆ t

Tactic:
fun _ h => (mem_map' f).1 (hs (mem_preimage.1 h))

Premises used: Finset.mem_preimage, Iff.mp, Finset.mem_map'
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
simp_rw : s ⊆ image (⇑f : (a : α) → β) t ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
simp_rw₁ : (∃ s' ⊆ t, image (⇑f : (a : α) → β) s' = s) ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u

Tactic:
simp_rw [map_eq_image, subset_image_iff, eq_comm]

Premises used: eq_comm, Finset.map_eq_image, Finset.subset_image_iff
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
simp_rw : s ⊆ image (⇑f : (a : α) → β) t ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
simp_rw₁ : (∃ s' ⊆ t, image (⇑f : (a : α) → β) s' = s) ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u

Tactic:
classical
  simp_rw [map_eq_image, subset_image_iff, eq_comm]

Premises used: eq_comm, Finset.map_eq_image, Finset.subset_image_iff
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
hf : Bijective f
rw : image f s = t ↔ image f s = image f (t.preimage f ⋯)
rw₁ rw₂ : image f s = t ↔ image f s = t
⊢ image f s = t ↔ s = t.preimage f ⋯

Tactic:
rw [← image_inj hf.injective, t.image_preimage_of_bijective hf]

Premises used: Finset.image_inj, Finset.image_preimage_of_bijective, Function.Bijective.injective
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' (↑s : Set β)) (↑s : Set β)
⊢ ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x

Tactic:
have hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x := hf.invOn_invFunOn.2
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' (↑s : Set β)) (↑s : Set β)
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x
rw : (s.preimage f ⋯).sup f = (image (invFunOn f (f ⁻¹' (↑s : Set β))) s).sup f
⊢ (s.preimage f ⋯).sup f = s.sup id

Tactic:
rw [← sup_congr (Eq.refl s) hfinvs, ← sup_image]

Premises used: Finset.sup_image, Finset.sup_congr, Eq.refl
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' (↑s : Set β)) (↑s : Set β)
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x
e_s : s.preimage f ⋯ = image (invFunOn f (f ⁻¹' (↑s : Set β))) s
⊢ (s.preimage f ⋯).sup f = (image (invFunOn f (f ⁻¹' (↑s : Set β))) s).sup f

Tactic:
congr
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' (↑s : Set β)) (↑s : Set β)
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x
⊢ s.preimage f ⋯ = image (invFunOn f (f ⁻¹' (↑s : Set β))) s

Tactic:
(image_eq_preimage_of_leftInvOn_injOn hf.invOn_invFunOn.2 hf.2.1).symm

Premises used: Finset.image_eq_preimage_of_leftInvOn_injOn, And.right, And.left, Set.BijOn.invOn_invFunOn, Eq.symm
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' (↑s : Set β)) (↑s : Set β)
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x
⊢ s.preimage f ⋯ = image (invFunOn f (f ⁻¹' (↑s : Set β))) s

Tactic:
exact (image_eq_preimage_of_leftInvOn_injOn hf.invOn_invFunOn.2 hf.2.1).symm

Premises used: Finset.image_eq_preimage_of_leftInvOn_injOn, And.right, And.left, Set.BijOn.invOn_invFunOn, Eq.symm
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' (↑s : Set β)) (↑s : Set β)
have have₁ have₂ :
  ∀ (hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x), (s.preimage f ⋯).sup f = s.sup id
have₃ :
  ∀ (hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x),
    (s.preimage f ⋯).sup f = (image (invFunOn f (f ⁻¹' (↑s : Set β))) s).sup f
e_s :
  ∀ (hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x),
    s.preimage f ⋯ = image (invFunOn f (f ⁻¹' (↑s : Set β))) s
⊢ (s.preimage f ⋯).sup f = s.sup id

Tactic:
classical
  have hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x := hf.invOn_invFunOn.2
  rw [← sup_congr (Eq.refl s) hfinvs, ← sup_image]
  congr
  exact (image_eq_preimage_of_leftInvOn_injOn hf.invOn_invFunOn.2 hf.2.1).symm

Premises used: Finset.sup_image
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
inst : Lattice α
inst_1 : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot (p := P) Pbot
a : (↑(sup (t.preimage (Subtype.val (p := P)) ⋯) id) : α) = (↑(Subtype.mk (p := P) (t.sup id) ⋯) : α)
⊢ sup (t.preimage (Subtype.val (p := P)) ⋯) id = Subtype.mk (p := P) (t.sup id) ⋯

Tactic:
ext
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
inst : Lattice α
inst_1 : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot (p := P) Pbot
a : (sup (t.preimage (Subtype.val (p := P)) ⋯) fun (x : Subtype P) ↦ (↑x : α)) = t.sup id
⊢ (↑(sup (t.preimage (Subtype.val (p := P)) ⋯) id) : α) = (↑(Subtype.mk (p := P) (t.sup id) ⋯) : α)

Tactic:
simp only [sup_coe, id_eq]

Premises used: Finset.sup_coe, id_eq