awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s : Set G
t : Set P
a : P
x : G × P
⊢ x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.smulAntidiagonal
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s₁ s₂ : Set G
t : Set P
a : P
h : s₁ ⊆ s₂
⊢ s₁.smulAntidiagonal t a ⊆ s₂.smulAntidiagonal t a

Tactic:
fun _ hx => ⟨h hx.1, hx.2.1, hx.2.2⟩

Premises used: Set.Mem, setOf, Set.Subset, And.right, And.left, And.intro, Set.smulAntidiagonal
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s : Set G
t₁ t₂ : Set P
a : P
h : t₁ ⊆ t₂
⊢ s.smulAntidiagonal t₁ a ⊆ s.smulAntidiagonal t₂ a

Tactic:
fun _ hx => ⟨hx.1, h hx.2.1, hx.2.2⟩

Premises used: Set.Mem, setOf, Set.Subset, And.right, And.left, And.intro, Set.smulAntidiagonal
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsCancelSMul G P
h : (↑x : G × P).1 = (↑y : G × P).1
rw : a = (↑x : G × P).1 • (↑x : G × P).2
⊢ a = (↑y : G × P).1 • (↑x : G × P).2

Tactic:
rw [← h]
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsCancelSMul G P
h : (↑x : G × P).1 = (↑y : G × P).1
⊢ a = (↑x : G × P).1 • (↑x : G × P).2

Tactic:
x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsCancelSMul G P
h : (↑x : G × P).1 = (↑y : G × P).1
⊢ a = (↑x : G × P).1 • (↑x : G × P).2

Tactic:
exact x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsCancelSMul G P
h : (↑x : G × P).2 = (↑y : G × P).2
rw : a = (↑x : G × P).1 • (↑x : G × P).2
⊢ a = (↑x : G × P).1 • (↑y : G × P).2

Tactic:
rw [← h]
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsCancelSMul G P
h : (↑x : G × P).2 = (↑y : G × P).2
⊢ a = (↑x : G × P).1 • (↑x : G × P).2

Tactic:
x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsCancelSMul G P
h : (↑x : G × P).2 = (↑y : G × P).2
⊢ a = (↑x : G × P).1 • (↑x : G × P).2

Tactic:
exact x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsLeftCancelSMul G P
h : (↑x : G × P).1 = (↑y : G × P).1
rw : a = (↑x : G × P).1 • (↑x : G × P).2
⊢ a = (↑y : G × P).1 • (↑x : G × P).2

Tactic:
rw [← h]
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsLeftCancelSMul G P
h : (↑x : G × P).1 = (↑y : G × P).1
⊢ a = (↑x : G × P).1 • (↑x : G × P).2

Tactic:
x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsLeftCancelSMul G P
h : (↑x : G × P).1 = (↑y : G × P).1
⊢ a = (↑x : G × P).1 • (↑x : G × P).2

Tactic:
exact x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
inst : SMul G P
inst_1 : IsLeftCancelSMul G P
hs : s.Finite
t : Set P
p : P
x : G × P
h : x ∈ s.smulAntidiagonal t p
x_1 : G × P
h_1 : x_1 ∈ s.smulAntidiagonal t p
h_2 : x.1 = x_1.1
⊢ x = x_1

Tactic:
grind only [mem_smulAntidiagonal, IsLeftCancelSMul.left_cancel]

Premises used: Set.mem_smulAntidiagonal, IsLeftCancelSMul.left_cancel
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : SMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
inst_1 : IsCancelSMul G P
h : (↑x : G × P).2 = (↑y : G × P).2
⊢ x = y

Tactic:
Subtype.ext <| Prod.ext (fst_eq_fst_iff_snd_eq_snd.2 h) h

Premises used: Iff.mpr, Set.SMulAntidiagonal.fst_eq_fst_iff_snd_eq_snd, Prod.ext, Subtype.ext
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
x y : (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2))
h₁ : (↑x : G × P).1 ≤ (↑y : G × P).1
h₂ : (↑x : G × P).2 ≤ (↑y : G × P).2
⊢ x = y

Tactic:
eq_of_fst_eq_fst <|
    h₁.eq_of_not_lt fun hlt =>
      (smul_lt_smul_of_lt_of_le hlt h₂).ne <|
        (mem_smulAntidiagonal.1 x.2).2.2.trans (mem_smulAntidiagonal.1 y.2).2.2.symm

Premises used: Set.mem_smulAntidiagonal, LE.le.eq_of_not_lt, SMul.smul_lt_smul_of_lt_of_le, And.right, Iff.mp, Set.SMulAntidiagonal.eq_of_fst_eq_fst, Eq.symm, Eq.trans, LT.lt.ne, Subtype.property
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
by_contra! : ∀ (h : (s.smulAntidiagonal t a).Infinite), False
⊢ (s.smulAntidiagonal t a).Finite

Tactic:
by_contra! h
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
⊢ (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)

Tactic:
have h1 : (smulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o (· ≤ ·)) :=
    fun f ↦ hs fun n ↦ ⟨_, (mem_smulAntidiagonal.1 (f n).2).1⟩
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
⊢ (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)

