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

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ iSupIndep f ↔ Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 2 ⊔ f 0) ∧ Disjoint (f 2) (f 0 ⊔ f 1)

Tactic:
rw [iSupIndep_def, sup_comm (f 2) (f 0)]

Goal state after:
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ (∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)) ↔
    Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ (∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)) ↔
    Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun ⟨h₀, h₁, h₂⟩ i ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 0) (f 1 ⊔ f 2)

case refine_2
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 1) (f 0 ⊔ f 2)

case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)

case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
A : Type w
M : Type v₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : MulAction A M
inst✝ : SMul R M
h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x
r : R
a : A
x : M
⊢ (algebraMap R A) r • a • x = r • a • x

Tactic:
h

Goal state after:
R : Type u
A : Type w
M : Type v₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : MulAction A M
inst✝ : SMul R M
h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x
r : R
a : A
x : M
⊢ r • a • x = r • a • x
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : Algebra R A
h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
x : R
y : S
z : A
⊢ (algebraMap S A) ((algebraMap R S) x) * ((algebraMap S A) y * z) = (algebraMap R A) x * ((algebraMap S A) y * z)

Tactic:
h

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
h : x ∈ span R s
⊢ f x ∈ span R₂ (⇑f '' s)

Tactic:
rw [Submodule.span_image]
  exact Submodule.mem_map_of_mem 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
ι : Type u_9
p : Submodule R M
s : ι → M
hs : ∀ (i : ι), s i ∈ p
⊢ span R (range fun i ↦ ⟨s i, ⋯⟩) = ⊤ ↔ span R (range s) = p

Tactic:
simp [← span_val_image_eq_iff, ← Set.range_comp, Function.comp_def]

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
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))

Tactic:
h

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
h : x ≠ y
⊢ Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
⊢ (f * g) x = g x

Tactic:
have : f x = 1 := notMem_mulSupport.1 (disjoint_right.1 h hx)

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ (f * g) x = g x
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ 1 * sᶜ.mulIndicator g x = g x

Tactic:
Set.mulIndicator_of_mem (Set.mem_compl h),

Goal state after:
case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ 1 * g x = 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
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
| ⨅ i, map f (p i)

Tactic:
← map_comap_eq_of_surjective hf (⨅ _, _),

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₂
hf : Surjective ⇑f
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
| map f (comap f (⨅ x, map f (p x)))
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
j' : γ
⊢ j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
j' : γ
h : j' ≠ j
⊢ {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
Module: Mathlib.Data.List.Find

Goal state before:
pp: α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ ~ l₂
hp : {x | x ∈ l₁ ∧ p x = true}.Subsingleton
⊢ find? p l₁ = find? p l₂

Tactic:
induction h with

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : Unique α
f g : α →₀ M
h : f default = g default
a : α
⊢ f a = g a

Tactic:
Unique.eq_default a

Goal state after:
α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : Unique α
f g : α →₀ M
h : f default = g default
a : α
⊢ f default = g default
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
⊢ mapRange e he₀ a = mapRange e he₀ b → a = b

Tactic:
h

Goal state after:
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : mapRange e he₀ a = mapRange e he₀ b
⊢ a = b
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
e : R
h : e * e = e
x✝ : R
⊢ x✝ * (e * e) = x✝ * e

Tactic:
h

Goal state after:
R : Type u_1
inst✝ : Semiring R
e : R
h : e * e = e
x✝ : R
⊢ x✝ * e = x✝ * e
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
h : f (f 1) = f 1
r : R
⊢ r • f (f 1) = r • f 1

Tactic:
h

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
h : f (f 1) = f 1
r : R
⊢ r • f 1 = r • f 1
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
⊢ (fun f ↦ indicator s f) a = (fun f ↦ indicator s f) b → a = b

Tactic:
h

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h : (fun f ↦ indicator s f) a = (fun f ↦ indicator s f) b
⊢ a = b
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case h.left
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
d : α
⊢ (embDomain f l) (f d) = (single c b) d

Tactic:
h

Goal state after:
case h.left
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
d : α
⊢ (single a b) (f d) = (single c b) d
Module: Mathlib.Data.Finsupp.Option

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

Tactic:
by
  ext a
  cases a
  · rw [optionElim_apply_none]
  · simp

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : f a = 0
⊢ g a (f a) = 1

Tactic:
h

Goal state after:
case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : f a = 0
⊢ g a 0 = 1
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
x✝ : ι
⊢ s.indicator 1 x✝ = 1 ↔ t.indicator 1 x✝ = 1

Tactic:
h

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

Goal state before:
pp: f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
x✝ : ℕ
hf : x✝ ∈ f.support
H : x✝ = 0
⊢ False

Tactic:
subst H

Goal state after:
f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
hf : 0 ∈ f.support
⊢ False
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
h : Rel (fun x1 x2 ↦ x1 ≤ x2) s t
⊢ s.prod ≤ t.prod

Tactic:
induction h with

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

Goal state before:
pp: α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
⊢ f.graph = g.graph → f = g

Tactic:
h

Goal state after:
α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f = g
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_12
M : Type u_13
inst✝ : Zero M
⊢ Injective graph

Tactic:
by
  intro f g h
  classical
    have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
    refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩
    exact mk_mem_graph _ (hsup ▸ hx)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ (mapDomain f x) (f a) = x a

Tactic:
rw [mapDomain, sum_apply, sum]
    simp_rw [single_apply]
    by_cases hax : a ∈ x.support
    · rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
    · rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
⊢ 0 < m.prod ↔ ∀ (x : R), x ∈ m → 0 < x

Tactic:
rcases m with ⟨l⟩

Goal state after:
case mk
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < prod (Quot.mk (⇑(List.isSetoid R)) l) ↔ ∀ (x : R), x ∈ Quot.mk (⇑(List.isSetoid R)) l → 0 < x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ ↑s.support ⊆ ↑s.support

Tactic:
exact Subset.refl _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
| f.sum g + g i a

Tactic:
rw [← Finsupp.update_self f i]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
| (f.update i (f i)).sum g + g i a
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
⊢ (r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j)) ^ 2 ≤ f i * g i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2

