awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
refine :
  ∀
    (h :
      Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
        (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))),
    f = g
⊢ Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) ↔
    f = g

Tactic:
refine ⟨fun h ↦ ?_, by rintro rfl; rfl⟩
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
ef : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑f : (a : α) → β) Set.univ ⋯
eg : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑g : (a : α) → β) Set.univ ⋯
⊢ Eq.{u_2 + 1} (α := Set β) (Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ)
    (Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ)

Tactic:
simpa using h
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
ef : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑f : (a : α) → β) Set.univ ⋯
eg : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑g : (a : α) → β) Set.univ ⋯
⊢ ∀ {a b : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2)},
    LE.le (α := (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2))
        ((Equiv.setCongr (s := Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) (t :=
                Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) ⋯ :
              (a : (↑((⇑f : (a : α) → β) '' Set.univ) : Type u_2)) → (↑((⇑g : (a : α) → β) '' Set.univ) : Type u_2))
            a :
          (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2))
        ((Equiv.setCongr (s := Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) (t :=
                Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) ⋯ :
              (a : (↑((⇑f : (a : α) → β) '' Set.univ) : Type u_2)) → (↑((⇑g : (a : α) → β) '' Set.univ) : Type u_2))
            b :
          (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2)) ↔
      a ≤ b

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
ef : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑f : (a : α) → β) Set.univ ⋯
eg : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑g : (a : α) → β) Set.univ ⋯
i : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) ≃o
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  let __spread.0 :=
    Equiv.setCongr (s := Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) (t :=
      Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) ⋯;
  RelIso.mk (r := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2)
    (s := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2) __spread.0
    ⋯
⊢ (ef.trans i).trans eg.symm = OrderIso.refl (↑Set.univ : Type u_1)

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
ef : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑f : (a : α) → β) Set.univ ⋯
eg : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑g : (a : α) → β) Set.univ ⋯
i : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) ≃o
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  let __spread.0 :=
    Equiv.setCongr (s := Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) (t :=
      Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) ⋯;
  RelIso.mk (r := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2)
    (s := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2) __spread.0
    ⋯
⊢ (ef.trans i).trans eg.symm = OrderIso.refl (↑Set.univ : Type u_1)

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
ef : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑f : (a : α) → β) Set.univ ⋯
eg : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑g : (a : α) → β) Set.univ ⋯
i : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) ≃o
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  let __spread.0 :=
    Equiv.setCongr (s := Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) (t :=
      Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) ⋯;
  RelIso.mk (r := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2)
    (s := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2) __spread.0
    ⋯
⊢ (ef.trans i).trans eg.symm = OrderIso.refl (↑Set.univ : Type u_1)

Tactic:
have : (ef.trans i).trans eg.symm = .refl _ := by
    exact Subsingleton.elim _ _
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
ef : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑f : (a : α) → β) Set.univ ⋯
eg : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑g : (a : α) → β) Set.univ ⋯
i : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) ≃o
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  let __spread.0 :=
    Equiv.setCongr (s := Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) (t :=
      Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) ⋯;
  RelIso.mk (r := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2)
    (s := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2) __spread.0
    ⋯
this : (ef.trans i).trans eg.symm = OrderIso.refl (↑Set.univ : Type u_1)
h₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
ef : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑f : (a : α) → β) Set.univ ⋯
eg : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑g : (a : α) → β) Set.univ ⋯
i : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) ≃o
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  let __spread.0 :=
    Equiv.setCongr (s := Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) (t :=
      Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) ⋯;
  RelIso.mk (r := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2)
    (s := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2) __spread.0
    ⋯
this : (ef.trans i).trans eg.symm = OrderIso.refl (↑Set.univ : Type u_1)
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
simpa only [OrderIso.trans_apply, OrderIso.apply_symm_apply, OrderIso.refl_apply, Subtype.ext_iff]
    using congr(eg ($this ⟨x, Set.mem_univ x⟩))

