awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
⊢ I = closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) x}
have h : ∀ (x : M),
  x ∈ I ↔
    Membership.mem (γ := SubMulAction M M)
      (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) x}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
⊢ x ∈ I ↔
    Membership.mem (γ := SubMulAction M M)
      (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) x}) x
have h : x ∈ I ↔ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
Tactic: simp only [mem_closure'', SetLike.setOf_mem_eq, SetLike.mem_coe, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
⊢ x ∈ I ↔ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
have h : x ∈ I → ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
h : x ∈ I → ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
⊢ x ∈ I ↔ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
have h₁ : (∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x) → x ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
hx : x ∈ I
⊢ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
have h : ∀ (z : M) (hz : z ≤ x) (hz' : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z),
  ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
Tactic: rcases hpwo.exists_le_minimal hx with ⟨z, hz, hz'⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
hx : x ∈ I
z : M
hz : z ≤ x
hz' : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z
⊢ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
have hz₁ : ∃ (c : M), x = c * z
Tactic: rw [le_iff_exists_mul'] at hz
Cleared hypotheses: hz, hz'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
hx : x ∈ I
z : M
hz : ∃ (c : M), x = c * z
hz' : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z
⊢ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
have h : ∀ (y : M) (hx : y * z ∈ I), ∃ (y_1 : M) (z_1 : M), Minimal (fun (x : M) ↦ x ∈ I) z_1 ∧ y_1 * z_1 = y * z
Tactic: rcases hz with ⟨y, rfl⟩
Cleared hypotheses: x, hx, hz
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
y z : M
hz : Minimal (fun (x : M) ↦ x ∈ I) z
⊢ y * z ∈ I
have h : z ∈ I
Tactic: apply SubMulAction.smul_mem
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
⊢ WellFoundedGT.{u_1} (SemigroupIdeal M)
have rw : ∀ (a : ℕ →o SemigroupIdeal M),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := SemigroupIdeal M) ((a : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
          ((a : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
Tactic: rw [wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
          ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
have rcases : ∀ (s : Finset M)
  (hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
          ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
Tactic: rcases fg_iff.1 (fg_of_wellQuasiOrderedLE (⨆ i, f i)) with ⟨s, hI⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))
x : M
hx : x ∈ s
⊢ ∃ (i : ℕ), Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) i : SemigroupIdeal M) x
have hx₁ : x ∈ (↑(closure (↑s : Set M)) : Set M)
Tactic: apply subset_closure (s := (s : Set M)) at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
          ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
have hs : ∀ x ∈ s, ∃ (i : ℕ), Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) i : SemigroupIdeal M) x
Tactic: have hs : ∀ x ∈ s, ∃ i, x ∈ f i := by
    intro x hx
    apply subset_closure (s := (s : Set M)) at hx
    simpa [← hI] using hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))
hs :
  ∀ x ∈ s, ∃ (i : ℕ), Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) i : SemigroupIdeal M) x
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
          ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
have choose! : ∀ (g : (x : M) → ℕ)
  (hg : ∀ x ∈ s, Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) (g x) : SemigroupIdeal M) x),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
          ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
Tactic: choose! g hg using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))
g : (x : M) → ℕ
hg : ∀ x ∈ s, Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) (g x) : SemigroupIdeal M) x
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
          ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
have exists : ∀ (m : ℕ),
  s.sup g ≤ m →
    Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M)
      ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
Tactic: exists s.sup g
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))
g : (x : M) → ℕ
hg : ∀ x ∈ s, Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) (g x) : SemigroupIdeal M) x
n : ℕ
hn : s.sup g ≤ n
⊢ Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M)
    ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
have apply : LE.le (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
  ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M)
Tactic: apply (f.mono hn).antisymm
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))
g : (x : M) → ℕ
hg : ∀ x ∈ s, Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) (g x) : SemigroupIdeal M) x
n : ℕ
hn : s.sup g ≤ n
⊢ LE.le (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
    ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M)
