mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, IsCompl ⟨x, hx⟩ b

Tactic:
Set.Iic.isCompl_iff

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, Disjoint x ↑b ∧ x ⊔ ↑b = a
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Tactic:
refine and_congr_right fun _ ↦ forall_congr' fun H ↦ ?_

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K < H → ¬H < L ↔ ∀ (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
⊢ a ⊆ s.biUnion g → ∀ ⦃i : ι⦄, i ∈ s.biUnion g → i ∉ a → Disjoint (f i) (a.sup f)

Tactic:
ha

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
⊢ ∀ ⦃i : ι⦄, i ∈ s.biUnion g → i ∉ a → Disjoint (f i) (a.sup f)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case smul
R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h✝ : ∀ y ∈ s, Commute y x
y : A
a✝ : R
x✝ : A
hx✝ : x✝ ∈ span R s
h : Commute x✝ x
⊢ Commute (a✝ • x✝) x

Tactic:
exact h.smul_left _

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
obtain (rfl | ⟨d, hd⟩) := eq_bot_or_exists_atom_le a'

Goal state after:
case inl
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
ha'b : ⊥ ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨⊥, ha'b⟩
⊢ ∃ x, a ⋖ x ∧ x ≤ b

case inr
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ ∃ x, a ⋖ x ∧ x ≤ b
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ {0, 1, 2}.sup f = f 0 ⊔ f 1 ⊔ f 2

Tactic:
simp [sup_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
this : ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩
⊢ f = g

Tactic:
by
      ext ⟨x, hx⟩
      exact this x hx

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
⊢ (⨆ i, p i).toAddSubmonoid = ⨆ i, (p i).toAddSubmonoid

Tactic:
refine le_antisymm (fun x => ?_) (iSup_le fun i => toAddSubmonoid_mono <| le_iSup _ i)
  simp_rw [iSup_eq_span, AddSubmonoid.iSup_eq_closure, mem_toAddSubmonoid, coe_toAddSubmonoid]
  intro hx
  refine Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_)
    (fun r x _ hx => ?_) hx
  · exact AddSubmonoid.subset_closure hx
  · exact AddSubmonoid.zero_mem _
  · exact AddSubmonoid.add_mem _ hx hy
  · refine AddSubmonoid.closure_induction ?_ ?_ ?_ hx
    · rintro x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩
      apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)
      exact smul_mem _ r hix
    · rw [smul_zero]
      exact AddSubmonoid.zero_mem _
    · intro x y _ _ hx hy
      rw [smul_add]
      exact AddSubmonoid.add_mem _ hx hy

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : ¬1 < s.card
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
by_cases hcard0 : s.card = 0

Goal state after:
case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : ¬1 < s.card
hcard0 : s.card = 0
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

case neg
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : ¬1 < s.card
hcard0 : ¬s.card = 0
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
s : Multiset M₀
h : 0 ∈ s
⊢ s.prod = 0

Tactic:
rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩; simp [hs', Multiset.prod_cons]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: R : Type u_4
inst✝ : NonUnitalSemiring R
s✝ : Multiset R
a x : R
s : Multiset R
ih : (∀ (x : R), x ∈ s → a ∣ x) → a ∣ s.sum
h : ∀ (x_1 : R), x_1 ∈ x ::ₘ s → a ∣ x_1
⊢ a ∣ (x ::ₘ s).sum

Tactic:
by
    rw [sum_cons]
    exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy ↦ h _ <| mem_cons.2 <| Or.inr hy)

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
⊢ a ∈ {a | a ≤ c ∧ IsAtom a} → a ≤ b ⊔ sSup s

Tactic:
ha

Goal state after:
case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
⊢ a ≤ b ⊔ sSup s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
⊢ IsAtom x ∧ x ≤ c

Tactic:
obtain hx | rfl := hx

Goal state after:
case inl
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s
⊢ IsAtom x ∧ x ≤ c