Premises used: OrderIso.apply_symm_apply, OrderIso.refl_apply, OrderIso.trans_apply, Subtype.ext_iff
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f : α →o β
hf hg : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α →o β
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hg : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑g : (a : α) → β)
refine :
  ∀
    (h :
      Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
        (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))),
    f = g
⊢ Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) ↔
    f = g

Tactic:
refine ⟨fun h ↦ ?_, by rintro rfl; rfl⟩
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α →o β
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hg : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑g : (a : α) → β)
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
h₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
ext : 2
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α →o β
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hg : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑g : (a : α) → β)
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
x : α
⊢ Eq.{u_2 + 1} (α := Set β)
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑(OrderEmbedding.ofStrictMono (⇑f : (a : α) → β) ⋯) : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑(OrderEmbedding.ofStrictMono (⇑g : (a : α) → β) ⋯) : (a : α) → β))

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α →o β
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hg : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑g : (a : α) → β)
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
exact DFunLike.congr_fun ((OrderEmbedding.range_eq_iff
    (f := .ofStrictMono f (f.monotone.strictMono_of_injective hf))
    (g := .ofStrictMono g (g.monotone.strictMono_of_injective hg))).1 (by simpa)) _

Premises used: DFunLike.congr_fun, Iff.mp, OrderEmbedding.range_eq_iff
-- Module: Mathlib.Data.Finset.Sort
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Finite α
f : α →o α
hf : Function.Injective (α := α) (β := α) (⇑f : (a : α) → α)
⊢ Eq (α := Set α) (Set.range (ι := α) (⇑f : (a : α) → α)) (Set.range (ι := α) (⇑id : (a : α) → α))

Tactic:
simpa [Set.range_eq_univ] using Finite.surjective_of_injective hf

Premises used: Set.range_eq_univ, Finite.surjective_of_injective
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).val = s.val.disjSum t.val

Tactic:
rfl

Premises used: rfl, Multiset.disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
t : Finset β
⊢ Eq (α := Finset (α ⊕ β)) (disjSum ∅ t) (map Embedding.inr t)

Tactic:
val_inj.1 <| Multiset.zero_disjSum _

Premises used: Iff.mp, Finset.val_inj, Multiset.zero_disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
⊢ Eq (α := Finset (α ⊕ β)) (s.disjSum ∅) (map Embedding.inl s)

Tactic:
val_inj.1 <| Multiset.disjSum_zero _

Premises used: Multiset.disjSum_zero, Iff.mp, Finset.val_inj
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ #(s.disjSum t) = #s + #t

Tactic:
Multiset.card_disjSum _ _

Premises used: Finset.card, Multiset.card_disjSum, Multiset.disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
simp_rw :
  ∀ ⦃a : α ⊕ β⦄,
    (∃ a_1 ∈ s, (Embedding.inl : (a : α) → α ⊕ β) a_1 = a) → ¬∃ a_2 ∈ t, (Embedding.inr : (a : β) → α ⊕ β) a_2 = a
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)

Tactic:
simp_rw [disjoint_left, mem_map]

Premises used: Finset.disjoint_left, Finset.mem_map
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ disjUnion (map Embedding.inl s) (map Embedding.inr t) ⋯ = s.disjSum t

Tactic:
rfl

Premises used: Multiset.map, Finset.disjUnion, Finset.disjSum, rfl, Multiset.disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : α ⊕ β
⊢ x ∈ s.disjSum t ↔ (∃ a ∈ s, inl a = x) ∨ ∃ b ∈ t, inr b = x

Tactic:
Multiset.mem_disjSum

Premises used: Set.Mem, setOf, Multiset.mem_disjSum, Multiset.Mem, Multiset.disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
a : α
⊢ inl a ∈ s.disjSum t ↔ a ∈ s

Tactic:
Multiset.inl_mem_disjSum

Premises used: Set.Mem, setOf, Multiset.inl_mem_disjSum, Multiset.Mem, Multiset.disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
b : β
⊢ inr b ∈ s.disjSum t ↔ b ∈ t

