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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo (a ⊓ b) a)
⊢ a ⊓ (b ⊔ ↑c) = ↑c

Tactic:
← inf_sup_assoc_of_le _ c.prop.2.le,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo (a ⊓ b) a)
⊢ a ⊓ b ⊔ ↑c = ↑c
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : CompleteLattice α
c : ClosureOperator α
p : α → Prop
hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)
a : α
⊢ a ≤ ⨅ b, ↑b

Tactic:
by simp +contextual

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
⊢ y₁ + (y₂ + z₁ + z₂) = y₁ + (z₁ + y₂ + z₂)

Tactic:
add_comm y₂

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
⊢ y₁ + (z₁ + y₂ + z₂) = y₁ + (z₁ + y₂ + z₂)
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case inl
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h✝ : a ≤ b
⊢ max a b ∈ s

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case inr
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h✝ : b ≤ a
⊢ max a b ∈ s

Tactic:
simp [*]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
P : M → Prop
⊢ (∀ x ∈ p ⊔ p', P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)

Tactic:
simp [mem_sup]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
P : M → Prop
⊢ (∀ (x x_1 : M), x_1 ∈ p → ∀ x_2 ∈ p', x_1 + x_2 = x → P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
P : M → Prop
⊢ (∃ x ∈ p ⊔ p', P x) ↔ ∃ x₁ ∈ p, ∃ x₂ ∈ p', P (x₁ + x₂)

Tactic:
simp [mem_sup]

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

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑X ∪ ↑Y ⊆ S

Tactic:
exact Set.union_subset hX hY

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

Goal state before:
pp: case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j ∈ span R (range (update v j (v j + r • v i)))

Tactic:
← add_sub_cancel_right (v j) (r • v i)

Goal state after:
case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i - r • v i ∈ span R (range (update v j (v j + r • v i)))
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e '' Ioo a b = Ioo (e a) (e b)

Tactic:
rw [e.image_eq_preimage_symm, e.symm.preimage_Ioo, e.symm_symm]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ ∀ a ∈ {f | IsAtom f ∧ f ≤ s}, IsAtom a

Tactic:
by simp +contextual

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ sSup s ∈ s

Tactic:
rw [ht₂]

Goal state after:
case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ ⊥ ∈ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ ⊥ ∈ s

Tactic:
simp [eq_singleton_bot_of_sSup_eq_bot_of_nonempty ht₂ hne]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s

Tactic:
rw [ht₂]

Goal state after:
case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ t.sup id ∈ s
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : x✝ ∈ s
⊢ (g ∘ f) x✝ = (g ∘ s.mulIndicator f) x✝

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case neg
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = (g ∘ s.mulIndicator f) x✝

Tactic:
simp [*]

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
⊢ (∏ i ∈ s, if p i then f i else 0) = if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0

Tactic:
by
  split_ifs with h
  · exact prod_congr rfl fun i hi => by simp [h i hi]
  · push Not at h
    rcases h with ⟨i, hi, hq⟩
    exact prod_eq_zero hi (by simp [hq])

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

Goal state before:
pp: case empty
ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
f : ι → G₀
h : ∏ i ∈ ∅, f i ≠ 0
⊢ mk0 (∏ i ∈ ∅, f i) h = ∏ i ∈ ∅.attach, mk0 (f ↑i) ⋯

Tactic:
simp [*]

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

Goal state before:
pp: case cons
ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
f : ι → G₀
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∀ (h : ∏ i ∈ s✝, f i ≠ 0), mk0 (∏ i ∈ s✝, f i) h = ∏ i ∈ s✝.attach, mk0 (f ↑i) ⋯
h : ∏ i ∈ Finset.cons a✝¹ s✝ h✝, f i ≠ 0
⊢ mk0 (∏ i ∈ Finset.cons a✝¹ s✝ h✝, f i) h = ∏ i ∈ (Finset.cons a✝¹ s✝ h✝).attach, mk0 (f ↑i) ⋯

Tactic:
simp [*]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
hf : Injective ⇑f
⊢ f x ∈ span R₂ (⇑f '' s) ↔ x ∈ span R s

Tactic:
by
  rw [← Submodule.mem_comap, ← Submodule.map_span, Submodule.comap_map_eq_of_injective hf]

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
⊢ ((s.antidiagonal.bind fun a_1 ↦
        map (fun x ↦ Prod.map id (cons a) x) (map (fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal)) +
      s.antidiagonal.bind fun a_1 ↦
        map (fun x ↦ Prod.map (cons a) id x) (map (fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal)) =
    (s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map id (cons a) a_1).1 + q.1, (Prod.map id (cons a) a_1).2 + q.2)) t.antidiagonal) +
      s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map (cons a) id a_1).1 + q.1, (Prod.map (cons a) id a_1).2 + q.2)) t.antidiagonal

