awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Ideal
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 ∈ (↑(closure (↑s : Set M)) : Set M)
⊢ ∃ (i : ℕ), Membership.mem (γ := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) i : SemigroupIdeal M) x

Tactic:
simpa [← hI] using hx
-- Module: Mathlib.Algebra.Order.Group.Ideal
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 ∈ 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
-- Module: Mathlib.Algebra.Order.Group.Ideal
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
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)
⊢ ∃ (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
-- Module: Mathlib.Algebra.Order.Group.Ideal
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
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)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
          ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)

Tactic:
exists s.sup g

Premises used: Finset.sup
-- Module: Mathlib.Algebra.Order.Group.Ideal
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
apply :
  LE.le (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
    ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M)
⊢ Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M)
    ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)

Tactic:
apply (f.mono hn).antisymm

Premises used: LE.le.antisymm, OrderHom.mono
-- Module: Mathlib.Algebra.Order.Group.Ideal
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
apply :
  LE.le (α := SemigroupIdeal M) (iSup (ι := ℕ) (⇑f : (a : ℕ) → SemigroupIdeal M) : SemigroupIdeal M)
    ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M)
⊢ LE.le (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
    ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M)

Tactic:
apply (le_iSup f n).trans

Premises used: le_iSup, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Group.Ideal
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
⊢ ∃ (y : M), ∃ z ∈ (↑s : Set M), y * z = x

Tactic:
rw [hI, mem_closure''] at hx

Premises used: SemigroupIdeal.mem_closure''
-- Module: Mathlib.Algebra.Order.Group.Ideal
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
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)
⊢ Membership.mem (γ := SubMulAction M M) ((f : (a : ℕ) → SemigroupIdeal M) (s.sup g) : SemigroupIdeal M) x

Tactic:
rcases hx with ⟨y, z, hz, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Ideal
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
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:
SemigroupIdeal.mul_mem _ _ (f.mono (Finset.le_sup hz) (hg _ hz))

Premises used: Set.Mem, OrderHom.mono, SemigroupIdeal.mul_mem, Finset.le_sup
-- Module: Mathlib.Algebra.Order.Group.Ideal
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
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:
exact SemigroupIdeal.mul_mem _ _ (f.mono (Finset.le_sup hz) (hg _ hz))

Premises used: OrderHom.mono, SemigroupIdeal.mul_mem, Finset.le_sup
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : One M
inst_1 : SemilatticeSup M
f g : α → M
⊢ (mulSupport.{u_2, u_3} (M := M) fun (x : α) ↦ f x ⊔ g x) ⊆ mulSupport f ∪ mulSupport g

Tactic:
mulSupport_binop_subset (· ⊔ ·) (sup_idem _) f g

Premises used: Function.mulSupport_binop_subset, sup_idem, Max.max
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : One M
inst_1 : SemilatticeInf M
f g : α → M
⊢ (mulSupport.{u_2, u_3} (M := M) fun (x : α) ↦ f x ⊓ g x) ⊆ mulSupport f ∪ mulSupport g

Tactic:
mulSupport_binop_subset (· ⊓ ·) (inf_idem _) f g