have apply : LE.le (α := SemigroupIdeal M) (iSup (ι := ℕ) (⇑f : (a : ℕ) → SemigroupIdeal M) : SemigroupIdeal M)
  ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M)
Tactic: apply (le_iSup f n).trans
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))
g : (x : M) → ℕ
hg : ∀ x ∈ s, Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) (g x) : SemigroupIdeal M) x
n : ℕ
hn : s.sup g ≤ n
x : M
hx : Membership.mem (γ := SubMulAction M M) (iSup (ι := ℕ) (⇑f : (a : ℕ) → SemigroupIdeal M)) x
⊢ Membership.mem (γ := SubMulAction M M) ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M) x
have hx₁ : ∃ (y : M), ∃ z ∈ (↑s : Set M), y * z = x
Tactic: rw [hI, mem_closure''] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))
g : (x : M) → ℕ
hg : ∀ x ∈ s, Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) (g x) : SemigroupIdeal M) x
n : ℕ
hn : s.sup g ≤ n
x : M
hx : ∃ (y : M), ∃ z ∈ (↑s : Set M), y * z = x
⊢ Membership.mem (γ := SubMulAction M M) ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M) x
have rcases : ∀ (y z : M) (hz : z ∈ (↑s : Set M)),
  Membership.mem (γ := SubMulAction M M) ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M) (y * z)
Tactic: rcases hx with ⟨y, z, hz, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : One M
inst_1 : ConditionallyCompleteLattice M
inst_2 : Nonempty ι
f : ι → α → M
⊢ Subset.{u_2} (α := Set α) (mulSupport.{u_2, u_3} (M := M) fun (x : α) ↦ ⨆ (i : ι), f i x)
    (⋃ (i : ι), mulSupport (f i))