Tactic:
have h2 : (smulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o (· ≤ ·)) :=
    fun f ↦ ht fun n ↦ ⟨_, (mem_smulAntidiagonal.1 (f n).2).2.1⟩
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
obtain :
  ∀ (g : ℕ ↪o ℕ)
    (hg :
      ∀ (m n : ℕ),
        m ≤ n →
          Order.Preimage (α := G × P) Prod.fst (fun (x1 x2 : G) ↦ x1 ≤ x2)
            (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                    (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
                  ((g : (a : ℕ) → ℕ) m : ℕ)) :
              G × P)
            (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                    (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
                  ((g : (a : ℕ) → ℕ) n : ℕ)) :
              G × P)),
    False
⊢ False

Tactic:
obtain ⟨g, hg⟩ := h1.exists_monotone_subseq fun n ↦ (h.natEmbedding _ n).2

Premises used: Set.PartiallyWellOrderedOn.exists_monotone_subseq, Set.Infinite.natEmbedding, Set.smulAntidiagonal, DFunLike.coe, Subtype.property
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := G × P) Prod.fst (fun (x1 x2 : G) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          G × P)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          G × P)
obtain :
  ∀ (m n : ℕ) (mn : m < n)
    (h2' :
      Subrel (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2) (fun (x : G × P) ↦ x ∈ s.smulAntidiagonal t a)
        ((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
            (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
          ((g : (a : ℕ) → ℕ) m : ℕ))
        ((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
            (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
          ((g : (a : ℕ) → ℕ) n : ℕ))),
    False
⊢ False

Tactic:
obtain ⟨m, n, mn, h2'⟩ := h2 fun n ↦ h.natEmbedding _ _

Premises used: Set.Infinite.natEmbedding, Set.smulAntidiagonal, DFunLike.coe
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := G × P) Prod.fst (fun (x1 x2 : G) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          G × P)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          G × P)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2) (fun (x : G × P) ↦ x ∈ s.smulAntidiagonal t a)
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) n : ℕ))
⊢ False

Tactic:
mn.ne (g.injective <| (h.natEmbedding _).injective ?_)

Premises used: RelEmbedding.injective, Set.Infinite.natEmbedding, Function.Embedding.injective, LT.lt.ne
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := G × P) Prod.fst (fun (x1 x2 : G) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          G × P)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          G × P)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2) (fun (x : G × P) ↦ x ∈ s.smulAntidiagonal t a)
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) n : ℕ))
refine :
  Eq (α := (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
        ((g : (a : ℕ) → ℕ) m : ℕ) :
      (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
        ((g : (a : ℕ) → ℕ) n : ℕ) :
      (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
⊢ False

Tactic:
refine mn.ne (g.injective <| (h.natEmbedding _).injective ?_)

Premises used: RelEmbedding.injective, Set.Infinite.natEmbedding, Function.Embedding.injective, LT.lt.ne
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := G × P) Prod.fst (fun (x1 x2 : G) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          G × P)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          G × P)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2) (fun (x : G × P) ↦ x ∈ s.smulAntidiagonal t a)
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) n : ℕ))
⊢ Eq (α := (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
        ((g : (a : ℕ) → ℕ) m : ℕ) :
      (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
        ((g : (a : ℕ) → ℕ) n : ℕ) :
      (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))

Tactic:
eq_of_fst_le_fst_of_snd_le_snd (hg _ _ mn.le) h2'

Premises used: Set.SMulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd, LT.lt.le
-- Module: Mathlib.Data.Set.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst : PartialOrder G
inst_1 : PartialOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : G) ↦ x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := G × P) Prod.fst (fun (x1 x2 : G) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          G × P)
        (↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h :
                (a_2 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          G × P)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : P) ↦ x1 ≤ x2) (fun (x : G × P) ↦ x ∈ s.smulAntidiagonal t a)
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
      ((g : (a : ℕ) → ℕ) n : ℕ))
