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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
s : Set α
hs : sSupIndep s
⊢ s.Finite

Tactic:
by_contra inf

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
⊢ False
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0

Tactic:
induction s using Finset.induction_on with
    | empty => exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
    | insert _ _ ha ih => rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ : S
⊢ ∀ (y_1 : S),
    x✝ ∈ span R s →
      y_1 ∈ span R s → x✝ • y ∈ span R (s • t) → y_1 • y ∈ span R (s • t) → (x✝ + y_1) • y ∈ span R (s • t)

Tactic:
_

Goal state after:
case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
⊢ x✝ ∈ span R s → y✝ ∈ span R s → x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → (x✝ + y✝) • y ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
⊢ x✝ ∈ span R s → y✝ ∈ span R s → x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → (x✝ + y✝) • y ∈ span R (s • t)

Tactic:
_

Goal state after:
case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
⊢ y✝ ∈ span R s → x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → (x✝ + y✝) • y ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
⊢ y✝ ∈ span R s → x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → (x✝ + y✝) • y ∈ span R (s • t)

Tactic:
_

Goal state after:
case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
⊢ x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → (x✝ + y✝) • y ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0✝ : S
y : A
hy : y ∈ t
r : R
s0 : S
⊢ s0 ∈ span R s → s0 • y ∈ span R (s • t) → (r • s0) • y ∈ span R (s • t)

Tactic:
_

Goal state after:
case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0✝ : S
y : A
hy : y ∈ t
r : R
s0 : S
hx✝ : s0 ∈ span R s
⊢ s0 • y ∈ span R (s • t) → (r • s0) • y ∈ span R (s • t)
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
| ∏ x, (φ x) (mulSingle i m x) = (φ i) m

Tactic:
1,

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
| ∏ x, (φ x) (mulSingle i m x)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case refine_4.refine_3
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
x✝² : M
hx✝ : x✝² ∈ span R (⋃ i, ↑(p i))
r : R
x✝¹ : M
x✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
hx : x✝¹ ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
x y : M
⊢ x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
    y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
      r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
        r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) → r • (x + y) ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
_

Goal state after:
case refine_4.refine_3
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
x✝² : M
hx✝¹ : x✝² ∈ span R (⋃ i, ↑(p i))
r : R
x✝¹ : M
x✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
hx : x✝¹ ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
x y : M
hx✝ : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
    r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
      r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) → r • (x + y) ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case refine_4.refine_3
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
x✝² : M
hx✝¹ : x✝² ∈ span R (⋃ i, ↑(p i))
r : R
x✝¹ : M
x✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
hx : x✝¹ ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
x y : M
hx✝ : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
    r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
      r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) → r • (x + y) ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
_

Goal state after:
case refine_4.refine_3
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
x✝² : M
hx✝¹ : x✝² ∈ span R (⋃ i, ↑(p i))
r : R
x✝¹ : M
x✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
hx : x✝¹ ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
x y : M
hx✝ : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
hy✝ : y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
    r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) → r • (x + y) ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
⊢ IsCompactlyGenerated α

Tactic:
isSupFiniteCompact_iff_all_elements_compact

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
⊢ IsCompactlyGenerated α
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:
by
  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 inr.refine_1
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
⊢ I ∈ S → ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
_

Goal state after:
case inr.refine_1
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s ∈ c
⊢ Disjoint b (sSup s)

Tactic:
exact (hc1 hs).2.1

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
⊢ x ∈ t a → ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))

Tactic:
_

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝ : x ∈ t a
⊢ ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝ : x ∈ t a
y : κ a
⊢ y ∈ t a → x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))

Tactic:
_

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝¹ : x ∈ t a
y : κ a
a✝ : y ∈ t a
⊢ x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case insert
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
⊢ (∑ b ∈ t a, f a b) * ∏ x ∈ s, ∑ b ∈ t x, f x b = ∑ p ∈ (insert a s).pi t, ∏ x ∈ (insert a s).attach, f (↑x) (p ↑x ⋯)

Tactic:
pi_insert ha,

Goal state after:
case insert
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
⊢ (∑ b ∈ t a, f a b) * ∏ x ∈ s, ∑ b ∈ t x, f x b =
    ∑ p ∈ (t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t), ∏ x ∈ (insert a s).attach, f (↑x) (p ↑x ⋯)
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
G : Type u_6
inst✝ : Group G
s : Set α
f : α → G
⊢ sᶜ.mulIndicator f = f / s.mulIndicator f

Tactic:
rw [div_eq_mul_inv, mulIndicator_compl]

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✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
⊢ map f (⨅ i, p i) = map f (⨅ i, comap f (map f (p i)))

Tactic:
simp_rw [fun i ↦ comap_map_eq_self (le_iInf_iff.mp h i)]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
⊢ a ∈ (onFinset s f hf).support ↔ f a ≠ 0