case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
x : α
ha : x ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
⊢ IsAtom x ∧ x ≤ c
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i

Tactic:
calc
    ∏ i ∈ s, (f i + g i) =
        ∏ i ∈ s, ∑ p ∈ ({True, False} : Finset Prop), if p then f i else g i := by simp
    _ = ∑ p ∈ (s.pi fun _ => {True, False} : Finset (∀ a ∈ s, Prop)),
          ∏ a ∈ s.attach, if p a.1 a.2 then f a.1 else g a.1 := prod_sum _ _ _
    _ = ∑ t ∈ s.powerset, (∏ a ∈ t, f a) * ∏ a ∈ s \ t, g a :=
      sum_bij'
        (fun f _ ↦ {a ∈ s | ∃ h : a ∈ s, f a h})
        (fun t _ a _ => a ∈ t)
        (by simp)
        (by simp [Classical.em])
        (by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
        (by simp_rw [Finset.ext_iff, mem_filter, mem_powerset]; tauto)
        (fun a _ ↦ by
          simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
            Subtype.map_coe, id_eq, prod_attach]
          congr 2 with x
          simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
          tauto)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
⊢ (∀ x ∈ s, x < a) →
    ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j →
      ∏ i ∈ insert a s, (f i + g i) =
        ∏ i ∈ insert a s, f i +
          ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j

Tactic:
ha

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
⊢ ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j →
    ∏ i ∈ insert a s, (f i + g i) =
      ∏ i ∈ insert a s, f i +
        ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case inl
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
z : V
hz : z ∈ s
hyq : 0 • x + z ∈ q
hyp : 0 • x + z ∉ s
⊢ K ∙ x ⊔ s ≤ q

pp: case inr
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ K ∙ x ⊔ s ≤ q

Tactic:
· simp [hz] at hyp

Goal state after:
case inr
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ K ∙ x ⊔ s ≤ q
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (Function.support g ⊆ ↑s ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ g = ⇑(indicator s f) ↔ Function.support g ⊆ ↑s ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i

Tactic:
by
    simp only [this, funext_iff, indicator_apply]
    grind

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = single a b + erase a f

Tactic:
by
  classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = erase a f + single a b

Tactic:
by
  classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
G : Type u_6
inst✝ : AddGroup G
f : ι →₀ G
a : ι
⊢ erase a f = f - single a (f a)

Tactic:
ext a'

Goal state after:
ι : Type u_1
G : Type u_6
inst✝ : AddGroup G
f : ι →₀ G
a a' : ι
⊢ (erase a f) a' = (f - single a (f a)) a'
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
⊢ (fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P) = P

Tactic:
ext (_ | a)

Goal state after:
case none
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
⊢ ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P)) none = P none

case some
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
a : α
⊢ ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P)) (Option.some a) =
    P (Option.some a)
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
⊢ ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i)

Tactic:
simp only [le_antisymm_iff, iSup_le_iff]
  refine ⟨fun i ↦ ?_, fun a ↦ ?_⟩
  · grw [← le_iSup f i, ← subset_iUnion s i]
    intro; simp [← h1]
  by_cases ha : a ∈ ⋃ i, s i
  · obtain ⟨i, hi⟩ : ∃ i, a ∈ s i := by simpa using ha
    rw [mulIndicator_of_mem ha, iSup_apply, iSup_apply]
    refine iSup_le fun j ↦ ?_
    obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j
    refine le_iSup_of_le k <| (hf hjk _).trans_eq ?_
    rw [mulIndicator_of_mem (hs hik hi)]
  · rw [mulIndicator_of_notMem ha, ← h1]
    exact bot_le

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ 1 * (erase y f).prod g = f.prod g

Tactic:
erase_of_notMem_support hyf,

Goal state after:
case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ 1 * f.prod g = f.prod g
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
⊢ ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
    (∑ i ∈ insert i s, g i).support = (insert i s).biUnion fun i ↦ (g i).support

