awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Antitone f
⊢ f (max a b) = min (f a) (f b)
have inl : ∀ (h : a ≤ b), f (max a b) = min (f a) (f b)
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Antitone f
inl : ∀ (h : a ≤ b), f (max a b) = min (f a) (f b)
⊢ f (max a b) = min (f a) (f b)
have inr : ∀ (h : b ≤ a), f (max a b) = min (f a) (f b)
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
inst : LinearOrder α
a b : α
⊢ min a b = a ∨ min a b = b
have inl : a ≤ b → min a b = a ∨ min a b = b
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
inst : LinearOrder α
a b : α
inl : a ≤ b → min a b = a ∨ min a b = b
⊢ min a b = a ∨ min a b = b
have inr : b ≤ a → min a b = a ∨ min a b = b
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : Subtype Q
⊢ Minimal (fun (x : Subtype Q) ↦ P (↑x : α)) x ↔ Minimal (P ⊓ Q) (↑x : α)
have obtain : ∀ (x : α) (hx : Q x),
  Minimal (fun (x : Subtype Q) ↦ P (↑x : α)) (Subtype.mk (p := Q) x hx) ↔
    Minimal (P ⊓ Q) (↑(Subtype.mk (p := Q) x hx) : α)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
⊢ Minimal (fun (x : Subtype Q) ↦ P (↑x : α)) (Subtype.mk (p := Q) x hx) ↔
    Minimal (P ⊓ Q) (↑(Subtype.mk (p := Q) x hx) : α)
have simp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
Tactic: simp only [Minimal, Subtype.forall, Subtype.mk_le_mk, Pi.inf_apply, inf_Prop_eq]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mp₁ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₁ mp₂ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mp₃ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → P x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₁ mp₂ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mp₃ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → P x
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mp₄ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → Q x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₁ mp₂ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mp₃ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → P x
mp₄ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → Q x
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mp₅ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₁ mp₂ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mp₃ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → P x
mp₄ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → Q x
mp₅ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mpr₁ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₁ mp₂ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mp₃ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → P x
mp₄ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → Q x
mp₅ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr₁ mpr₂ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mpr₃ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → P x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₁ mp₂ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mp₃ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → P x
mp₄ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → Q x
mp₅ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr₁ mpr₂ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mpr₃ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → P x
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mpr₄ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₁ mp₂ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mp₃ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → P x
mp₄ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → Q x
mp₅ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr₁ mpr₂ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mpr₃ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → P x
mpr₄ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₆ mp₇ mp₈ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr₅ mpr₆ mpr₇ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → ∀ (a : α), Q a → P a → a ≤ x → x ≤ a
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
have mp₉ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, y ≤ x → P y → Q y → x ≤ y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P : α → Prop
inst : LE α
x : Subtype P
⊢ Minimal (fun (x : Subtype P) ↦ True) x ↔ Minimal P (↑x : α)
have obtain : ∀ (x : α) (hx : P x),
  Minimal (fun (x : Subtype P) ↦ True) (Subtype.mk (p := P) x hx) ↔ Minimal P (↑(Subtype.mk (p := P) x hx) : α)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