Premises used: Function.mulSupport_binop_subset, inf_idem, Min.min
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : One M
inst_1 : LinearOrder M
f g : α → M
⊢ (mulSupport.{u_2, u_3} (M := M) fun (x : α) ↦ max (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g

Tactic:
mulSupport_sup f g

Premises used: Function.mulSupport_sup
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : One M
inst_1 : LinearOrder M
f g : α → M
⊢ (mulSupport.{u_2, u_3} (M := M) fun (x : α) ↦ min (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g

Tactic:
mulSupport_inf f g

Premises used: Function.mulSupport_inf
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : One M
inst_1 : ConditionallyCompleteLattice M
inst_2 : Nonempty ι
f : ι → α → M
simp : ∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → Eq.{u_3 + 1} (α := M) (⨆ (i : ι), f i x) 1
⊢ Subset.{u_2} (α := Set α) (mulSupport.{u_2, u_3} (M := M) fun (x : α) ↦ ⨆ (i : ι), f i x)
    (⋃ (i : ι), mulSupport (f i))

Tactic:
simp only [mulSupport_subset_iff', mem_iUnion, not_exists, notMem_mulSupport]

Premises used: Set.mem_iUnion, Function.mulSupport_subset_iff', not_exists, Function.notMem_mulSupport
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : One M
inst_1 : ConditionallyCompleteLattice M
inst_2 : Nonempty ι
f : ι → α → M
x : α
hx : ∀ (x_1 : ι), f x_1 x = 1
⊢ Eq.{u_3 + 1} (α := M) (⨆ (i : ι), f i x) 1

Tactic:
simp only [hx, ciSup_const]

Premises used: ciSup_const
-- Module: Mathlib.Algebra.Order.Group.Indicator
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))

Tactic:
mulSupport_iSup (M := Mᵒᵈ) f

Premises used: iInf, Function.mulSupport_iSup, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
neg : ∀ (ha : a ∉ s), s.mulIndicator f a ≤ y
⊢ s.mulIndicator f a ≤ y

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
ha : a ∈ s
⊢ s.mulIndicator f a ≤ y

Tactic:
simpa [ha] using hfg ha
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
ha : a ∉ s
⊢ s.mulIndicator f a ≤ y

Tactic:
simpa [ha] using hg ha
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : LE M
inst_1 : One M
s : Set α
f g : α → M
hfg : ∀ a ∈ s, f a ≤ g a
hg : ∀ a ∉ s, 1 ≤ g a
⊢ s.mulIndicator f ≤ g

Tactic:
fun _ ↦ mulIndicator_apply_le' (hfg _) (hg _)

Premises used: Set.mulIndicator_apply_le'
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : LE M
inst_1 : One M
s : Set α
g : α → M
a : α
y : M
hfg : a ∈ s → y ≤ g a
hf : a ∉ s → y ≤ 1
⊢ y ≤ s.mulIndicator g a

Tactic:
mulIndicator_apply_le' (M := Mᵒᵈ) hfg hf

Premises used: Set.mulIndicator_apply_le', OrderDual
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : LE M
inst_1 : One M
s : Set α
f g : α → M
hfg : ∀ a ∈ s, f a ≤ g a
hf : ∀ a ∉ s, f a ≤ 1
⊢ f ≤ s.mulIndicator g

Tactic:
fun _ ↦ le_mulIndicator_apply (hfg _) (hf _)

Premises used: Set.le_mulIndicator_apply
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s : Set α
f : α → M
a : α
h : a ∈ s → 1 ≤ f a
⊢ 1 ≤ s.mulIndicator f a

Tactic:
le_mulIndicator_apply h fun _ ↦ le_rfl

Premises used: le_rfl, Set.le_mulIndicator_apply
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s : Set α
f : α → M
h : ∀ a ∈ s, 1 ≤ f a
a : α
⊢ 1 ≤ s.mulIndicator f a

Tactic:
one_le_mulIndicator_apply (h a)

Premises used: Set.one_le_mulIndicator_apply
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s : Set α
f : α → M
a : α
h : a ∈ s → f a ≤ 1
⊢ s.mulIndicator f a ≤ 1

Tactic:
mulIndicator_apply_le' h fun _ ↦ le_rfl

Premises used: le_rfl, Set.mulIndicator_apply_le'
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s : Set α
f : α → M
h : ∀ a ∈ s, f a ≤ 1
a : α
⊢ s.mulIndicator f a ≤ 1

Tactic:
mulIndicator_apply_le_one (h a)

Premises used: Set.mulIndicator_apply_le_one
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s : Set α
f g : α → M
a : α
h : a ∈ s → f a ≤ g a
⊢ s.mulIndicator f a ≤ s.mulIndicator g a

Tactic:
mulIndicator_rel_mulIndicator le_rfl h

Premises used: le_rfl, Set.mulIndicator_rel_mulIndicator
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s : Set α
f g : α → M
a : α
h : f a ≤ g a
⊢ s.mulIndicator f a ≤ s.mulIndicator g a

Tactic:
mulIndicator_rel_mulIndicator le_rfl fun _ ↦ h

Premises used: le_rfl, Set.mulIndicator_rel_mulIndicator
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s : Set α
f g : α → M
h : f ≤ g
⊢ s.mulIndicator f ≤ s.mulIndicator g

Tactic:
fun _ ↦ mulIndicator_le_mulIndicator (h _)

Premises used: Set.mulIndicator_le_mulIndicator
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s t : Set α
f : α → M
a : α
h : s ⊆ t
hf : 1 ≤ f a
⊢ s.mulIndicator f a ≤ t.mulIndicator f a

Tactic:
mulIndicator_apply_le'
    (fun ha ↦ le_mulIndicator_apply (fun _ ↦ le_rfl) fun hat ↦ (hat <| h ha).elim) fun _ ↦
    one_le_mulIndicator_apply fun _ ↦ hf

Premises used: le_rfl, False.elim, Set.le_mulIndicator_apply, Set.mulIndicator_apply_le', Set.one_le_mulIndicator_apply
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s t : Set α
f : α → M
h : s ⊆ t
hf : 1 ≤ f
⊢ s.mulIndicator f ≤ t.mulIndicator f

Tactic:
fun _ ↦ mulIndicator_le_mulIndicator_apply_of_subset h (hf _)

Premises used: Set.mulIndicator_le_mulIndicator_apply_of_subset
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Preorder M
inst_1 : One M
s : Set α
f : α → M
hf : ∀ x ∉ s, 1 ≤ f x
⊢ s.mulIndicator f ≤ f

Tactic:
mulIndicator_le' (fun _ _ ↦ le_rfl) hf

Premises used: le_rfl, Set.mulIndicator_le'
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
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

Tactic:
simp_rw [indicator_apply]

Premises used: Set.indicator_apply
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
neg₁ : a ∉ s → a ∉ {a : α | 0 ≤ f a} → LE.le.{u_3} (α := M) 0 0
⊢ (if a ∈ s then f a else 0) ≤ if Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a then f a else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
h : a ∈ s
h_1 : Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a
⊢ f a ≤ f a

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
h : a ∈ s
h_1 : a ∉ {a : α | 0 ≤ f a}
⊢ f a ≤ 0

Tactic:
(not_le.1 ‹_›).le

Premises used: not_le, LT.lt.le, Iff.mp
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
h : a ∉ s
h_1 : a ∉ {a : α | 0 ≤ f a}
⊢ LE.le.{u_3} (α := M) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
a : α
h : a ∈ s
h_1 : Membership.mem (γ := Set α) {a : α | 0 ≤ f a} a
⊢ f a ≤ f a

Tactic:
exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]

Premises used: not_le, le_rfl, LT.lt.le, Iff.mp
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
neg₁ : a ∉ s → a ∉ {a : α | 0 ≤ f a} → LE.le.{u_3} (α := M) 0 0
⊢ s.indicator f a ≤ indicator {a : α | 0 ≤ f a} f a

Tactic:
classical
  simp_rw [indicator_apply]
  split_ifs
  exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]

Premises used: not_le, Set.indicator_apply, le_rfl, LT.lt.le, Iff.mp
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Zero M
inst_1 : LinearOrder M
s : Set α
f : α → M
⊢ indicator {a : α | f a ≤ 0} f ≤ s.indicator f

Tactic:
indicator_le_indicator_nonneg (M := Mᵒᵈ) _ _

Premises used: Set.indicator_le_indicator_nonneg, setOf, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
neg : ∀ (hx : x ∉ ⋃ (i : ι), s i), mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x

Tactic:
by_cases hx : x ∈ ⋃ i, s i
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
pos : f x = ⨆ (i : ι), (s i).mulIndicator f x
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x

Tactic:
rw [mulIndicator_of_mem hx]

Premises used: Set.mulIndicator_of_mem
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
⊢ ∃ (i : ι), x ∈ s i

Tactic:
rw [mem_iUnion] at hx

Premises used: Set.mem_iUnion
-- Module: Mathlib.Algebra.Order.Group.Indicator
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

Tactic:
le_antisymm ?_ (iSup_le fun i ↦ mulIndicator_le_self' (fun x _ ↦ h1 ▸ bot_le) x)

Premises used: Set.mulIndicator_le_self', le_antisymm, iSup_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
pos : f x ≤ ⨆ (i : ι), (s i).mulIndicator f x
⊢ 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)

Premises used: Set.mulIndicator_le_self', le_antisymm, iSup_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
pos : ∀ (i : ι) (hi : x ∈ s i), f x ≤ ⨆ (i : ι), (s i).mulIndicator f x
⊢ f x ≤ ⨆ (i : ι), (s i).mulIndicator f x

Tactic:
rcases hx with ⟨i, hi⟩
-- Module: Mathlib.Algebra.Order.Group.Indicator
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 : α
i : ι
hi : x ∈ s i
⊢ f x ≤ ⨆ (i : ι), (s i).mulIndicator f x

Tactic:
le_iSup_of_le i (ge_of_eq <| mulIndicator_of_mem hi _)

Premises used: ge_of_eq, le_iSup_of_le, Set.mulIndicator_of_mem
-- Module: Mathlib.Algebra.Order.Group.Indicator
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 : α
i : ι
hi : x ∈ s i
⊢ f x ≤ ⨆ (i : ι), (s i).mulIndicator f x

Tactic:
exact le_iSup_of_le i (ge_of_eq <| mulIndicator_of_mem hi _)

Premises used: ge_of_eq, le_iSup_of_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
neg : Eq.{u_3 + 1} (α := M) 1 (⨆ (i : ι), (s i).mulIndicator f x)
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), (s i).mulIndicator f x

Tactic:
rw [mulIndicator_of_notMem hx]

Premises used: Set.mulIndicator_of_notMem
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
⊢ ∀ (x_1 : ι), x ∉ s x_1

Tactic:
simp only [mem_iUnion, not_exists] at hx

Premises used: Set.mem_iUnion, not_exists
-- Module: Mathlib.Algebra.Order.Group.Indicator
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_1 : ι), x ∉ s x_1
⊢ Eq.{u_3 + 1} (α := M) 1 (⨆ (i : ι), (s i).mulIndicator f x)

Tactic:
simp [hx, ← h1]
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
neg : ∀ (hx : x ∉ ⋂ (i : ι), s i), mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x
⊢ mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x

Tactic:
by_cases hx : x ∈ ⋂ i, s i
-- Module: Mathlib.Algebra.Order.Group.Indicator
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 : Membership.mem (γ := Set α) (⋂ (i : ι), s i) x
⊢ mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Group.Indicator
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
neg : Eq.{u_3 + 1} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)
⊢ mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), (s i).mulIndicator f x

Tactic:
rw [mulIndicator_of_notMem hx]

Premises used: Set.mulIndicator_of_notMem