have simp : ∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → Eq.{u_3 + 1} (α := M) (⨆ (i : ι), f i x) 1
Tactic: simp only [mulSupport_subset_iff', mem_iUnion, not_exists, notMem_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : LE M
inst_1 : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
⊢ s.mulIndicator f a ≤ y
have pos : ∀ (ha : a ∈ s), s.mulIndicator f a ≤ y
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : LE M
inst_1 : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
pos : ∀ (ha : a ∈ s), s.mulIndicator f a ≤ y
⊢ s.mulIndicator f a ≤ y
have neg : ∀ (ha : a ∉ s), s.mulIndicator f a ≤ y
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
⊢ s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
have simp_rw : (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
Tactic: simp_rw [indicator_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
⊢ (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
have pos : a ∈ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → f a ≤ f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
pos : a ∈ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → f a ≤ f a
⊢ (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
have neg : a ∈ s → a ∉ {a : α | 0 ≤ f a} → f a ≤ 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
pos : a ∈ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → f a ≤ f a
neg : a ∈ s → a ∉ {a : α | 0 ≤ f a} → f a ≤ 0
⊢ (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
have pos₁ : a ∉ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → 0 ≤ f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
pos : a ∈ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → f a ≤ f a
neg : a ∈ s → a ∉ {a : α | 0 ≤ f a} → f a ≤ 0
pos₁ : a ∉ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → 0 ≤ f a
⊢ (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
have neg₁ : a ∉ s → a ∉ {a : α | 0 ≤ f a} → LE.le.{u_3} (α := M) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
simp_rw simp_rw₁ : s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
⊢ s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
have simp_rw₂ : (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
Tactic: classical
  simp_rw [indicator_apply]
  split_ifs
  exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
simp_rw simp_rw₁ : s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
simp_rw₂ : (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
⊢ s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
have pos : a ∈ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → f a ≤ f a
Tactic: classical
  simp_rw [indicator_apply]
  split_ifs
  exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
simp_rw simp_rw₁ : s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
simp_rw₂ : (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
pos : a ∈ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → f a ≤ f a
⊢ s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
have neg : a ∈ s → a ∉ {a : α | 0 ≤ f a} → f a ≤ 0
Tactic: classical
  simp_rw [indicator_apply]
  split_ifs
  exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
simp_rw simp_rw₁ : s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
simp_rw₂ : (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
pos : a ∈ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → f a ≤ f a
neg : a ∈ s → a ∉ {a : α | 0 ≤ f a} → f a ≤ 0
⊢ s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
have pos₁ : a ∉ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → 0 ≤ f a
Tactic: classical
  simp_rw [indicator_apply]
  split_ifs
  exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
simp_rw simp_rw₁ : s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
simp_rw₂ : (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0
pos : a ∈ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → f a ≤ f a
neg : a ∈ s → a ∉ {a : α | 0 ≤ f a} → f a ≤ 0
pos₁ : a ∉ s → Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a → 0 ≤ f a
⊢ s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a
have neg₁ : a ∉ s → a ∉ {a : α | 0 ≤ f a} → LE.le.{u_3} (α := M) 0 0
Tactic: classical
  simp_rw [indicator_apply]
  split_ifs
  exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x
have pos : ∀ (hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x),
  mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x
Tactic: by_cases hx : x ∈ ⋃ i, s i
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
pos :
  ∀ (hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x),
    mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x
have neg : ∀ (hx : x ∉ ⋃ (i : ι), s i), mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x
Tactic: by_cases hx : x ∈ ⋃ i, s i
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x
have pos : f x = ⨆ (i : ι), (s i).mulIndicator f x
Tactic: rw [mulIndicator_of_mem hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
⊢ f x = ⨆ (i : ι), (s i).mulIndicator f x
have hx₁ : ∃ (i : ι), x ∈ s i
Tactic: rw [mem_iUnion] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : ∃ (i : ι), x ∈ s i
⊢ f x = ⨆ (i : ι), (s i).mulIndicator f x
have pos : f x ≤ ⨆ (i : ι), (s i).mulIndicator f x
Tactic: refine le_antisymm ?_ (iSup_le fun i ↦ mulIndicator_le_self' (fun x _ ↦ h1 ▸ bot_le) x)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : ∃ (i : ι), x ∈ s i
⊢ f x ≤ ⨆ (i : ι), (s i).mulIndicator f x
have pos : ∀ (i : ι) (hi : x ∈ s i), f x ≤ ⨆ (i : ι), (s i).mulIndicator f x
Tactic: rcases hx with ⟨i, hi⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ (i : ι), s i
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x
have neg : Eq.{u_3 + 1} (α := M) 1 (⨆ (i : ι), (s i).mulIndicator f x)
Tactic: rw [mulIndicator_of_notMem hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ (i : ι), s i
⊢ Eq.{u_3 + 1} (α := M) 1 (⨆ (i : ι), (s i).mulIndicator f x)
have hx₁ : ∀ (x_1 : ι), x ∉ s x_1
Tactic: simp only [mem_iUnion, not_exists] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
inst_2 : Nonempty ι
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
⊢ mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x
have pos : ∀ (hx : Membership.mem (γ := Set α) (⋂ (i : ι), s i) x),
  mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x
Tactic: by_cases hx : x ∈ ⋂ i, s i
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
inst_2 : Nonempty ι
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
pos :
  ∀ (hx : Membership.mem (γ := Set α) (⋂ (i : ι), s i) x),
    mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x
⊢ mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x
have neg : ∀ (hx : x ∉ ⋂ (i : ι), s i), mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x
Tactic: by_cases hx : x ∈ ⋂ i, s i
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
inst_2 : Nonempty ι
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ (i : ι), s i
⊢ mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x
have neg : Eq.{u_3 + 1} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)
Tactic: rw [mulIndicator_of_notMem hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
inst_2 : Nonempty ι
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ (i : ι), s i
⊢ Eq.{u_3 + 1} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)
have hx₁ : ∃ (x_1 : ι), x ∉ s x_1
Tactic: simp only [mem_iInter, not_forall] at hx
Cleared hypotheses: hx