Tactic:
map_map

Goal state after:
case cons
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
⊢ ((s.antidiagonal.bind fun a_1 ↦
        map ((fun x ↦ Prod.map id (cons a) x) ∘ fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal) +
      s.antidiagonal.bind fun a_1 ↦
        map ((fun x ↦ Prod.map (cons a) id x) ∘ fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal) =
    (s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map id (cons a) a_1).1 + q.1, (Prod.map id (cons a) a_1).2 + q.2)) t.antidiagonal) +
      s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map (cons a) id a_1).1 + q.1, (Prod.map (cons a) id a_1).2 + q.2)) t.antidiagonal
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ (a : Multiset α) (s : Multiset (Multiset α)),
    s.Sections.card = (map card s).prod → (a ::ₘ s).Sections.card = (map card (a ::ₘ s)).prod

Tactic:
by simp +contextual

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
⊢ c ≤ b ⊔ sSup s

Tactic:
rw [← h, sSup_le_iff]

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
⊢ ∀ b_1 ∈ {a | a ≤ c ∧ IsAtom a}, b_1 ≤ b ⊔ sSup s
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ f.range ≤ map f p ↔ Codisjoint p f.ker

Tactic:
← map_top,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ map f ⊤ ≤ map f p ↔ Codisjoint p f.ker
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : ¬a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : ¬a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
simp [*]

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

Goal state before:
pp: M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst✝⁴ : Semiring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
this : ⨆ i ∈ s, comap f.range.subtype (p i) = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict

Goal state after:
M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst✝⁴ : Semiring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
this : ⨆ i ∈ s, comap f.range.subtype (p i) = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⨆ i ∈ s, comap f.rangeRestrict (comap f.range.subtype (p i))
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e₁ : N → O
e₂ : M → N
he₁ : e₁ 0 = 0
he₂ : e₂ 0 = 0
f : α →₀ M
⊢ (e₁ ∘ e₂) 0 = 0

Tactic:
simp [*]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

