mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s t : Set M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ ∀ (c : R) {x : M × M'}, x ∈ ↑p ×ˢ ↑q₁ → c • x ∈ ↑p ×ˢ ↑q₁

Tactic:
rintro a ⟨x, y⟩ ⟨hx, hy⟩; exact ⟨smul_mem _ a hx, smul_mem _ a hy⟩

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

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ ∀ a ∈ {c | IsCompactElement c ∧ c ≤ b}, a = ⊥

Tactic:
exact h

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
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
yy : M'
hyy : yy ∈ q₁ ⊔ q₁'
x : M
hx : x ∈ p
x' : M
hx' : x' ∈ p'
hxx : x + x' ∈ p ⊔ p'
⊢ (x + x', yy) ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
rcases mem_sup.1 hyy with ⟨y, hy, y', hy', rfl⟩

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
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
x : M
hx : x ∈ p
x' : M
hx' : x' ∈ p'
hxx : x + x' ∈ p ⊔ p'
y : M'
hy : y ∈ q₁
y' : M'
hy' : y' ∈ q₁'
hyy : y + y' ∈ q₁ ⊔ q₁'
⊢ (x + x', y + y') ∈ p.prod q₁ ⊔ p'.prod q₁'
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) = -span R s

Tactic:
apply le_antisymm
  · rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]
    exact subset_span
  · rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]
    exact subset_span

Goal state after:
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 : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ f a b * ∏ x ∈ s.attach, f (↑x) (g ↑x ⋯) =
    f (↑⟨a, ⋯⟩) (Pi.cons s a b g ↑⟨a, ⋯⟩ ⋯) * ∏ x ∈ s.attach, f (↑⟨↑x, ⋯⟩) (Pi.cons s a b g ↑⟨↑x, ⋯⟩ ⋯)

Tactic:
simp only [Pi.cons_same]

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 : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ f a b * ∏ x ∈ s.attach, f (↑x) (g ↑x ⋯) = f a b * ∏ x ∈ s.attach, f (↑x) (Pi.cons s a b g ↑x ⋯)
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
p : Submodule R M
le : f.ker ≤ p
hp : IsCoatom p
⊢ IsCoatom (comap f (map f p))

Tactic:
rwa [comap_map_eq_self le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
i : α
j : γ
hj✝ : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
hi : {i} ⊆ mulSupport f
hs : ∀ ⦃i j : γ⦄, i ≠ j → ∀ ⦃x : Set α⦄, x ⊆ s i ∧ x ⊆ mulSupport f → x ⊆ s j ∧ x ⊆ mulSupport f → x ⊆ ⊥
⊢ False

Tactic:
simpa using hs h ⟨hj', hi⟩ ⟨hj, hi⟩

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ motive f

Tactic:
← single_add_erase a f

Goal state after:
case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ motive (single a (f a) + erase a f)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : 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
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
by
  by_cases hyf : y ∈ f.support
  · exact Finsupp.mul_prod_erase f y g hyf
  · rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
⊢ s.indicator (fun x ↦ a * f x) i = a * s.indicator f i

Tactic:
rw [indicator_mul_right]

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

Goal state before:
pp: case cons
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x1 x2 ↦ x1 ≤ x2) as✝ bs✝
rt : as✝.prod ≤ bs✝.prod
⊢ (a✝¹ ::ₘ as✝).prod ≤ (b✝ ::ₘ bs✝).prod

Tactic:
rw [prod_cons, prod_cons]
    exact mul_le_mul' rh rt

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

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

Tactic:
apply h

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0

Tactic:
simp_rw [graph, mem_map, mem_support_iff]
  constructor
  · rintro ⟨b, ha, rfl, -⟩
    exact ⟨rfl, ha⟩
  · rintro ⟨rfl, ha⟩
    exact ⟨a, ha, rfl⟩

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

Goal state before:
pp: case h₁
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ f a < g a

Tactic:
apply h

Goal state after:
case h₁
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ a ∈ a :: s
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
⊢ f i < g i

Tactic:
apply h

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
⊢ i ∈ a :: s
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ a ∉ Set.range f

Tactic:
exact h

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

Goal state before:
pp: α : Type u_12
β : Type u_13
M : Type u_14
inst✝ : AddCommGroup M
v₁ v₂ : α →₀ M
f : α → β
⊢ mapDomain f (v₁ - v₂) = mapDomain f v₁ - mapDomain f v₂

