awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = ∅ → #s < n
have contrapose! : n ≤ #s → (powersetCard n s).Nonempty
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = {x ∈ s.powerset | #x = n}
have h : ∀ (a : Finset α), a ∈ powersetCard n s ↔ a ∈ {x ∈ s.powerset | #x = n}
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
have rw : powersetCard n.succ s ∪ {x ∈ image (insert x) s.powerset | #x = n.succ} =
  powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
Tactic: rw [powersetCard_eq_filter, powerset_insert, filter_union, ← powersetCard_eq_filter]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
⊢ powersetCard (#s) s = {s}
have h : ∀ (a : Finset α), a ∈ powersetCard (#s) s ↔ Membership.mem (γ := Finset (Finset α)) {s} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s a : Finset α
⊢ a ∈ powersetCard (#s) s ↔ Membership.mem (γ := Finset (Finset α)) {s} a
have h : a ⊆ s ∧ #a = #s ↔ a = s
Tactic: rw [mem_powersetCard, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s a : Finset α
⊢ a ⊆ s ∧ #a = #s ↔ a = s
have h : a ⊆ s ∧ #a = #s → a = s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s a : Finset α
h : a ⊆ s ∧ #a = #s → a = s
⊢ a ⊆ s ∧ #a = #s ↔ a = s
have h₁ : a = s → a ⊆ s ∧ #a = #s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
⊢ s.powerset = (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯
have refine_1 : ∀ (a : Finset α) (ha : a ∈ s.powerset), a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) sorry
Tactic: refine ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
refine_1 : ∀ (a : Finset α) (ha : a ∈ s.powerset), a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯
⊢ s.powerset = (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯
have refine_2 : ∀ (a : Finset α) (ha : a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) sorry), a ∈ s.powerset
Tactic: refine ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯
have refine_1 : ∃ a_1 ∈ range (#s + 1), a ∈ powersetCard a_1 s
Tactic: rw [mem_disjiUnion]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s a : Finset α
ha : a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯
⊢ a ∈ s.powerset
have refine_2 : ∀ (i : ℕ) (_hi : i ∈ range (#s + 1)) (ha : a ∈ powersetCard i s), a ∈ s.powerset
Tactic: rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ (powersetCard n.succ u).sup id = u
have a : (powersetCard n.succ u).sup id ≤ u
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
a : (powersetCard n.succ u).sup id ≤ u
⊢ (powersetCard n.succ u).sup id = u
have a₁ : u ≤ (powersetCard n.succ u).sup id
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ (powersetCard n.succ u).sup id ≤ u
have a : ∀ (b : Finset α), b ⊆ u ∧ #b = n.succ → id b ≤ u
Tactic: simp_rw [Finset.sup_le_iff, mem_powersetCard]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ u ≤ (powersetCard n.succ u).sup id
have a : ∀ ⦃x : α⦄, x ∈ u → x ∈ (powersetCard n.succ u).biUnion id
Tactic: rw [sup_eq_biUnion, le_iff_subset, subset_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ x ∈ (powersetCard n.succ u).biUnion id
have a : ∃ a ∈ powersetCard n.succ u, x ∈ a
Tactic: simp only [mem_biUnion, id]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a
have a : ∀ (t : Finset α) (ht : t ∈ powersetCard n (u.erase x)), ∃ 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)
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
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
have a : insert x t ∈ powersetCard n.succ u
Tactic: refine ⟨insert x t, ?_, mem_insert_self _ _⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
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
have a : insert x t ∈ powersetCard n.succ (u.erase x) ∪ image (insert x) (powersetCard n (u.erase x))
Tactic: rw [← insert_erase hx, powersetCard_succ_insert (notMem_erase _ _)]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ 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)
have simp : t ⊆ map f s ∧ #t = n ↔ ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
Tactic: simp only [mem_powersetCard, mem_map, RelEmbedding.coe_toEmbedding, mapEmbedding_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n ↔ ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
have mp : t ⊆ map f s ∧ #t = n → ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
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
⊢ t ⊆ map f s ∧ #t = n ↔ ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
have mpr : (∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t) → t ⊆ map f s ∧ #t = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
⊢ ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
have this : 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
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
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
have mp : {x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)} ⊆ s ∧
  #({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = n
Tactic: refine ⟨_, ?_, this⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
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 ∧
    #({x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)}) = n
have mp : {x ∈ s | Membership.mem (α := β) t ((f : (a : α) → β) x : β)} ⊆ s ∧ n = n
Tactic: rw [← card_map f, this, h.2]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
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
⊢ t ⊆ map f s ∧ #t = n → ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
have 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
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
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
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
⊢ t ⊆ map f s ∧ #t = n → ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
have 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
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
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
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
⊢ t ⊆ map f s ∧ #t = n → ∃ (a : Finset α), (a ⊆ s ∧ #a = n) ∧ map f a = t
have 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
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
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
have rw : image (⇑f : (a : α) → β) s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) sorry
Tactic: rw [map_eq_image, image_subset_iff_subset_preimage]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
rw : image (⇑f : (a : α) → β) s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
⊢ map f s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
have rw₁ : s ⊆ t.preimage (⇑f : (a : α) → β) sorry ↔ s ⊆ t.preimage (⇑f : (a : α) → β) sorry
Tactic: rw [map_eq_image, image_subset_iff_subset_preimage]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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 : α) → β) ⋯
⊢ map f s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
have rw₂ : InjOn.{u, v} (α := α) (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' (↑t : Set β))
Tactic: rw [map_eq_image, image_subset_iff_subset_preimage]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
have classical : image (⇑f : (a : α) → β) s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) sorry
Tactic: classical rw [map_eq_image, image_subset_iff_subset_preimage]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
classical : image (⇑f : (a : α) → β) s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
⊢ map f s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
have classical₁ : s ⊆ t.preimage (⇑f : (a : α) → β) sorry ↔ s ⊆ t.preimage (⇑f : (a : α) → β) sorry
Tactic: classical rw [map_eq_image, image_subset_iff_subset_preimage]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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 : α) → β) ⋯
⊢ map f s ⊆ t ↔ s ⊆ t.preimage (⇑f : (a : α) → β) ⋯
have classical₂ : InjOn.{u, v} (α := α) (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' (↑t : Set β))
Tactic: classical rw [map_eq_image, image_subset_iff_subset_preimage]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset β
inst_1 : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' (↑s : Set β))
⊢ (↑(image f (s.preimage f hf)) : Set β) = (↑({x ∈ s | x ∈ Set.range f}) : Set β)
have simp : Eq.{v + 1} (α := Set β) {x : β | x ∈ (↑s : Set β) ∧ x ∈ Set.range f} {x : β | x ∈ s ∧ x ∈ Set.range f}
Tactic: simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range,
      ← Set.sep_mem_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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 α))
⊢ image f s = s.preimage g ginj
have simp : f '' (↑s : Set α) = g ⁻¹' (↑s : Set α)
Tactic: simp only [SetLike.ext'_iff, coe_preimage, coe_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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 α))
⊢ f '' (↑s : Set α) = g ⁻¹' (↑s : Set α)
have rw : g ⁻¹' (↑s : Set α) = g ⁻¹' (↑s : Set α)
Tactic: rw [Set.image_eq_preimage_of_leftInvOn_injOn hgf ginj]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' (↑s : Set β))
⊢ s.preimage f hf ⊆ t
have rw : f ⁻¹' (↑s : Set β) ⊆ (↑t : Set α)
Tactic: rw [← coe_subset, coe_preimage]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u
have simp_rw : s ⊆ image (⇑f : (a : α) → β) t ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
Tactic: simp_rw [map_eq_image, subset_image_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
simp_rw : s ⊆ image (⇑f : (a : α) → β) t ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u
have simp_rw₁ : (∃ s' ⊆ t, image (⇑f : (a : α) → β) s' = s) ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
Tactic: simp_rw [map_eq_image, subset_image_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u
have simp_rw : s ⊆ image (⇑f : (a : α) → β) t ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
Tactic: classical
  simp_rw [map_eq_image, subset_image_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
simp_rw : s ⊆ image (⇑f : (a : α) → β) t ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u
have simp_rw₁ : (∃ s' ⊆ t, image (⇑f : (a : α) → β) s' = s) ↔ ∃ u ⊆ t, s = image (⇑f : (a : α) → β) u
Tactic: classical
  simp_rw [map_eq_image, subset_image_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
hf : Bijective f
⊢ image f s = t ↔ s = t.preimage f ⋯
have rw : image f s = t ↔ image f s = image f (t.preimage f sorry)
Tactic: rw [← image_inj hf.injective, t.image_preimage_of_bijective hf]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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 ⋯)
⊢ image f s = t ↔ s = t.preimage f ⋯
have rw₁ : image f s = t ↔ image f s = t
Tactic: rw [← image_inj hf.injective, t.image_preimage_of_bijective hf]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (hypothesis)
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 β)
⊢ (s.preimage f ⋯).sup f = s.sup id
have hfinvs : ∀ 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
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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 ⋯).sup f = s.sup id
have rw : (s.preimage f sorry).sup f = (image (invFunOn f (f ⁻¹' (↑s : Set β))) s).sup f
Tactic: rw [← sup_congr (Eq.refl s) hfinvs, ← sup_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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 ⋯).sup f = (image (invFunOn f (f ⁻¹' (↑s : Set β))) s).sup f
have e_s : s.preimage f sorry = image (invFunOn f (f ⁻¹' (↑s : Set β))) s
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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 β)
⊢ (s.preimage f ⋯).sup f = s.sup id
have have : ∀ (hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x), (s.preimage f sorry).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
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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
⊢ (s.preimage f ⋯).sup f = s.sup id
have have₃ : ∀ (hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x),
  (s.preimage f sorry).sup f = (image (invFunOn f (f ⁻¹' (↑s : Set β))) s).sup f
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
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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
⊢ (s.preimage f ⋯).sup f = s.sup id
have e_s : ∀ (hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' (↑s : Set β))) x = id x),
  s.preimage f sorry = image (invFunOn f (f ⁻¹' (↑s : Set β))) s
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
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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
⊢ sup (t.preimage (Subtype.val (p := P)) ⋯) id = Subtype.mk (p := P) (t.sup id) ⋯
have a : (↑(sup (t.preimage (Subtype.val (p := P)) sorry) id) : α) = (↑(Subtype.mk (p := P) (t.sup id) sorry) : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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
⊢ (↑(sup (t.preimage (Subtype.val (p := P)) ⋯) id) : α) = (↑(Subtype.mk (p := P) (t.sup id) ⋯) : α)
have a : (sup (t.preimage (Subtype.val (p := P)) sorry) fun (x : Subtype P) ↦ (↑x : α)) = t.sup id
Tactic: simp only [sup_coe, id_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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
⊢ (sup (t.preimage (Subtype.val (p := P)) ⋯) fun (x : Subtype P) ↦ (↑x : α)) = t.sup id
have a : BijOn (α := Subtype P) (Subtype.val (p := P)) (Subtype.val (p := P) ⁻¹' (↑t : Set α)) (↑t : Set α)
Tactic: apply sup_preimage_self
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
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
⊢ BijOn (α := Subtype P) (Subtype.val (p := P)) (Subtype.val (p := P) ⁻¹' (↑t : Set α)) (↑t : Set α)
have a : SurjOn (α := Subtype P) (Subtype.val (p := P)) (Subtype.val (p := P) ⁻¹' (↑t : Set α)) (↑t : Set α)
Tactic: refine ⟨mapsTo_preimage _ _, injOn_of_injective Subtype.val_injective, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : α → Type u_1
inst : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
⊢ (t.sigma (α := fun (a : α) ↦ β a) fun (a : α) ↦ s.preimage (Sigma.mk (β := fun (a : α) ↦ β a) a) ⋯) =
    {a ∈ s | a.fst (β := fun (a : α) ↦ β a) ∈ t}
have h : ∀ (x : (i : α) × β i),
  Membership.mem (γ := Finset ((i : α) × β i))
      (t.sigma (α := fun (a : α) ↦ β a) fun (a : α) ↦ s.preimage (Sigma.mk (β := fun (a : α) ↦ β a) a) sorry) x ↔
    x ∈ {a ∈ s | a.fst (β := fun (a : α) ↦ β a) ∈ t}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : α → Type u_1
inst : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
ht : image (Sigma.fst (β := fun (a : α) ↦ β a)) s ⊆ t
⊢ (t.sigma (α := fun (a : α) ↦ β a) fun (a : α) ↦ s.preimage (Sigma.mk (β := fun (a : α) ↦ β a) a) ⋯) = s
have rw : {a ∈ s | a.fst (β := fun (a : α) ↦ β a) ∈ t} = s
Tactic: rw [sigma_preimage_mk, filter_true_of_mem <| image_subset_iff.1 ht]