Tactic:
Multiset.inr_mem_disjSum

Premises used: Multiset.inr_mem_disjSum, Set.Mem, setOf, Multiset.Mem, Multiset.disjSum
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ s₁.disjSum t₁ ⊆ s₂.disjSum t₂

Tactic:
val_le_iff.1 <| Multiset.disjSum_mono (val_le_iff.2 hs) (val_le_iff.2 ht)

Premises used: Iff.mpr, Multiset.disjSum_mono, Iff.mp, Finset.val_le_iff
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
t : Finset β
⊢ Monotone (β := Finset (α ⊕ β)) fun (s : Finset α) ↦ s.disjSum t

Tactic:
fun _ _ hs => disjSum_mono hs Subset.rfl

Premises used: Finset.Subset.rfl, Set.Mem, Monotone, setOf, Finset.disjSum_mono
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
⊢ Monotone (α := Finset β) s.disjSum

Tactic:
fun _ _ => disjSum_mono Subset.rfl

Premises used: Finset.Subset.rfl, Monotone, Finset.disjSum_mono
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₁ ⊂ s₂
ht : t₁ ⊆ t₂
⊢ s₁.disjSum t₁ ⊂ s₂.disjSum t₂

Tactic:
val_lt_iff.1 <| disjSum_lt_disjSum_of_lt_of_le (val_lt_iff.2 hs) (val_le_iff.2 ht)

Premises used: Iff.mpr, Finset.val_lt_iff, Multiset.disjSum_lt_disjSum_of_lt_of_le, Iff.mp, Finset.val_le_iff
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₁ ⊆ s₂
ht : t₁ ⊂ t₂
⊢ s₁.disjSum t₁ ⊂ s₂.disjSum t₂

Tactic:
val_lt_iff.1 <| disjSum_lt_disjSum_of_le_of_lt (val_le_iff.2 hs) (val_lt_iff.2 ht)

Premises used: Iff.mpr, Finset.val_lt_iff, Multiset.disjSum_lt_disjSum_of_le_of_lt, Iff.mp, Finset.val_le_iff
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
t : Finset β
⊢ StrictMono (β := Finset (α ⊕ β)) fun (s : Finset α) ↦ s.disjSum t

Tactic:
fun _ _ hs => disjSum_ssubset_disjSum_of_ssubset_of_subset hs Subset.rfl

Premises used: StrictMono, Finset.Subset.rfl, Set.Mem, setOf, Set.Subset, Finset.disjSum_ssubset_disjSum_of_ssubset_of_subset
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
⊢ StrictMono (α := Finset β) s.disjSum

Tactic:
fun _ _ =>
  disjSum_ssubset_disjSum_of_subset_of_ssubset Subset.rfl

Premises used: StrictMono, Finset.Subset.rfl, Finset.disjSum_ssubset_disjSum_of_subset_of_ssubset, Set.Subset
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_4
β : Type u_5
s₁ s₂ : Finset α
t₁ t₂ : Finset β
⊢ s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_4
β : Type u_5
x x_1 : Finset α
x_2 x_3 : Finset β
⊢ x.disjSum x_2 = x_1.disjSum x_3 → x = x_1 ∧ x_2 = x_3

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim some (fun (x : β) ↦ none) a, b ∈ Sum.elim some (fun (x : β) ↦ none) a' → a = a'

Tactic:
aesop
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim (fun (x : α) ↦ none) some a, b ∈ Sum.elim (fun (x : α) ↦ none) some a' → a = a'

Tactic:
aesop
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
⊢ a ∈ u.toLeft ↔ inl a ∈ u

Tactic:
simp [toLeft]

Premises used: Finset.toLeft
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
⊢ b ∈ u.toRight ↔ inr b ∈ u

Tactic:
simp [toRight]

Premises used: Finset.toRight
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x : α
⊢ x ∈ u.toLeft → x ∈ v.toLeft

