awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : {a ∈ s | a.fst (β := fun (a : α) ↦ β a) ∈ t} = s
⊢ (t.sigma (α := fun (a : α) ↦ β a) fun (a : α) ↦ s.preimage (Sigma.mk (β := fun (a : α) ↦ β a) a) ⋯) = s
have rw₁ : s = s
Tactic: rw [sigma_preimage_mk, filter_true_of_mem <| image_subset_iff.1 ht]
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inl ⋯ = s.toLeft
have h : ∀ (x : α), x ∈ s.preimage Sum.inl sorry ↔ x ∈ s.toLeft
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inr ⋯ = s.toRight
have h : ∀ (x : β), x ∈ s.preimage Sum.inr sorry ↔ x ∈ s.toRight
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Preimage (goal)
Goal:
α : Type u
β : Type v
π : β → Type u_1
s : Finset β
e : α ≃ β
⊢ Eq (α := ((a : α) → π ((e : (a : α) → β) a)) → (i : ↥s) → π (↑i : β))
    (s.restrict (π := π) ∘ (⇑(Equiv.piCongrLeft π e) : (a : (a : α) → π ((e : (a : α) → β) a)) → (b : β) → π b))
    ((⇑(Equiv.piCongrLeft.{u_1 + 1, u + 1, v + 1} (fun (b : ↥s) ↦ π (↑b : β)) (e.restrictPreimageFinset s) :
            ((a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) →
                π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) → ↥s) a) : β)) ≃
              ((b : ↥s) → π (↑b : β))) :
        (a :
            (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) →
              π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) → ↥s) a) : β)) →
          (b : ↥s) → π (↑b : β)) ∘
      (s.preimage (⇑e : (a : α) → β) ⋯).restrict (π := fun (i : α) ↦ π ((e : (a : α) → β) i)))
have h : ∀ (x : (a : α) → π ((e : (a : α) → β) a)) (b : ↥s),
  Eq.{u_1 + 1} (α := π (↑b : β))
    ((s.restrict (π := π) ∘ (⇑(Equiv.piCongrLeft π e) : (a : (a : α) → π ((e : (a : α) → β) a)) → (b : β) → π b)) x b :
      π (↑b : β))
    (((⇑(Equiv.piCongrLeft.{u_1 + 1, u + 1, v + 1} (fun (b : ↥s) ↦ π (↑b : β)) (e.restrictPreimageFinset s) :
                ((a : ↥(s.preimage (⇑e : (a : α) → β) sorry)) →
                    π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) sorry)) → ↥s) a) : β)) ≃
                  ((b : ↥s) → π (↑b : β))) :
            (a :
                (a : ↥(s.preimage (⇑e : (a : α) → β) sorry)) →
                  π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) sorry)) → ↥s) a) : β)) →
              (b : ↥s) → π (↑b : β)) ∘
          (s.preimage (⇑e : (a : α) → β) sorry).restrict (π := fun (i : α) ↦ π ((e : (a : α) → β) i)))
        x b :
      π (↑b : β))