h : Minimal (fun (x : α) ↦ P x ∨ Q x) x
⊢ Minimal P x ∨ Minimal Q x
have inl : ∀ (hmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ P x ∨ Q x) y → y ≤ x → x ≤ y) (h : P x), Minimal P x ∨ Minimal Q x
Tactic: obtain ⟨h | h, hmin⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
h : Minimal (fun (x : α) ↦ P x ∨ Q x) x
inl : ∀ (hmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ P x ∨ Q x) y → y ≤ x → x ≤ y) (h : P x), Minimal P x ∨ Minimal Q x
⊢ Minimal P x ∨ Minimal Q x
have inr : ∀ (hmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ P x ∨ Q x) y → y ≤ x → x ≤ y) (h : Q x), Minimal P x ∨ Minimal Q x
Tactic: obtain ⟨h | h, hmin⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun (x : α) ↦ P x ∧ Q x) x ↔ Minimal P x ∧ Q x
have simp_rw : Minimal (fun (x : α) ↦ P x) x → Q x
Tactic: simp_rw [and_iff_left_of_imp (fun x ↦ hPQ x), iff_self_and]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun (x : α) ↦ Q x ∧ P x) x ↔ Q x ∧ Minimal P x
have simp_rw : Q x ∧ Minimal P x ↔ Minimal (fun (x : α) ↦ Q x ∧ P x) x
Tactic: simp_rw [iff_comm, and_comm, minimal_and_iff_right_of_imp hPQ, and_comm]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
simp_rw : Q x ∧ Minimal P x ↔ Minimal (fun (x : α) ↦ Q x ∧ P x) x
⊢ Minimal (fun (x : α) ↦ Q x ∧ P x) x ↔ Q x ∧ Minimal P x
have simp_rw₁ : Q x ∧ Minimal P x ↔ Minimal (fun (x : α) ↦ P x ∧ Q x) x
Tactic: simp_rw [iff_comm, and_comm, minimal_and_iff_right_of_imp hPQ, and_comm]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
simp_rw : Q x ∧ Minimal P x ↔ Minimal (fun (x : α) ↦ Q x ∧ P x) x
simp_rw₁ : Q x ∧ Minimal P x ↔ Minimal (fun (x : α) ↦ P x ∧ Q x) x
⊢ Minimal (fun (x : α) ↦ Q x ∧ P x) x ↔ Q x ∧ Minimal P x
have simp_rw₂ : Q x ∧ Minimal P x ↔ Minimal P x ∧ Q x
Tactic: simp_rw [iff_comm, and_comm, minimal_and_iff_right_of_imp hPQ, and_comm]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P : α → Prop
x : α
inst : Preorder α
hx : P x
⊢ ¬Minimal P x ↔ ∃ (y : α), y < x ∧ P y
have simp_rw : (∃ (y : α), P y ∧ y ≤ x ∧ ¬x ≤ y) ↔ ∃ (y : α), y < x ∧ P y
Tactic: simp_rw [not_minimal_iff hx, lt_iff_le_not_ge, and_comm]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P : α → Prop
x : α
inst : Preorder α
hx : P x
simp_rw : (∃ (y : α), P y ∧ y ≤ x ∧ ¬x ≤ y) ↔ ∃ (y : α), y < x ∧ P y
⊢ ¬Minimal P x ↔ ∃ (y : α), y < x ∧ P y
have simp_rw₁ : (∃ (y : α), P y ∧ y ≤ x ∧ ¬x ≤ y) ↔ ∃ (y : α), (y ≤ x ∧ ¬x ≤ y) ∧ P y
Tactic: simp_rw [not_minimal_iff hx, lt_iff_le_not_ge, and_comm]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
⊢ MinimalFor Q f i
have refine : ∀ (j : ι) (hj : Q j) (hle : f j ≤ f i), f i ≤ f j
Tactic: refine ⟨h.prop, fun j hj hle ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f j ≤ f i
⊢ f i ≤ f j
have by_contra : ∀ (this : ¬f i ≤ f j), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
⊢ MaximalFor Q f i
have refine : ∀ (j : ι) (hj : Q j) (hle : f i ≤ f j), f j ≤ f i
Tactic: refine ⟨h.prop, fun j hj hle ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f i ≤ f j
⊢ f j ≤ f i
have by_contra : ∀ (this : ¬f j ≤ f i), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : WellFoundedLT α
P : α → Prop
a : α
ha : P a
⊢ ∃ (b : α), b ≤ a ∧ Minimal P b
have obtain : ∀ (b : α) (hbmin : ∀ ⦃y : α⦄, (fun (b : α) ↦ b ≤ a ∧ P b) y → y ≤ b → b ≤ y) (hba : b ≤ a) (hb : P b),
  ∃ (b : α), b ≤ a ∧ Minimal P b
Tactic: obtain ⟨b, ⟨hba, hb⟩, hbmin⟩ :=
    exists_minimal_of_wellFoundedLT (fun b ↦ b ≤ a ∧ P b) ⟨a, le_rfl, ha⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