Tactic:
simp [mapDomain, sum_sub_index]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hf : Injective f
l' : α →₀ M
⊢ (fun l ↦ comapDomain f l ⋯) (embDomain { toFun := f, inj' := hf } l') = l'

Tactic:
exact Finsupp.comapDomain_embDomain ..

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

Goal state before:
pp: case refine_2
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
x✝ : ℕ
⊢ x✝ ∈ ↑(erase 0 l).support → x✝ ∈ Set.range fun x ↦ x + 1

Tactic:
simp_all [Nat.pos_iff_ne_zero]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
x : α
hx : x ∈ Finset.filter p f.support
⊢ single x ((filter p f) x) = single x (f x)

Tactic:
by
      rw [filter_apply_pos _ _ (mem_filter.1 hx).2]

Goal state after:
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✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
gcongr with j hj j hj

Goal state after:
case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ g j ≤ f j

case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ h j ≤ f j
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case neg
ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∉ S
⊢ ∏ x ∈ S', f x < ∏ x ∈ S, f x

Tactic:
calc ∏ x ∈ S', f x
        ≤ ∏ x ∈ S.erase d ∪ {d'}, f x := Finset.prod_le_prod_of_subset' hS'
      _ = (∏ x ∈ S.erase d, f x) * f d' := by
          rw [Finset.prod_union (Finset.disjoint_singleton_right.mpr
            (fun h ↦ hd'S (Finset.mem_of_mem_erase h))), Finset.prod_singleton]
      _ < (∏ x ∈ S.erase d, f x) * f d := mul_lt_mul_right hlt _
      _ = ∏ x ∈ S, f x := Finset.prod_erase_mul S f hd_mem

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

Goal state before:
pp: M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
this : Multiset.map (fun x ↦ b • f x) s.val = Multiset.map (fun x ↦ b • x) (Multiset.map f s.val)
⊢ b ^ #s • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

Tactic:
prod_eq_multiset_prod,

Goal state after:
M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
this : Multiset.map (fun x ↦ b • f x) s.val = Multiset.map (fun x ↦ b • x) (Multiset.map f s.val)
⊢ b ^ #s • (Multiset.map f s.val).prod = (Multiset.map (fun x ↦ b • f x) s.val).prod
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (mapRange.addMonoidHom ↑f) (g • (x✝¹ + x✝)) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (x✝¹ + x✝)

Tactic:
rw [smul_add, map_add, h, h', map_add, smul_add]

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

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
⊢ (↑↑(ringHomEndFinsupp ι)).toFun ((fun f ↦ { toFun := fun m ↦ (f (single i m)) i, map_add' := ⋯, map_smul' := ⋯ }) f) =
    f

Tactic:
ext x j
    change f (Finsupp.lsingle (R := R) (M := M) i ∘ₗ Finsupp.lapply j • x) i = _
    rw [map_smul]
    simp

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ ∏ᶠ (x : α), f x = f a

Tactic:
by
  have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) := by
    intro x
    contrapose
    simpa [PLift.eq_up_iff_down_eq] using ha x.down
  rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton]

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

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ image Fin.val (s.attachFin h) = s

Tactic:
apply coe_injective
  rw [coe_image, coe_attachFin, Set.image_preimage_eq_iff]
  exact fun m hm ↦ ⟨⟨m, h m hm⟩, rfl⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ val '' castAdd m '' Ici i = val '' Ico (castAdd m i) (natAdd n 0)

Tactic:
simp [← image_comp]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ val '' castAdd m '' Ioi i = val '' Ioo (castAdd m i) (natAdd n 0)

Tactic:
simp [← image_comp]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
u : M
⊢ ∑ i, b.equivFun u i • b i = u

Tactic:
rw [← b.equivFun_symm_apply, b.equivFun.symm_apply_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ (linearCombination R A) ((linearCombination R B) f) = (linearCombination R fun b ↦ (linearCombination R A) (B b)) f

Tactic:
simp only [linearCombination_apply]
  induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i
x✝ : M
a✝ : ι
⊢ (b₁.repr x✝) a✝ = (b₂.repr x✝) a✝

Tactic:
apply h

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
hg : (s ∩ mulSupport g).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
rw [← mulSupport_mulIndicator] at hf hg
  simp only [finprod_mem_def, mulIndicator_mul, finprod_mul_distrib hf hg]

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

Goal state before:
pp: m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ vecAppend ho u v i = if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Tactic:
rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]

Goal state after:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (if hi : ↑(Fin.cast ho i) < m then ⋯ ▸ u ((Fin.cast ho i).castLT hi)
    else ⋯ ▸ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯)) =
    if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg.succ
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h✝ : ¬↑⟨i + 1, hi⟩ < m + 1
h : m + 1 ≤ ↑⟨i + 1, hi⟩
⊢ v ⟨↑⟨i + 1, hi⟩ - (m + 1), ⋯⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨i + 1, hi⟩

Tactic:
Fin.val_mk,

Goal state after:
case neg.succ
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h✝ : ¬↑⟨i + 1, hi⟩ < m + 1
h : m + 1 ≤ i + 1
⊢ v ⟨↑⟨i + 1, hi⟩ - (m + 1), ⋯⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨i + 1, hi⟩
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n

Tactic:
Fin.val_mk,

Goal state after:
case neg
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
Fin.val_mk,

Goal state after:
case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i

Tactic:
· rw [finprod_mem_range]
    exact Option.some_injective _

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

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
⊢ (vecCons a (vecCons b x) ∘ ⇑(Equiv.swap 0 1)) ⟨i + 2, h⟩ = vecCons b (vecCons a x) ⟨i + 2, h⟩

Tactic:
have h' : (⟨i + 2, h⟩ : Fin n.succ.succ) = Fin.succ (Fin.succ ⟨i, by lia⟩) := by grind
    simp only [Nat.succ_eq_add_one, h', Function.comp_apply,
      Equiv.swap_apply_of_ne_of_ne (Fin.succ_ne_zero _) (Fin.succ_succ_ne_one _), cons_val_succ]

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

Goal state before:
pp: case inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k

Tactic:
rcases eq_or_ne k i.succ with rfl | hki

Goal state after:
case inr.inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : i.succ ≠ 0
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) i.succ = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) i.succ

case inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ᶠ (x : α), ∏ y ∈ s with f y = x, g y = ∏ k ∈ s, g k

Tactic:
finprod_eq_finsetProd_of_mulSupport_subset

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ i ∈ ?s, ∏ y ∈ s with f y = i, g y = ∏ k ∈ s, g k

case s
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ Finset α

case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ (mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) ⊆ ↑?s
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ x ^ ⊤ ≤ z ^ ⊤

Tactic:
rw [Order.lt_one_iff.1 x_0, zero_epow_top]

Goal state after:
case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ 0 ≤ z ^ ⊤
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
hv : ∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i
f g : ι → R
hfg : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = g i

Tactic:
← s.sum_attach

Goal state after:
case mp
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
hv : ∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i
f g : ι → R
i : ι
hi : i ∈ s
hfg : ∑ x ∈ s.attach, f ↑x • v ↑x = ∑ x ∈ s.attach, g ↑x • v ↑x
⊢ f i = g i
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n : ℕ
h : ∃ m n, m • p + a = n • p + b
⊢ ∃ m n_1, m • n • p + n • a = n_1 • n • p + n • b

Tactic:
rcases h with ⟨k, l, h⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
⊢ ∃ m n_1, m • n • p + n • a = n_1 • n • p + n • b
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
⊢ ∀ (s_1 : Finset ↑s), LinearIndependent R ((fun x ↦ v ↑x) ∘ Subtype.val)

Tactic:
exact fun t ↦ (hv (t.map <| .subtype _) (by simp)).comp (ι' := t)
      (fun x ↦ ⟨x, Finset.mem_map_of_mem (.subtype _) x.2⟩) fun x ↦ by aesop

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : ∃ m n, m • p + a = n • p + b
hadd : ∃ m n, m • p + (a + c) = n • p + (b + d)
⊢ ∃ m n, m • p + c = n • p + d

Tactic:
rcases h with ⟨k, l, h⟩

Goal state after:
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
hadd : ∃ m n, m • p + (a + c) = n • p + (b + d)
k l : ℕ
h : k • p + a = l • p + b
⊢ ∃ m n, m • p + c = n • p + d