Tactic: ext x b
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst : DecidableEq α
ht : t.Nonempty
⊢ image Prod.fst (s ×ˢ t) = s
have h : ∀ (i : α), i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst : DecidableEq β
ht : s.Nonempty
⊢ image Prod.snd (s ×ˢ t) = t
have h : ∀ (i : β), i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (↑(map { toFun := Prod.swap, inj' := ⋯ : β × α ↪ α × β } (t ×ˢ s)) : Set (α × β)) = (↑(s ×ˢ t) : Set (α × β))
have push_cast : (⇑{ toFun := Prod.swap, inj' := sorry } : (a : β × α) → α × β) '' (↑t : Set β) ×ˢ (↑s : Set α) =
  (↑s : Set α) ×ˢ (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ (↑(image Prod.swap (t ×ˢ s)) : Set (α × β)) = (↑(s ×ˢ t) : Set (α × β))
have push_cast : Prod.swap '' (↑t : Set β) ×ˢ (↑s : Set α) = (↑s : Set α) ×ˢ (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)
have simp_rw : 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)
Tactic: simp_rw [← card_pos, ← one_lt_card_iff_nontrivial, card_product]
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
have rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Tactic: rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
have rw₁ : Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Tactic: rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
have h : {x ∈ s ×ˢ t | p x.1 = q x.2} = {x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2}
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
have h : Disjoint (α := α × β → Prop) (fun (x : α × β) ↦ p x.1 ∧ q x.2) fun (x : α × β) ↦ ¬p x.1 ∧ ¬q x.2
Tactic: apply Finset.disjoint_filter_filter'
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
have rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
Tactic: classical
  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    grind
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
have rw₁ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
Tactic: classical
  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    grind
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
rw₁ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
have rw₂ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
Tactic: classical
  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    grind
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
rw₁ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
rw₂ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
have rw₃ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Tactic: classical
  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    grind
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
rw₁ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
rw₂ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
rw₃ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
have rw₄ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Tactic: classical
  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    grind
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
rw₁ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
rw₂ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
rw₃ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
rw₄ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
have rw₅ : Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Tactic: classical
  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    grind
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
have contrapose! : (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
t : Finset β
a : α
⊢ SProd.sprod (α := Finset α) {a} t = map { toFun := Prod.mk a, inj' := ⋯ } t
have h : ∀ (x : α) (y : β),
  (x, y) ∈ SProd.sprod (α := Finset α) {a} t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := sorry : β ↪ α × β } t
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
b : β
⊢ SProd.sprod (β := Finset β) s {b} = map { toFun := fun (i : α) ↦ (i, b), inj' := ⋯ } s
have h : ∀ (x : α) (y : β),
  (x, y) ∈ SProd.sprod (β := Finset β) s {b} ↔ (x, y) ∈ map { toFun := fun (i : α) ↦ (i, b), inj' := sorry : α ↪ α × β } s
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
⊢ Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'
have simp_rw : Disjoint (↑(s ×ˢ t) : Set (α × β)) (↑(s' ×ˢ t') : Set (α × β)) ↔
  Disjoint (↑s : Set α) (↑s' : Set α) ∨ Disjoint (↑t : Set β) (↑t' : Set β)
Tactic: simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
simp_rw :
  Disjoint (↑(s ×ˢ t) : Set (α × β)) (↑(s' ×ˢ t') : Set (α × β)) ↔
    Disjoint (↑s : Set α) (↑s' : Set α) ∨ Disjoint (↑t : Set β) (↑t' : Set β)
⊢ Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'
have simp_rw₁ : Disjoint ((↑s : Set α) ×ˢ (↑t : Set β)) ((↑s' : Set α) ×ˢ (↑t' : Set β)) ↔
  Disjoint (↑s : Set α) (↑s' : Set α) ∨ Disjoint (↑t : Set β) (↑t' : Set β)
Tactic: simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ Nodup (Quotient.map List.offDiag ⋯ s.val)
have mk : ∀ (val : Multiset α) (s : List α) (hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)),
  Nodup
    (Quotient.map List.offDiag sorry
      { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.val)
Tactic: rcases s with ⟨⟨s⟩, hs⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
s : Finset α
x : α × α
⊢ x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2
have mk : ∀ (val : Multiset α) (s : List α) (hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)),
  x ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.offDiag ↔
    x.1 ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α } ∧
      x.2 ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α } ∧ x.1 ≠ x.2
Tactic: rcases s with ⟨⟨s⟩, hs⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ s.diag = {a ∈ s ×ˢ s | a.1 = a.2}
have h : ∀ (a : α × α), a ∈ s.diag ↔ a ∈ {a ∈ s ×ˢ s | a.1 = a.2}
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
s : Finset α
⊢ #s.offDiag = #s * #s - #s
have rw : #s.offDiag = HPow.hPow (β := ℕ) (#s) 2 - #s
Tactic: rw [← sq]
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
s : Finset α
⊢ #s.offDiag = HPow.hPow (β := ℕ) (#s) 2 - #s
have mk : ∀ (val : Multiset α) (s : List α) (hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)),
  #{ val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.offDiag =
    HPow.hPow (β := ℕ) (#{ val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }) 2 -
      #{ val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }
Tactic: rcases s with ⟨⟨s⟩, hs⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ (↑(s ∩ t).offDiag : Set (α × α)) = (↑(s.offDiag ∩ t.offDiag) : Set (α × α))
have push_cast : ((↑s : Set α) ∩ (↑t : Set α)).offDiag = (↑s : Set α).offDiag ∩ (↑t : Set α).offDiag
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : Disjoint s t
⊢ (↑(s ∪ t).offDiag : Set (α × α)) = (↑(s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s) : Set (α × α))
have push_cast : ((↑s : Set α) ∪ (↑t : Set α)).offDiag =
  (↑s : Set α).offDiag ∪ (↑t : Set α).offDiag ∪ (↑s : Set α) ×ˢ (↑t : Set α) ∪ (↑t : Set α) ×ˢ (↑s : Set α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.Prod (goal)
Goal:
ι : Type u_4
inst : PartialOrder ι
inst_1 : DecidableLE ι
inst_2 : DecidableLT ι
s : Finset ι
⊢ {i ∈ s.offDiag | i.1 < i.2} = {i ∈ s.offDiag | i.1 ≤ i.2}
have h : ∀ (a : ι × ι), a ∈ {i ∈ s.offDiag | i.1 < i.2} ↔ a ∈ {i ∈ s.offDiag | i.1 ≤ i.2}
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Range (goal)
Goal:
n : ℕ
hn : 1 < n
⊢ (range n).Nontrivial
have rw : (Set.Iio n).Nontrivial
Tactic: rw [Finset.Nontrivial, Finset.coe_range]
-- Lean 4 proof step from Mathlib.Data.Finset.SDiff (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
⊢ insert a s \ insert b s = {a}
have h : ∀ (a_1 : α), a_1 ∈ insert a s \ insert b s ↔ Membership.mem (γ := Finset α) {a} a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
⊢ (s • t).IsPWO
have rw : IsPWO.{u_2} (α := P) ((fun (x : G × P) ↦ x.1 • x.2) '' s ×ˢ t)
Tactic: rw [← @image_smul_prod]
-- Lean 4 proof step from Mathlib.Data.Finset.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ min (s := s • t) ⋯ ⋯ = hs.min (s := s) hsn • ht.min (s := t) htn
have refine : hs.min (s := s) hsn • ht.min (s := t) htn ≤ min (s := s • t) sorry sorry
Tactic: refine le_antisymm (IsWF.min_le _ _ (mem_smul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_
-- Lean 4 proof step from Mathlib.Data.Finset.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ hs.min (s := s) hsn • ht.min (s := t) htn ≤ min (s := s • t) ⋯ ⋯
have rw : ∀ b ∈ s • t, hs.min (s := s) hsn • ht.min (s := t) htn ≤ b
Tactic: rw [IsWF.le_min_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s : Set G
t : Set P
a : P
h : (s.smulAntidiagonal t a).Finite
x : G × P
⊢ x ∈ SMulAntidiagonal (s := s) (t := t) a h ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
have simp : x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
Tactic: simp only [SMulAntidiagonal, Set.Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Finset.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ SMulAntidiagonal (s := s) (t := t) (hs.min (s := s) hns • ht.min (s := t) hnt) ⋯ =
    {(hs.min (s := s) hns, ht.min (s := t) hnt)}
have h : ∀ (a : G) (b : P),
  (a, b) ∈ SMulAntidiagonal (s := s) (t := t) (hs.min (s := s) hns • ht.min (s := t) hnt) sorry ↔
    Membership.mem (γ := Finset (G × P)) {(hs.min (s := s) hns, ht.min (s := t) hnt)} (a, b)
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Data.Finset.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ (a, b) ∈ SMulAntidiagonal (s := s) (t := t) (hs.min (s := s) hns • ht.min (s := t) hnt) ⋯ ↔
    Membership.mem (γ := Finset (G × P)) {(hs.min (s := s) hns, ht.min (s := t) hnt)} (a, b)
have h : a ∈ s ∧ b ∈ t ∧ a • b = hs.min (s := s) hns • ht.min (s := t) hnt ↔ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
Tactic: simp only [mem_smulAntidiagonal, mem_singleton, Prod.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ a ∈ s ∧ b ∈ t ∧ a • b = hs.min (s := s) hns • ht.min (s := t) hnt ↔ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
have h : a ∈ s ∧ b ∈ t ∧ a • b = hs.min (s := s) hns • ht.min (s := t) hnt → a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
h :
  a ∈ s ∧ b ∈ t ∧ a • b = hs.min (s := s) hns • ht.min (s := t) hnt → a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
⊢ a ∈ s ∧ b ∈ t ∧ a • b = hs.min (s := s) hns • ht.min (s := t) hnt ↔ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
have h₁ : a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt → a ∈ s ∧ b ∈ t ∧ a • b = hs.min (s := s) hns • ht.min (s := t) hnt
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.SMulAntidiagonal (goal)
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
has : a ∈ s
hat : b ∈ t
hst : a • b = hs.min (s := s) hns • ht.min (s := t) hnt
⊢ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
have h : ∀ (has : hs.min (s := s) hns ∈ s) (hst : hs.min (s := s) hns • b = hs.min (s := s) hns • ht.min (s := t) hnt),
  hs.min (s := s) hns = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
Tactic: obtain rfl :=
      (hs.min_le hns has).eq_of_not_lt fun hlt =>
        (SMul.smul_lt_smul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst
Cleared hypotheses: a, has, hst
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ s.sigma (α := α) t = ∅ ↔ ∀ i ∈ s, t i = ∅
have contrapose! : (s.sigma (α := α) t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
h : i ∈ (↑s : Set ι)
j : ι
h_1 : j ∈ (↑s : Set ι)
hij : i ≠ j
⊢ onFun (β := Finset ((x : ι) × α x)) Disjoint (fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i)) i j
have rw : ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk (β := α) i) (t i) → a ∉ map (Embedding.sigmaMk (β := α) j) (t j)
Tactic: rw [Function.onFun, disjoint_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
h : i ∈ (↑s : Set ι)
j : ι
h_1 : j ∈ (↑s : Set ι)
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk (β := α) i) (t i) → a ∉ map (Embedding.sigmaMk (β := α) j) (t j)
have simp_rw : ∀ ⦃a : (x : ι) × α x⦄, (∃ a_1 ∈ t i, Sigma.mk (β := α) i a_1 = a) → ¬∃ a_2 ∈ t j, Sigma.mk (β := α) j a_2 = a
Tactic: simp_rw [mem_map, Function.Embedding.sigmaMk_apply]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ s.sigma (α := α) t = s.biUnion fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i)
have h : ∀ (x : ι) (y : α x),
  Sigma.mk (β := fun (i : ι) ↦ α i) x y ∈ s.sigma (α := α) t ↔
    Membership.mem (γ := Finset ((i : ι) × α i)) (s.biUnion fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i))
      (Sigma.mk (β := fun (i : ι) ↦ α i) x y)
Tactic: ext ⟨x, y⟩