Tactic:
by
  rw [Finsupp.mem_support_iff, Finsupp.onFinset_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ b₁ = b₂

Tactic:
have : (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a := by rw [eq]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
this : (single a b₁) a = (single a b₂) a
⊢ b₁ = b₂
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ f = single a b ↔ f.support ⊆ {a} ∧ f a = b

Tactic:
by
  refine ⟨fun h => h.symm ▸ ⟨support_single_subset, single_eq_same⟩, ?_⟩
  rintro ⟨h, rfl⟩
  ext x
  by_cases hx : x = a <;> simp only [hx, single_eq_same, single_eq_of_ne, Ne, not_false_iff]
  exact notMem_support_iff.1 (mt (fun hx => (mem_singleton.1 (h hx))) hx)

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : MulZeroOneClass R
s : Set α
r : R
a : α
⊢ s.indicator (fun x ↦ r • 1 x) a = s.indicator (fun x ↦ r) a

Tactic:
Pi.one_apply,

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : MulZeroOneClass R
s : Set α
r : R
a : α
⊢ s.indicator (fun x ↦ r • 1) a = s.indicator (fun x ↦ r) a
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
⊢ ∑ a ∈ (indicator s f).support, single a ((indicator s f) a) = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)

Tactic:
sum_subset (support_indicator_subset _ _),

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

α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∀ x ∈ s, x ∉ (indicator s f).support → single x ((indicator s f) x) = 0
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
i : α
⊢ i ∈ s → i ∉ (indicator s f).support → single i ((indicator s f) i) = 0

Tactic:
_

Goal state after:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
a✝ : i ∈ s
⊢ i ∉ (indicator s f).support → single i ((indicator s f) i) = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
⊢ x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0

Tactic:
_

Goal state after:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
a✝ : x b ≠ 0
⊢ b ≠ a → (single (f b) (x b)) (f a) = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ Multiset.map (fun i ↦ g i) s.val ≠ ∅

pp: case refine_2
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ ∀ a ∈ Multiset.map (fun i ↦ g i) s.val, p a

pp: case refine_3
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ (Multiset.map f (Multiset.map (fun i ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)

Tactic:
· simp [hs_nonempty.ne_empty]

Goal state after:
case refine_2
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ ∀ a ∈ Multiset.map (fun i ↦ g i) s.val, p a

case refine_3
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ (Multiset.map f (Multiset.map (fun i ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)
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
l : α →₀ M
⊢ comapDomain f (mapDomain f l) ⋯ = l

Tactic:
ext; rw [comapDomain_apply, mapDomain_apply hf]

Goal state after:
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 ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
⊢ ∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1

Tactic:
rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
      forall_mem_insert, ih this]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0
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₁ ∈ ↑f.support →
    ∀ ⦃y : α⦄, y ∈ ↑f.support → a₁ ≠ y → (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ y

Tactic:
_

Goal state after:
α : 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✝ : a₁ ∈ ↑f.support
⊢ ∀ ⦃y : α⦄, y ∈ ↑f.support → a₁ ≠ y → (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ y
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✝ : a₁ ∈ ↑f.support
a₂ : α
⊢ a₂ ∈ ↑f.support → a₁ ≠ a₂ → (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ a₂

Tactic:
_

Goal state after:
α : 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✝¹ : a₁ ∈ ↑f.support
a₂ : α
a✝ : a₂ ∈ ↑f.support
⊢ a₁ ≠ a₂ → (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ a₂
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #({a ∈ s | ¬f a = ∅}) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
grw [card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
    nonempty_of_ne_empty (mem_filter.1 hi).2, filter_subset]

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
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
i : ι
⊢ i ∈ l.splitSupport ↔ g i (l.split i) ≠ 0

Tactic:
mem_splitSupport_iff_nonzero,

Goal state after:
α : 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
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
i : ι
⊢ l.split i ≠ 0 ↔ g i (l.split i) ≠ 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ (if h : HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down) then ∏ i ∈ Finite.toFinset h, f i.down else 1) =
    ∏ i ∈ s, f i.down

Tactic:
dif_pos hf

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ i ∈ Finite.toFinset hf, f i.down = ∏ i ∈ s, f i.down
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Prop
f : p → M
g : q → M
hpq : p = q
hfg : ∀ (h : q), f ⋯ = g h
⊢ finprod f = finprod g

Tactic:
subst q

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
p : Prop
f g : p → M
hfg : ∀ (h : p), f ⋯ = g h
⊢ finprod f = finprod g
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Unique α
l : α →₀ R
v : α → M
⊢ (linearCombination R v) l = l default • v default

Tactic:
← linearCombination_single,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Unique α
l : α →₀ R
v : α → M
⊢ (linearCombination R v) l = (linearCombination R v) (single default (l default))