Tactic:
mul_pow,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
⊢ r i ^ 2 * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * g i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (∏ᶠ (i : α), f i)

Tactic:
rw [finprod]
  split_ifs
  exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f i

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset this]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)
⊢ ∏ i ∈ Finset.map Equiv.plift.symm.toEmbedding s, f i.down = ∏ i ∈ s, f i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ x ∈ span R (Set.range v)

Tactic:
← hl

Goal state after:
case mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ (linearCombination R v) l ∈ span R (Set.range v)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ (linearCombination R v) l ∈ span R (Set.range v)

Tactic:
linearCombination_apply

Goal state after:
case mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ (l.sum fun i a ↦ a • v i) ∈ span R (Set.range v)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case inr
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Nontrivial R
⊢ ∑ᶠ (i : α), f i ≠ 0

Tactic:
h

Goal state after:
case inr
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Nontrivial R
⊢ 1 ≠ 0
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), z i • v i ∈ span R (v '' s)
⊢ (linearCombination R v) z ∈ span R (v '' s)

Tactic:
linearCombination_apply

Goal state after:
case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), z i • v i ∈ span R (v '' s)
⊢ (z.sum fun i a ↦ a • v i) ∈ span R (v '' s)
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
v : Option α → M
f : Option α →₀ R
⊢ (f none • v none + f.some.sum fun a r ↦ r • v (Option.some a)) =
    f none • v none + (linearCombination R (v ∘ Option.some)) f.some

Tactic:
linearCombination_apply

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Option α → M
f : Option α →₀ R
⊢ (f none • v none + f.some.sum fun a r ↦ r • v (Option.some a)) =
    f none • v none + f.some.sum fun i a ↦ a • (v ∘ Option.some) i
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
α' : Type u_7
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ (linearCombination R v) (comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

Tactic:
linearCombination_apply

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ ((comapDomain f l hf).sum fun i a ↦ a • v i) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i
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
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
x : α
a✝ : x ∈ s
⊢ f x • g x ≠ 0 → f x ≠ 0

Tactic:
h

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
x : α
a✝ : x ∈ s
h : f x • g x ≠ 0
⊢ f x ≠ 0
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
α' : Type u_7
M' : Type u_8
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
v✝ : α → M
v' : α' → M'
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
u v : α → M
a✝ : α
⊢ (linearCombination R (u + v) ∘ₗ lsingle a✝) 1 = ((linearCombination R u + linearCombination R v) ∘ₗ lsingle a✝) 1

Tactic:
simp [Pi.add_apply, smul_add]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set M
inst✝ : Fintype ↑s
x : M
⊢ x ∈ span R s ↔ ∃ f, ∑ a, f a • ↑a = x

Tactic:
conv_lhs => rw [← Subtype.range_val (s := s)]
  exact mem_span_range_iff_exists_fun _

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

Goal state before:
pp: α : Type u
m i : ℕ
h : i.succ < m.succ
x : α
u : Fin m → α
⊢ vecCons x u ⟨i.succ, h⟩ = u ⟨i, ⋯⟩

Tactic:
by
  simp only [vecCons, Fin.cons, Fin.cases_succ']

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
⊢ vecAppend ⋯ ![] v = v

Tactic:
by
  ext
  simp [vecAppend_eq_ite]

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
⊢ vecAppend ⋯ v ![] = v

Tactic:
by
  ext
  simp [vecAppend_eq_ite]

Goal state after:
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
⊢ 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:
not_lt,

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, 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⟩
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
⊢ (b ∈ mulSupport fun b ↦ ∏ a ∈ s with g a = b, f a) → b ∈ g '' ↑s

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b ↦ ∏ a ∈ s with g a = b, f a
⊢ b ∈ g '' ↑s
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y : ℕ∞
h : y ≠ 0
⊢ ⊤ ^ y = ⊤

Tactic:
induction y with
  | top => exact top_epow_top
  | coe y => rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : x ≠ 0
y : ℕ∞
⊢ ∀ ⦃b : ℕ∞⦄, y ≤ b → (fun y ↦ x ^ y) y ≤ (fun y ↦ x ^ y) b

Tactic:
z

Goal state after:
x : ℕ∞
h : x ≠ 0
y z : ℕ∞
⊢ y ≤ z → (fun y ↦ x ^ y) y ≤ (fun y ↦ x ^ y) z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe.top.inl
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_0 : x < 1
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

pp: case coe.top.inr.inl
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
h : 1 ≠ 0
⊢ (fun y ↦ 1 ^ y) ↑a✝ ≤ (fun y ↦ 1 ^ y) ⊤

pp: case coe.top.inr.inr
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_2 : 1 < x
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

Tactic:
· exact (h (Order.lt_one_iff.1 x_0)).rec

Goal state after:
case coe.top.inr.inl
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
h : 1 ≠ 0
⊢ (fun y ↦ 1 ^ y) ↑a✝ ≤ (fun y ↦ 1 ^ y) ⊤

case coe.top.inr.inr
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_2 : 1 < x
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