awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 < (f j, g j, j).1
⊢ f i ≤ f j

Tactic:
exact h.le

Premises used: LT.lt.le
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 = (f j, g j, j).1
⊢ f i ≤ f j

Tactic:
h.le

Premises used: Eq.le
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 = (f j, g j, j).1
⊢ f i ≤ f j

Tactic:
exact h.le

Premises used: Eq.le
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
refine_2 : ∀ (h : (f i, g i, i).1 < (f j, g j, j).1), g i ≤ g j
refine_2₁ : ∀ (h : Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2), g i ≤ g j
⊢ g i ≤ g j

Tactic:
obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij

Premises used: Prod.lex_iff, Iff.mp
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 < (f j, g j, j).1
⊢ g i ≤ g j

Tactic:
hfg.symm hi hj h

Premises used: MonovaryOn.symm
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 < (f j, g j, j).1
⊢ g i ≤ g j

Tactic:
exact hfg.symm hi hj h

Premises used: MonovaryOn.symm
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
refine_2 : ∀ (h : (f i, g i, i).2.1 < (f j, g j, j).2.1), g i ≤ g j
refine_2₁ : ∀ (h : (f i, g i, i).2.1 = (f j, g j, j).2.1), g i ≤ g j
⊢ g i ≤ g j

Tactic:
obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h

Premises used: Prod.lex_iff, Iff.mp
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h_1 : Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
h : (f i, g i, i).2.1 < (f j, g j, j).2.1
⊢ g i ≤ g j

Tactic:
h.le

Premises used: LT.lt.le
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h_1 : Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
h : (f i, g i, i).2.1 < (f j, g j, j).2.1
⊢ g i ≤ g j

Tactic:
exact h.le

Premises used: LT.lt.le
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h_1 : Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
h : (f i, g i, i).2.1 = (f j, g j, j).2.1
⊢ g i ≤ g j

Tactic:
h.le

Premises used: Eq.le
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h_1 : Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
h : (f i, g i, i).2.1 = (f j, g j, j).2.1
⊢ g i ≤ g j

Tactic:
exact h.le

Premises used: Eq.le
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
w : LinearOrder ι
hf : MonotoneOn f s
hg : MonotoneOn g s
⊢ MonovaryOn f g s

Tactic:
hf.monovaryOn hg

Premises used: MonotoneOn.monovaryOn
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
w : LinearOrder ι
hf : MonotoneOn f s
hg : MonotoneOn g s
⊢ MonovaryOn f g s

Tactic:
exact hf.monovaryOn hg

Premises used: MonotoneOn.monovaryOn
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
letI letI₁ letI₂ : MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
refine_1 :
  let this := linearOrderOfSTO (MonovaryOrder f g);
  ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), f i ≤ f j
refine_2 :
  let this := linearOrderOfSTO (MonovaryOrder f g);
  ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), g i ≤ g j
refine_3 : (∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s
refine_2₁ :
  let this := linearOrderOfSTO (MonovaryOrder f g);
  ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), g i ≤ g j
refine_3₁ refine_3₂ : (∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s

Tactic:
classical
  letI := linearOrderOfSTO (MonovaryOrder f g)
  refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
  · obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij <;> exact h.le
  · obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij
    · exact hfg.symm hi hj h
    obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h <;> exact h.le
  · rintro ⟨_, hf, hg⟩
    exact hf.monovaryOn hg
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
simp_rw :
  MonovaryOn (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) s ↔
    ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s
simp_rw₁ :
  (∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn (β := βᵒᵈ) ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) s) ↔
    ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s
⊢ AntivaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s

Tactic:
simp_rw [← monovaryOn_toDual_right, monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff]

Premises used: monovaryOn_iff_exists_monotoneOn, monovaryOn_toDual_right, monotoneOn_toDual_comp_iff
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
simp_rw :
  AntivaryOn (α := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) g s ↔
    ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s
simp_rw₁ :
  (∃ (x : LinearOrder ι), MonotoneOn (β := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) s ∧ AntitoneOn g s) ↔
    ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s

Tactic:
simp_rw [← antivaryOn_toDual_left, antivaryOn_iff_exists_monotoneOn_antitoneOn,
    monotoneOn_toDual_comp_iff]

Premises used: antivaryOn_toDual_left, antivaryOn_iff_exists_monotoneOn_antitoneOn, monotoneOn_toDual_comp_iff
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
simp_rw :
  MonovaryOn (α := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) g s ↔
    ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s