⊢ Minimal P x ↔ Minimal Q x
have refine_1 : ∀ (h' : Minimal P x), Q x
Tactic: refine ⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩,
    fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
refine_1 : ∀ (h' : Minimal P x), Q x
⊢ Minimal P x ↔ Minimal Q x
have refine_2 : ∀ (h' : Minimal Q x) (y : α) (hy : P y) (hyx : y ≤ x), x ≤ y
Tactic: refine ⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩,
    fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
h' : Minimal P x
⊢ Q x
have refine_1 : ∀ (y : α) (hyx : y ≤ x) (hy : Q y), Q x
Tactic: obtain ⟨y, hyx, hy⟩ := h h'.prop
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
⊢ x ≤ y
have refine_2 : ∀ (z : α) (hzy : z ≤ y) (hz : Q z), x ≤ y
Tactic: obtain ⟨z, hzy, hz⟩ := h hy
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), ¬x ∈ s → ¬P (insert x s)
have simp : Maximal P s ↔ P s ∧ ∀ (x : α), P (insert x s) → x ∈ s
Tactic: simp only [not_imp_not]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
x : α
s : Set α
inst : Preorder α
h : s.Subsingleton
⊢ Minimal (fun (x : α) ↦ x ∈ s) x ↔ x ∈ s
have inl : ∀ (h : Set.Subsingleton.{u_2} (α := α) ∅),
  Minimal (fun (x : α) ↦ Membership.mem (γ := Set α) ∅ x) x ↔ Membership.mem (γ := Set α) ∅ x
Tactic: obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
x : α
s : Set α
inst : Preorder α
h : s.Subsingleton
inl :
  ∀ (h : Set.Subsingleton.{u_2} (α := α) ∅),
    Minimal (fun (x : α) ↦ Membership.mem (γ := Set α) ∅ x) x ↔ Membership.mem (γ := Set α) ∅ x
⊢ Minimal (fun (x : α) ↦ x ∈ s) x ↔ x ∈ s
have inr : ∀ (x_1 : α) (h : Set.Subsingleton (α := α) {x_1}),
  Minimal (fun (x : α) ↦ Membership.mem (γ := Set α) {x_1} x) x ↔ Membership.mem (γ := Set α) {x_1} x
Tactic: obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
⊢ Minimal (fun (x : β) ↦ x ∈ f '' s) (f x)
have refine : ∀ ⦃y : β⦄, (fun (x : β) ↦ x ∈ f '' s) y → y ≤ f x → f x ≤ y
Tactic: refine ⟨mem_image_of_mem f hx.prop, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
y : α
hy : y ∈ s
⊢ f y ≤ f x → f x ≤ f y
have rw : y ≤ x → x ≤ y
Tactic: rw [hf hx.prop hy, hf hy hx.prop]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
a : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
⊢ Minimal (fun (x : β) ↦ x ∈ f '' s) (f a) ↔ Minimal (fun (x : α) ↦ x ∈ s) a
have refine : ∀ (h : Minimal (fun (x : β) ↦ x ∈ f '' s) (f a)) (y : α) (hys : (fun (x : α) ↦ x ∈ s) y), y ≤ a → a ≤ y
Tactic: refine ⟨fun h ↦ ⟨ha, fun y hys ↦ ?_⟩, minimal_mem_image_monotone hf⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
a : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun (x : β) ↦ x ∈ f '' s) (f a)
y : α
hys : (fun (x : α) ↦ x ∈ s) y
⊢ y ≤ a → a ≤ y
have rw : f y ≤ f a → f a ≤ f y
Tactic: rw [← hf ha hys, ← hf hys ha]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
⊢ f '' {x : α | Minimal P x} = {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x}
have refine_1 : ∀ (x : β),
  x ∈ f '' {x : α | Minimal P x} →
    Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} x
Tactic: refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
refine_1 :
  ∀ (x : β),
    x ∈ f '' {x : α | Minimal P x} →
      Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} x
⊢ f '' {x : α | Minimal P x} = {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x}
have refine_2 : ∀ (x : β) (h : Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} x),
  x ∈ f '' {x : α | Minimal P x}
Tactic: refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
h : Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} x
⊢ x ∈ f '' {x : α | Minimal P x}
have refine_2 : ∀ (y : α) (hy : P y)
  (h : Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} (f y)),
  f y ∈ f '' {x : α | Minimal P x}
Tactic: obtain ⟨y, hy, rfl⟩ := (mem_setOf_eq ▸ h).prop
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
⊢ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
have refine_1 : ∀
  (h :
    Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) x : β))
  (y : α) (hy : (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) y), y ≤ x → x ≤ y
Tactic: refine ⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, mem_range_self x⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
refine_1 :
  ∀
    (h :
      Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
        ((f : (a : α) → β) x : β))
    (y : α) (hy : (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) y), y ≤ x → x ≤ y
⊢ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
have refine_2 : ∀ (h : Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x) ⦃y : β⦄,
  (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) y →
    y ≤ (f : (a : α) → β) x → (f : (a : α) → β) x ≤ y
Tactic: refine ⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, mem_range_self x⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
h :
  Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) x : β)
y : α
hy : (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) y
⊢ y ≤ x → x ≤ y
have refine_1 : LE.le.{u_3} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) x : β) →
  LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
Tactic: rw [← f.le_iff_le, ← f.le_iff_le]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
y : α
hyt : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) x : β) →
    LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
have refine_2 : y ≤ x → x ≤ y
Tactic: simp_rw [f.le_iff_le]
-- Lean 4 proof step from Mathlib.Order.Minimal (goal)
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
have rw : Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
  Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) x : β)
Tactic: rw [← f.minimal_apply_mem_inter_range_iff, inter_eq_self_of_subset_left ht]