Tactic:
rw [prod_preimage', prod_filter_of_ne]

Goal state after:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ (embDomain Embedding.some f) (Option.some x) = f x

Tactic:
by
  simp [← Function.Embedding.some_apply]

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

Goal state before:
pp: case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
suffices ∀ y, f y = 0 by simp [this]
    clear x
    intro x
    rw [← smul_inv_smul₀ hR x, map_natCast_smul f R S, hS, zero_smul]

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
m : Multiset α
a : α
ha : a ∈ m
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedMul α
⊢ a ≤ m.prod

Tactic:
obtain ⟨t, rfl⟩ := exists_cons_of_mem ha

Goal state after:
α : Type u_2
inst✝² : CommMonoid α
a : α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedMul α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ (a ::ₘ t).prod
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ ∏ x ∈ s.erase i, f x ≤ ∏ x ∈ s.erase i, g x

pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 < ∏ x ∈ s.erase i, f x

pp: case refine_3
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 ≤ g i

Tactic:
· exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 < ∏ x ∈ s.erase i, f x

case refine_3
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 ≤ g i
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a✝ : List ι
h0 : ∀ (i : ι), i ∈ ⟦a✝⟧ → 0 ≤ f i
h : ∀ (i : ι), i ∈ ⟦a✝⟧ → f i ≤ g i
⊢ (map f ⟦a✝⟧).prod ≤ (map g ⟦a✝⟧).prod

Tactic:
simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *

Goal state after:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a✝ : List ι
h0 : ∀ (i : ι), i ∈ a✝ → 0 ≤ f i
h : ∀ (i : ι), i ∈ a✝ → f i ≤ g i
⊢ (List.map f a✝).prod ≤ (List.map g a✝).prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
this : (mapDomain f v₁) (f a) = (mapDomain f v₂) (f a)
⊢ v₁ a = v₂ a

Tactic:
mapDomain_apply hf,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
this : v₁ a = (mapDomain f v₂) (f a)
⊢ v₁ a = v₂ a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' ↑l.support)
⊢ ∀ (a : α), a ∈ l.support.preimage f hf ↔ l (f a) ≠ 0

Tactic:
by
    intro a
    rw [Finset.mem_preimage]
    exact l.mem_support_toFun (f a)

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

Goal state before:
pp: case empty
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
⊢ MulLECancellable (∏ i ∈ ∅, f i) ↔ ∀ ⦃i : ι⦄, i ∈ ∅ → MulLECancellable (f i)

Tactic:
simp [*]

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

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : MulLECancellable (∏ i ∈ s✝, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s✝ → MulLECancellable (f i)
⊢ MulLECancellable (∏ i ∈ cons a✝¹ s✝ h✝, f i) ↔ ∀ ⦃i : ι⦄, i ∈ cons a✝¹ s✝ h✝ → MulLECancellable (f i)

Tactic:
simp [*]

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

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

Tactic:
intro f s ih ha
      by_cases h : a ∈ f.support
      · exact ⟨f, Multiset.mem_cons_self _ _, h⟩
      · simp_rw [Multiset.sum_cons, mem_support_iff, add_apply, notMem_support_iff.1 h,
          zero_add] at ha
        rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩
        exact ⟨f', Multiset.mem_cons_of_mem h₀, h₁⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α × β →₀ M
a : α
⊢ ∀ (a_1 a' : α × β),
    ∀ b ∈ if a_1.1 = a then some a_1.2 else none, (b ∈ if a'.1 = a then some a'.2 else none) → a_1 = a'

Tactic:
by simp +contextual

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
a : α × β
m : M
⊢ (single a m).curry = (single a.1 (single a.2 m)).uncurry.curry

Tactic:
uncurry_single

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α × β
m : M
⊢ (single a m).curry = (single (a.1, a.2) m).curry
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = 0

Tactic:
simp [*]

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

Goal state before:
pp: case neg.h
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ a ∉ Set.range ⇑(Embedding.subtype P)

Tactic:
simp [*]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
f g : ι → M
s : Finset ι
inst✝ : MulLeftMono M
Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i
⊢ ∃ i ∈ s, f i < g i

Tactic:
contrapose! Hlt with Hle

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
f g : ι → M
s : Finset ι
inst✝ : MulLeftMono M
Hle : ∀ i ∈ s, g i ≤ f i
⊢ ∏ i ∈ s, g i ≤ ∏ i ∈ s, f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ s ∧ x ∈ mulSupport f

Tactic:
exact ⟨hx, hxf⟩

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ ↑t ∧ x ∈ mulSupport f

Tactic:
exact ⟨hx, hxf⟩

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ 1 < ∏ᶠ (i : ι), f i

Tactic:
rw [← finprod_mem_univ]

Goal state after:
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ 1 < ∏ᶠ (i : ι) (_ : i ∈ univ), f i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁴ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Module R M'
i : ι
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ (b.equiv b' e) (b i) = b' (e i)

Tactic:
by simp [Basis.equiv]

Goal state after:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
v : List.Vector α n
⊢ #{i | v.get i = a} = List.count a v.toList

Tactic:
induction v with
  | nil => simp
  | @cons n x xs hxs =>
    simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]

Goal state after:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
f : ℕ → α
⊢ (univ.sup fun n_1 ↦ f ↑n_1) = (range n).sup f

Tactic:
rw [← image_fin_univ, sup_image, Function.comp_def]

Goal state after: