awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s s₂ : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
h : MonotoneOn f s
h' : s₂ ⊆ s
⊢ MonotoneOn f s₂

Tactic:
fun _ hx _ hy => h (h' hx) (h' hy)

Premises used: MonotoneOn
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s s₂ : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
h : AntitoneOn f s
h' : s₂ ⊆ s
⊢ AntitoneOn f s₂

Tactic:
fun _ hx _ hy => h (h' hx) (h' hy)

Premises used: AntitoneOn
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s s₂ : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
h : StrictMonoOn f s
h' : s₂ ⊆ s
⊢ StrictMonoOn f s₂

Tactic:
fun _ hx _ hy => h (h' hx) (h' hy)

Premises used: StrictMonoOn
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s s₂ : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
h : StrictAntiOn f s
h' : s₂ ⊆ s
⊢ StrictAntiOn f s₂

Tactic:
fun _ hx _ hy => h (h' hx) (h' hy)

Premises used: StrictAntiOn
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
h : MonotoneOn f s
⊢ Monotone (α := (↑s : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
fun x y hle => h x.coe_prop y.coe_prop hle

Premises used: Subtype.coe_prop, Monotone
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
h : AntitoneOn f s
⊢ Antitone (α := (↑s : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
fun x y hle => h x.coe_prop y.coe_prop hle

Premises used: Subtype.coe_prop, Antitone
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
h : StrictMonoOn f s
⊢ StrictMono (α := (↑s : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
fun x y hlt => h x.coe_prop y.coe_prop hlt

Premises used: Subtype.coe_prop, StrictMono
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
h : StrictAntiOn f s
⊢ StrictAnti (α := (↑s : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
fun x y hlt => h x.coe_prop y.coe_prop hlt

Premises used: Subtype.coe_prop, StrictAnti
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
⊢ MonotoneOn f (insert a s) ↔
    (∀ (b : α), b ∈ s → b ≤ a → f b ≤ f a) ∧ (∀ (b : α), b ∈ s → a ≤ b → f a ≤ f b) ∧ MonotoneOn f s

Tactic:
simp [MonotoneOn, forall_and]

Premises used: MonotoneOn, forall_and
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
⊢ AntitoneOn f (insert a s) ↔
    (∀ (b : α), b ∈ s → b ≤ a → f a ≤ f b) ∧ (∀ (b : α), b ∈ s → a ≤ b → f b ≤ f a) ∧ AntitoneOn f s

Tactic:
@monotoneOn_insert_iff α βᵒᵈ _ _ _ _ _

Premises used: AntitoneOn, Set.monotoneOn_insert_iff
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : Monotone f
s : Set α
⊢ Monotone (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
fun _ _ hxy =>
  h hxy

Premises used: Monotone, Set.restrict
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : Monotone f
s : Set β
hs : ∀ (x : α), f x ∈ s
⊢ Monotone (Set.codRestrict f s hs)

Tactic:
h

Premises used: Monotone, Set.codRestrict
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : Monotone f
⊢ Monotone (Set.rangeFactorization f)

Tactic:
h

Premises used: Monotone, Set.rangeFactorization
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ StrictMono (s.restrict (π := fun (a : α) ↦ β) f) ↔ StrictMonoOn f s

Tactic:
simp [Set.restrict, StrictMono, StrictMonoOn]

Premises used: StrictMono, Set.restrict, StrictMonoOn
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
s : Set β
hs : ∀ (x : α), f x ∈ s
⊢ StrictMono (Set.codRestrict f s hs)

Tactic:
hf

Premises used: StrictMono, Set.codRestrict
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
⊢ StrictMonoOn f (insert a s) ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
simp [StrictMonoOn, forall_and]

Premises used: StrictMonoOn, forall_and
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
⊢ StrictAntiOn f (insert a s) ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s

Tactic:
@strictMonoOn_insert_iff α βᵒᵈ _ _ _ _ _

Premises used: StrictAntiOn, strictMonoOn_insert_iff
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
rw :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s

Tactic:
rw [strictMonoOn_insert_iff]

Premises used: strictMonoOn_insert_iff
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b

Tactic:
cases (ha _ hb).not_gt hab

Premises used: LE.le.not_gt
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ ∀ (b : α), b ∈ s → a < b → f a < f b

Tactic:
have : ∀ b ∈ s, a < b → f a < f b := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    StrictMonoOn f s →
      (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr₃ : (∀ (b : α), b ∈ s → b < a → f b < f a) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
mpr₄ : (∀ (b : α), b ∈ s → b < a → f b < f a) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
mpr₅ : (∀ (b : α), b ∈ s → b < a → f b < f a) → StrictMonoOn f s → StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s

Tactic:
tauto
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
rw :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
rw [strictMonoOn_insert_iff]

Premises used: strictMonoOn_insert_iff
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
hb : b ∈ s
hab : b < a
⊢ f b < f a

Tactic:
cases (ha _ hb).not_gt hab

Premises used: LE.le.not_gt
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ ∀ (b : α), b ∈ s → b < a → f b < f a

Tactic:
have : ∀ b ∈ s, b < a → f b < f a := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → a < b → f a < f b) →
    StrictMonoOn f s →
      (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr₃ : (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
mpr₄ : (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
mpr₅ : (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
tauto
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
rw :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
⊢ StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s

Tactic:
rw [strictAntiOn_insert_iff]

Premises used: strictAntiOn_insert_iff
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
hb : b ∈ s
hab : a < b
⊢ f b < f a

Tactic:
cases (ha _ hb).not_gt hab

Premises used: LE.le.not_gt
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ ∀ (b : α), b ∈ s → a < b → f b < f a

Tactic:
have : ∀ b ∈ s, a < b → f b < f a := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    StrictAntiOn f s →
      (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr₃ : (∀ (b : α), b ∈ s → b < a → f a < f b) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
mpr₄ : (∀ (b : α), b ∈ s → b < a → f a < f b) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
mpr₅ : (∀ (b : α), b ∈ s → b < a → f a < f b) → StrictAntiOn f s → StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s

Tactic:
tauto
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
rw :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
⊢ StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s

Tactic:
rw [strictAntiOn_insert_iff]

Premises used: strictAntiOn_insert_iff
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
hb : b ∈ s
hab : b < a
⊢ f a < f b

Tactic:
cases (ha _ hb).not_gt hab

Premises used: LE.le.not_gt
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ ∀ (b : α), b ∈ s → b < a → f a < f b

Tactic:
have : ∀ b ∈ s, b < a → f a < f b := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → a < b → f b < f a) →
    StrictAntiOn f s →
      (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr₃ : (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
mpr₄ : (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
mpr₅ : (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s

Tactic:
tauto
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
inl : ∀ (ψxy : ψ x ≤ ψ y), ψ x ≤ ψ y
inr : ∀ (ψyx : ψ y ≤ ψ x), ψ x ≤ ψ y
⊢ ψ x ≤ ψ y

Tactic:
rcases le_total (ψ x) (ψ y) with (ψxy | ψyx)

Premises used: le_total
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψxy : ψ x ≤ ψ y
⊢ ψ x ≤ ψ y

Tactic:
ψxy
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψxy : ψ x ≤ ψ y
⊢ ψ x ≤ ψ y

Tactic:
exact ψxy
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
⊢ φ (ψ y) ≤ φ (ψ x)

Tactic:
have := hφ (ψts ys) (ψts xs) ψyx
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : φ (ψ y) ≤ φ (ψ x)
⊢ y ≤ x

Tactic:
rw [φψs.eq ys, φψs.eq xs] at this

Premises used: Set.RightInvOn.eq
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ x
inr : ∀ (ys : x ∈ s) (l : x ≤ x) (ψyx : ψ x ≤ ψ x) (this : x ≤ x), ψ x ≤ ψ x
⊢ ψ x ≤ ψ y

Tactic:
induction le_antisymm l this

Premises used: le_antisymm
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : x ∈ s
l : x ≤ x
ψyx : ψ x ≤ ψ x
this : x ≤ x
⊢ ψ x ≤ ψ x

Tactic:
le_refl _

Premises used: le_refl
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : x ∈ s
l : x ≤ x
ψyx : ψ x ≤ ψ x
this : x ≤ x
⊢ ψ x ≤ ψ x

Tactic:
exact le_refl _

Premises used: le_refl
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : AntitoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
⊢ AntitoneOn ψ s

Tactic:
(monotoneOn_of_rightInvOn_of_mapsTo hφ.dual_left φψs ψts).dual_right

Premises used: AntitoneOn.dual_left, Function.monotoneOn_of_rightInvOn_of_mapsTo, MonotoneOn.dual_right, OrderDual
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : Mul α
s t : Set α
a : α
x : α × α
⊢ x ∈ s.mulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a

Tactic:
Iff.rfl

Premises used: Set.mulAntidiagonal, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : Mul α
s₁ s₂ t : Set α
a : α
h : s₁ ⊆ s₂
⊢ s₁.mulAntidiagonal t a ⊆ s₂.mulAntidiagonal t a

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

Premises used: Set.mulAntidiagonal, Set.Mem, setOf, Set.Subset, And.right, And.left, And.intro
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : Mul α
s t₁ t₂ : Set α
a : α
h : t₁ ⊆ t₂
⊢ s.mulAntidiagonal t₁ a ⊆ s.mulAntidiagonal t₂ a

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

Premises used: Set.mulAntidiagonal, Set.Mem, setOf, Set.Subset, And.right, And.left, And.intro
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMagma α
s t : Set α
a : α
x : α × α
⊢ x.swap ∈ s.mulAntidiagonal t a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
simp [mul_comm, and_left_comm]

Premises used: and_left_comm, mul_comm
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMagma α
s t : Set α
a : α
x : α × α
⊢ x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 * x.1 = a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
simp [mul_comm, and_left_comm]

Premises used: and_left_comm, mul_comm
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).1 = (↑y : α × α).1
rw : a = (↑x : α × α).1 * (↑x : α × α).2
⊢ a = (↑y : α × α).1 * (↑x : α × α).2

Tactic:
rw [← h]
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).1 = (↑y : α × α).1
⊢ a = (↑x : α × α).1 * (↑x : α × α).2

Tactic:
x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).1 = (↑y : α × α).1
⊢ a = (↑x : α × α).1 * (↑x : α × α).2

Tactic:
exact x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).2 = (↑y : α × α).2
rw : a = (↑x : α × α).1 * (↑x : α × α).2
⊢ a = (↑x : α × α).1 * (↑y : α × α).2

Tactic:
rw [← h]
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).2 = (↑y : α × α).2
⊢ a = (↑x : α × α).1 * (↑x : α × α).2

Tactic:
x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).2 = (↑y : α × α).2
⊢ a = (↑x : α × α).1 * (↑x : α × α).2

Tactic:
exact x.2.2.2.symm

Premises used: And.right, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).1 = (↑y : α × α).1
⊢ x = y

Tactic:
Subtype.ext <| Prod.ext h <| fst_eq_fst_iff_snd_eq_snd.1 h

Premises used: Prod.ext, Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd, Iff.mp, Subtype.ext
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).2 = (↑y : α × α).2
⊢ x = y

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

Premises used: Iff.mpr, Prod.ext, Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd, Subtype.ext
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h₁ : (↑x : α × α).1 ≤ (↑y : α × α).1
h₂ : (↑x : α × α).2 ≤ (↑y : α × α).2
⊢ x = y

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

Premises used: LE.le.eq_of_not_lt, Set.MulAntidiagonal.eq_of_fst_eq_fst, And.right, Iff.mp, Eq.symm, mul_lt_mul_of_lt_of_le, Eq.trans, LT.lt.ne, Subtype.property, Set.mem_mulAntidiagonal
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
by_contra! : ∀ (h : (s.mulAntidiagonal t a).Infinite), False
⊢ (s.mulAntidiagonal t a).Finite

Tactic:
by_contra! h