simp_rw₁ :
  (∃ (x : LinearOrder ι), MonotoneOn (β := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) s ∧ MonotoneOn g s) ↔
    ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s
⊢ AntivaryOn f g s ↔ ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s

Tactic:
simp_rw [← monovaryOn_toDual_left, monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff]

Premises used: monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff, monovaryOn_toDual_left
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
⊢ Monovary f g ↔ ∃ (x : LinearOrder ι), Monotone f ∧ Monotone g

Tactic:
simp [← monovaryOn_univ, monovaryOn_iff_exists_monotoneOn]

Premises used: monovaryOn_iff_exists_monotoneOn, monovaryOn_univ
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
⊢ Monovary f g ↔ ∃ (x : LinearOrder ι), Antitone f ∧ Antitone g

Tactic:
simp [← monovaryOn_univ, monovaryOn_iff_exists_antitoneOn]

Premises used: monovaryOn_univ, monovaryOn_iff_exists_antitoneOn
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
⊢ Antivary f g ↔ ∃ (x : LinearOrder ι), Monotone f ∧ Antitone g

Tactic:
simp [← antivaryOn_univ, antivaryOn_iff_exists_monotoneOn_antitoneOn]

Premises used: antivaryOn_univ, antivaryOn_iff_exists_monotoneOn_antitoneOn
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
⊢ Antivary f g ↔ ∃ (x : LinearOrder ι), Antitone f ∧ Monotone g

Tactic:
simp [← antivaryOn_univ, antivaryOn_iff_exists_antitoneOn_monotoneOn]

Premises used: antivaryOn_univ, antivaryOn_iff_exists_antitoneOn_monotoneOn
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
⊢ StrictMono f

Tactic:
StrictMonoOn.Iic_union_Ici (fun x hx y hy hxy => neg_lt_neg_iff.1 ?_) h₂

Premises used: neg_lt_neg_iff, StrictMonoOn.Iic_union_Ici, Iff.mp
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
refine :
  ∀ (x : G) (hx : Membership.mem (γ := Set G) (Iic 0) x) (y : G) (hy : Membership.mem (γ := Set G) (Iic 0) y)
    (hxy : x < y), -f y < -f x
⊢ StrictMono f

Tactic:
refine StrictMonoOn.Iic_union_Ici (fun x hx y hy hxy => neg_lt_neg_iff.1 ?_) h₂

Premises used: neg_lt_neg_iff, StrictMonoOn.Iic_union_Ici, Iff.mp
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : Membership.mem (γ := Set G) (Iic 0) x
y : G
hy : Membership.mem (γ := Set G) (Iic 0) y
hxy : x < y
rw : f (-y) < f (-x)
⊢ -f y < -f x

Tactic:
rw [← h₁, ← h₁]
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : Membership.mem (γ := Set G) (Iic 0) x
y : G
hy : Membership.mem (γ := Set G) (Iic 0) y
hxy : x < y
⊢ f (-y) < f (-x)

Tactic:
h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_lt_neg hxy)

Premises used: Iff.mpr, neg_lt_neg, neg_nonneg
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : Membership.mem (γ := Set G) (Iic 0) x
y : G
hy : Membership.mem (γ := Set G) (Iic 0) y
hxy : x < y
⊢ f (-y) < f (-x)

Tactic:
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_lt_neg hxy)

Premises used: Iff.mpr, neg_lt_neg, neg_nonneg
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictAntiOn f (Ici 0)
⊢ StrictAnti f

Tactic:
strictMono_of_odd_strictMonoOn_nonneg (H := Hᵒᵈ) h₁ h₂

Premises used: strictMono_of_odd_strictMonoOn_nonneg, StrictAnti
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
⊢ Monotone f

Tactic:
MonotoneOn.Iic_union_Ici (fun x hx y hy hxy => neg_le_neg_iff.1 ?_) h₂

Premises used: MonotoneOn.Iic_union_Ici, Iff.mp, neg_le_neg_iff
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
refine :
  ∀ (x : G) (hx : Membership.mem (γ := Set G) (Iic 0) x) (y : G) (hy : Membership.mem (γ := Set G) (Iic 0) y)
    (hxy : x ≤ y), -f y ≤ -f x
⊢ Monotone f

Tactic:
refine MonotoneOn.Iic_union_Ici (fun x hx y hy hxy => neg_le_neg_iff.1 ?_) h₂

Premises used: MonotoneOn.Iic_union_Ici, Iff.mp, neg_le_neg_iff
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : Membership.mem (γ := Set G) (Iic 0) x
y : G
hy : Membership.mem (γ := Set G) (Iic 0) y
hxy : x ≤ y
rw : f (-y) ≤ f (-x)
⊢ -f y ≤ -f x