⊢ Eq (α := (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
        ((g : (a : ℕ) → ℕ) m : ℕ) :
      (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
    ((Infinite.natEmbedding (s.smulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))
        ((g : (a : ℕ) → ℕ) n : ℕ) :
      (↑(s.smulAntidiagonal t a) : Type (max u_1 u_2)))

Tactic:
exact eq_of_fst_le_fst_of_snd_le_snd (hg _ _ mn.le) h2'

Premises used: Set.SMulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd, LT.lt.le
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
s : Set α
⊢ (down : (a : SetSemiring α) → Set α) ((up : (a : Set α) → SetSemiring α) s : SetSemiring α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
s : SetSemiring α
⊢ (up : (a : Set α) → SetSemiring α) ((down : (a : SetSemiring α) → Set α) s : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
s t : Set α
⊢ LE.le (α := SetSemiring α) ((up : (a : Set α) → SetSemiring α) s : SetSemiring α)
      ((up : (a : Set α) → SetSemiring α) t : SetSemiring α) ↔
    s ⊆ t

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
s t : Set α
⊢ LT.lt (α := SetSemiring α) ((up : (a : Set α) → SetSemiring α) s : SetSemiring α)
      ((up : (a : Set α) → SetSemiring α) t : SetSemiring α) ↔
    s ⊂ t

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
s t : SetSemiring α
⊢ Subset (α := Set α) ((down : (a : SetSemiring α) → Set α) s : Set α)
      ((down : (a : SetSemiring α) → Set α) t : Set α) ↔
    s ≤ t

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
s t : SetSemiring α
⊢ SSubset (α := Set α) ((down : (a : SetSemiring α) → Set α) s : Set α)
      ((down : (a : SetSemiring α) → Set α) t : Set α) ↔
    s < t

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := SetSemiring α) (0 : SetSemiring α) ((up : (a : Set α) → SetSemiring α) ∅ : SetSemiring α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set α) ((down : (a : SetSemiring α) → Set α) 0 : Set α) (∅ : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := SetSemiring α) ((up : (a : Set α) → SetSemiring α) ∅ : SetSemiring α) (0 : SetSemiring α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
s t : SetSemiring α
⊢ s + t =
    (up : (a : Set α) → SetSemiring α)
      ((down : (a : SetSemiring α) → Set α) s ∪ (down : (a : SetSemiring α) → Set α) t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
s t : SetSemiring α
⊢ Eq (α := Set α) ((down : (a : SetSemiring α) → Set α) (s + t) : Set α)
    ((down : (a : SetSemiring α) → Set α) s ∪ (down : (a : SetSemiring α) → Set α) t : Set α)

Tactic:
rfl

Premises used: Set.union, setOf, rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
s t : Set α
⊢ (up : (a : Set α) → SetSemiring α) (s ∪ t) =
    HAdd.hAdd (α := SetSemiring α) (β := SetSemiring α) ((up : (a : Set α) → SetSemiring α) s : SetSemiring α)
      ((up : (a : Set α) → SetSemiring α) t : SetSemiring α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
β : Type u_2
⊢ AddLeftMono.{u_1} (SetSemiring α)

Tactic:
⟨fun _ _ _ => union_subset_union_right _⟩

Premises used: CovariantClass.mk, SetSemiring.down, Set.union_subset_union_right, DFunLike.coe
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
inst : Mul α
s t : SetSemiring α
⊢ s * t =
    (up : (a : Set α) → SetSemiring α)
      (HMul.hMul (α := Set α) (β := Set α) ((down : (a : SetSemiring α) → Set α) s : Set α)
        ((down : (a : SetSemiring α) → Set α) t : Set α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
inst : Mul α
s t : SetSemiring α
⊢ (down : (a : SetSemiring α) → Set α) (s * t) =
    HMul.hMul (α := Set α) (β := Set α) ((down : (a : SetSemiring α) → Set α) s : Set α)
      ((down : (a : SetSemiring α) → Set α) t : Set α)

Tactic:
rfl

Premises used: setOf, Set.image2, rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
inst : Mul α
s t : Set α
⊢ (up : (a : Set α) → SetSemiring α) (s * t) =
    HMul.hMul (α := SetSemiring α) (β := SetSemiring α) ((up : (a : Set α) → SetSemiring α) s : SetSemiring α)
      ((up : (a : Set α) → SetSemiring α) t : SetSemiring α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
⊢ NoZeroDivisors.{u_1} (SetSemiring α)

Tactic:
⟨fun {a b} ab =>
    a.eq_empty_or_nonempty.imp_right fun ha =>
      b.eq_empty_or_nonempty.resolve_right fun hb =>
        Nonempty.ne_empty ⟨_, mul_mem_mul ha.some_mem hb.some_mem⟩ ab⟩

Premises used: HMul.hMul, Set.Nonempty.ne_empty, Set.Nonempty.some_mem, Set.eq_empty_or_nonempty, Exists.intro, Or.resolve_right, Or.imp_right, Set.mul_mem_mul, NoZeroDivisors.mk, Set.Nonempty.some
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
⊢ MulLeftMono.{u_1} (SetSemiring α)

Tactic:
⟨fun _ _ _ => mul_subset_mul_left⟩

Premises used: CovariantClass.mk, Set.mul_subset_mul_left
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
⊢ MulRightMono.{u_1} (SetSemiring α)

Tactic:
⟨fun _ _ _ => mul_subset_mul_right⟩

Premises used: CovariantClass.mk, Set.mul_subset_mul_right
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := SetSemiring α) (1 : SetSemiring α) ((up : (a : Set α) → SetSemiring α) 1 : SetSemiring α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := Set α) ((down : (a : SetSemiring α) → Set α) 1 : Set α) (1 : Set α)

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := SetSemiring α) ((up : (a : Set α) → SetSemiring α) 1 : SetSemiring α) (1 : SetSemiring α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
⊢ IsOrderedRing.{u_1} (SetSemiring α)

Tactic:
CanonicallyOrderedAdd.toIsOrderedRing

Premises used: CanonicallyOrderedAdd.toIsOrderedRing