Tactic:
simp only [hi, sum_insert, not_false_iff, biUnion_insert]

Goal state after:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
⊢ ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
    (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun i ↦ (g i).support
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ indicator s f = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)

Tactic:
by
  rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach]
  · refine Finset.sum_congr rfl (fun _ _ => ?_)
    rw [indicator_of_mem]
  · intro i _ hi
    rw [notMem_support_iff.mp hi, single_zero]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
⊢ 1 ≤ (map f s).prod

Tactic:
refine one_le_prod fun r hr ↦ ?_

Goal state after:
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
r : R
hr : r ∈ map f s
⊢ 1 ≤ r
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)

Tactic:
refine ((sum_sum_index ?_ ?_).trans ?_).symm
  · intro
    exact single_zero _
  · intro
    exact single_add _
  refine sum_congr fun _ _ => sum_single_index ?_
  exact single_zero _

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
a : β
⊢ a ∉ l.support

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
⊢ False
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
⊢ a ∉ s →
    ((∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)) →
      (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)

Tactic:
ha

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
⊢ ((∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)) →
    (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
hsum : 1 ≤ ∏ x ∈ s, f x
⊢ 1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x

Tactic:
hsum.lt_iff_ne',

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
hsum : 1 ≤ ∏ x ∈ s, f x
⊢ ∏ x ∈ s, f x ≠ 1 ↔ ∃ x ∈ s, 1 < f x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
y : M
⊢ y ∈ f.frange ↔ y ≠ 0 ∧ y ∈ Set.range ⇑f

Tactic:
rw [frange, @Finset.mem_image _ _ (Classical.decEq _) _ f.support]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
y : M
⊢ (∃ a ∈ f.support, f a = y) ↔ y ≠ 0 ∧ y ∈ Set.range ⇑f
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
M : Type u_4
inst✝ : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
a✝ : M
⊢ a✝ ∈ Multiset.map (fun i ↦ g i) s.val → p a✝

Tactic:
ha

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
M : Type u_4
inst✝ : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
a✝ : M
ha : a✝ ∈ Multiset.map (fun i ↦ g i) s.val
⊢ p a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
⊢ a ∈ (f ::ₘ s).sum.support → ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
ha

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
⊢ ∑ t ∈ B, #(s ∩ t) ≤ #s * n

Tactic:
refine le_trans ?_ (s.sum_le_card_nsmul _ _ h)
  simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
  exact sum_comm.le

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
⊢ (single a m).extendDomain = single (↑a) m

Tactic:
ext a'

Goal state after:
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
a' : α
⊢ (single a m).extendDomain a' = (single (↑a) m) a'
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ i ∈ image Sigma.fst l.support ↔ l.split i ≠ 0

Tactic:
mem_image,

Goal state after:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst = i) ↔ l.split i ≠ 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a), ⟨a, b⟩ ∈ l.support ↔ a ∈ image Sigma.fst l.support ∧ b ∈ l.support.preimage (Sigma.mk a) ⋯

Tactic:
mem_image,

Goal state after:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a), ⟨a, b⟩ ∈ l.support ↔ (∃ a_1 ∈ l.support, a_1.fst = a) ∧ b ∈ l.support.preimage (Sigma.mk a) ⋯
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
⊢ (single a r) b • f a = (single a (r • f b)) b

Tactic:
by
  by_cases h : a = b <;> simp [h]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
s : Finset α
f : α → ℕ
⊢ ∑ x ∈ s, f x ≤ 1 ↔ ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1

Tactic:
refine ⟨fun h x y hsx hsy hfx hfy ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_2
s : Finset α
f : α → ℕ
h : ∑ x ∈ s, f x ≤ 1
x y : α
hsx : x ∈ s
hsy : y ∈ s
hfx : f x ≠ 0
hfy : f y ≠ 0
⊢ x = y ∧ f x = 1

case refine_2
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
⊢ ∑ x ∈ s, f x ≤ 1