Tactic:
rw [← h₁, ← h₁]
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : Membership.mem (γ := Set G) (Iic 0) x
y : G
hy : Membership.mem (γ := Set G) (Iic 0) y
hxy : x ≤ y
⊢ f (-y) ≤ f (-x)

Tactic:
h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)

Premises used: Iff.mpr, neg_nonneg, neg_le_neg
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : Membership.mem (γ := Set G) (Iic 0) x
y : G
hy : Membership.mem (γ := Set G) (Iic 0) y
hxy : x ≤ y
⊢ f (-y) ≤ f (-x)

Tactic:
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)

Premises used: Iff.mpr, neg_nonneg, neg_le_neg
-- Module: Mathlib.Order.Monotone.Odd
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : AddCommGroup H
inst_4 : PartialOrder H
inst_5 : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : AntitoneOn f (Ici 0)
⊢ Antitone f

Tactic:
monotone_of_odd_of_monotoneOn_nonneg (H := Hᵒᵈ) h₁ h₂

Premises used: Antitone, monotone_of_odd_of_monotoneOn_nonneg
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hx : x ∈ s ∪ t
hxc : x ≤ c
inl : x ∈ s → x ∈ s
inr : x ∈ t → x ∈ s
⊢ x ∈ s

Tactic:
cases hx
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h : x ∈ s
⊢ x ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h : x ∈ t
inr : ∀ (hs : IsGreatest s x) (ht : IsLeast t x) (hxc : x ≤ x), x ∈ s
inr₁ : ∀ (h'x : x < c), x ∈ s
⊢ x ∈ s

Tactic:
rcases eq_or_lt_of_le hxc with (rfl | h'x)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
x : α
h : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s

Tactic:
hs.1

Premises used: And.left
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
x : α
h : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s

Tactic:
exact hs.1

Premises used: And.left
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h : x ∈ t
h'x : x < c
⊢ x ∈ t

Tactic:
assumption
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h : x ∈ t
h'x : x < c
⊢ x ∈ s

Tactic:
exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim

Premises used: lt_irrefl, False.elim, And.right, LT.lt.trans_le
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ ∀ x ∈ s ∪ t, x ≤ c → x ∈ s

Tactic:
have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s := by
    intro x hx hxc
    cases hx
    · assumption
    rcases eq_or_lt_of_le hxc with (rfl | h'x)
    · exact hs.1
    exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx_1 : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ t
⊢ x ∈ t

Tactic:
hx
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx_1 : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ t
⊢ x ∈ t

Tactic:
exact hx
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx_1 : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
inl : ∀ (hx : c ∈ s ∪ t) (hxc : c ≤ c) (hx : c ∈ s), c ∈ t
inr : ∀ (h'x : c < x), x ∈ t
⊢ x ∈ t

Tactic:
rcases eq_or_lt_of_le hxc with (rfl | h'x)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
hx_1 : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t

Tactic:
ht.1

Premises used: And.left
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
hx_1 : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t

Tactic:
exact ht.1

Premises used: And.left
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx_1 : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
h'x : c < x
⊢ x ∈ t

Tactic:
(lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim

Premises used: lt_irrefl, False.elim, And.right, LT.lt.trans_le
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx_1 : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
h'x : c < x
⊢ x ∈ t

Tactic:
exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim

Premises used: lt_irrefl, False.elim, And.right, LT.lt.trans_le
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx : x ∈ s ∪ t
hxc : c ≤ x
⊢ x ∈ t

Tactic:
match hx with
    | Or.inr hx => exact hx
    | Or.inl hx =>
      rcases eq_or_lt_of_le hxc with (rfl | h'x)
      · exact ht.1
      exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
⊢ ∀ x ∈ s ∪ t, c ≤ x → x ∈ t

Tactic:
have B : ∀ x, x ∈ s ∪ t → c ≤ x → x ∈ t := by
    intro x hx hxc
    match hx with
    | Or.inr hx => exact hx
    | Or.inl hx =>
      rcases eq_or_lt_of_le hxc with (rfl | h'x)
      · exact ht.1
      exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
-- Module: Mathlib.Order.Monotone.Union
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
inl : ∀ (hxc : x < c), f x < f y
inr : ∀ (hcx : c ≤ x), f x < f y
⊢ f x < f y

Tactic:
rcases lt_or_ge x c with (hxc | hcx)

Premises used: lt_or_ge