Tactic:
simpa only [mem_toLeft] using @h _

Premises used: Finset.mem_toLeft
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x : β
⊢ x ∈ u.toRight → x ∈ v.toRight

Tactic:
simpa only [mem_toRight] using @h _

Premises used: Finset.mem_toRight
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
⊢ Monotone (α := Finset (α ⊕ β)) toLeft

Tactic:
fun _ _ => toLeft_subset_toLeft

Premises used: Finset.toLeft_subset_toLeft, Monotone
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
⊢ Monotone (α := Finset (α ⊕ β)) toRight

Tactic:
fun _ _ => toRight_subset_toRight

Premises used: Monotone, Finset.toRight_subset_toRight
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
h : ∀ (x : α), inl x ∈ u.toLeft.disjSum u.toRight ↔ inl x ∈ u
h₁ : ∀ (x : β), inr x ∈ u.toLeft.disjSum u.toRight ↔ inr x ∈ u
⊢ u.toLeft.disjSum u.toRight = u

Tactic:
ext (x | x)
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ inl x ∈ u.toLeft.disjSum u.toRight ↔ inl x ∈ u

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ inr x ∈ u.toLeft.disjSum u.toRight ↔ inr x ∈ u

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
rw : #(u.toLeft.disjSum u.toRight) = #u
rw₁ rw₂ : #u = #u
⊢ #u.toLeft + #u.toRight = #u

Tactic:
rw [← card_disjSum, toLeft_disjSum_toRight]

Premises used: Finset.card_disjSum, Finset.toLeft_disjSum_toRight
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ #u.toLeft ≤ #u

Tactic:
(Nat.le_add_right _ _).trans_eq card_toLeft_add_card_toRight

Premises used: LE.le.trans_eq, Nat.le_add_right, Finset.card_toLeft_add_card_toRight
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ #u.toRight ≤ #u

Tactic:
(Nat.le_add_left _ _).trans_eq card_toLeft_add_card_toRight

Premises used: LE.le.trans_eq, Nat.le_add_left, Finset.card_toLeft_add_card_toRight
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ (s.disjSum t).toLeft ↔ x ∈ s
⊢ (s.disjSum t).toLeft = s

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : α
⊢ x ∈ (s.disjSum t).toLeft ↔ x ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
h : ∀ (x : β), x ∈ (s.disjSum t).toRight ↔ x ∈ t
⊢ (s.disjSum t).toRight = t

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : β
⊢ x ∈ (s.disjSum t).toRight ↔ x ∈ t

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : s.disjSum t = u
⊢ s = u.toLeft ∧ t = u.toRight

Tactic:
simp [← h]
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : s = u.toLeft ∧ t = u.toRight
⊢ s.disjSum t = u

Tactic:
simp [h, toLeft_disjSum_toRight]

Premises used: Finset.toLeft_disjSum_toRight
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : u = s.disjSum t
⊢ u.toLeft = s ∧ u.toRight = t

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : u.toLeft = s ∧ u.toRight = t
⊢ u = s.disjSum t

Tactic:
simp [← h, toLeft_disjSum_toRight]

Premises used: Finset.toLeft_disjSum_toRight
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
⊢ s.disjSum t ⊆ u ↔ s ⊆ u.toLeft ∧ t ⊆ u.toRight

Tactic:
simp [subset_iff]

Premises used: Finset.subset_iff
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
⊢ u ⊆ s.disjSum t ↔ u.toLeft ⊆ s ∧ u.toRight ⊆ t

Tactic:
simp [subset_iff]

Premises used: Finset.subset_iff
-- Module: Mathlib.Data.Finset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Finset α
u : Finset (α ⊕ β)
⊢ u ⊆ map Embedding.inl s ↔ u.toLeft ⊆ s ∧ u.toRight = ∅

Tactic:
simp [← disjSum_empty, subset_disjSum]

Premises used: Finset.disjSum_empty, Finset.subset_disjSum