mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ y = A * (B * ↑u⁻¹)

Tactic:
rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
h : DvdNotUnit p q
⊢ p ≠ q

Tactic:
by_contra hcontra

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
h : DvdNotUnit p q
hcontra : p = q
⊢ False
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
r : R
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂) r) = (algebraMap R A₁) r

Tactic:
by
      rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)]
      congr
      simp

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x y : A₁ ≃ₐ[R] A₁
z : A₁ˣ
⊢ (x * y) • z = x • y • z

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ˣ
⊢ 1 • x = x

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
⊢ ofEq p p ⋯ = refl R ↥p

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Surjective ⇑f.rangeRestrict

Tactic:
← range_eq_top,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.rangeRestrict.range = ⊤
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
x : M₁
y : M₂
⊢ i (((f.codRestrict₂ i hi hf) x) y) = (f x) y

Tactic:
by
  simp [codRestrict₂]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
h : s • N ≤ p
r : S
n : M
⊢ r ∈ s → n ∈ N → r • n ∈ p

Tactic:
hr

Goal state after:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
h : s • N ≤ p
r : S
n : M
hr : r ∈ s
⊢ n ∈ N → r • n ∈ p
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
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) → x ∈ p ⊔ p'

Tactic:
rintro ⟨y, hy, z, hz, rfl⟩
    exact add_mem ((le_sup_left : p ≤ p ⊔ p') hy) ((le_sup_right : p' ≤ p ⊔ p') hz)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
⊢ x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)

Tactic:
refine ⟨fun h => h ▸ by simp, fun h => ?_⟩

Goal state after:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
⊢ x = y
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case 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 : M
hx : x ∈ S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T

pp: case refine_2
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
⊢ ∃ T, ↑T ⊆ S ∧ 0 ∈ span R ↑T

pp: case refine_3
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 ∈ span R S →
      y ∈ span R S → (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T

pp: case refine_4
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
⊢ ∀ (a : R), ∀ x ∈ span R S, (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T

Tactic:
· refine ⟨{x}, ?_, ?_⟩
    · rwa [Finset.coe_singleton, Set.singleton_subset_iff]
    · rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x

Goal state after:
case refine_2
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
⊢ ∃ T, ↑T ⊆ S ∧ 0 ∈ span R ↑T

case refine_3
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 ∈ span R S →
      y ∈ span R S → (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T

case refine_4
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
⊢ ∀ (a : R), ∀ x ∈ span R S, (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
i : ι
x✝³ : i ∈ s
t : Finset (β i)
x✝² : t ⊆ g i
j : β i
x✝¹ : j ∈ g i
x✝ : j ∉ t
⊢ Disjoint (f ⟨i, j⟩) ((image (fun b ↦ ⟨i, b⟩) t).sup f)

Tactic:
grind [= SupIndep]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
⊢ Disjoint x (sSup y)

Tactic:
by
  have := (hs.mono <| insert_subset_iff.mpr ⟨hx, hy⟩) (mem_insert x _)
  rw [insert_sdiff_of_mem _ (mem_singleton _), sdiff_singleton_eq_self hxy] at this
  exact this

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : j ≠ i
⊢ t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k

Tactic:
exact le_iSup₂ (f := fun x _ ↦ t x) j contra

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

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬sSup s < k
sSup' : sSup s ≤ k
⊢ False

Tactic:
replace sSup : sSup s = k := eq_iff_le_not_lt.mpr ⟨sSup', h⟩

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
⊢ False
Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ IsSquare (∏ i ∈ s, f i)

Tactic:
rw [isSquare_iff_exists_sq]
  use (∏ (x : s), ((isSquare_iff_exists_sq _).mp (h _ x.2)).choose)
  rw [@sq, ← Finset.prod_mul_distrib, ← Finset.prod_coe_sort]
  congr
  ext i
  rw [← @sq]
  exact ((isSquare_iff_exists_sq _).mp (h _ i.2)).choose_spec

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
intro c hc hcinf
        rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc
        rw [le_inf_iff] at hcinf
        rcases hc s hs h hcinf.2 with ⟨d, ds, cd⟩
        exact (le_inf hcinf.1 cd).trans (le_biSup _ ds)

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

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

Tactic:
intro h
    subst hV
    suffices ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩ by
      ext ⟨x, hx⟩
      exact this x hx
    intro x hx
    induction hx using span_induction with
    | mem x hx => exact h ⟨x, hx⟩
    | zero => erw [map_zero, map_zero]
    | add x y hx hy hx' hy' =>
        erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
        rw [hx', hy']
    | smul a x hx hx' =>
        erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]
        rw [hx']

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ sSupIndep (⋃₀ s)

Tactic:
Set.sUnion_eq_iUnion

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ sSupIndep (⋃ i, ↑i)
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
a : α
s : Multiset α
ih : map Prod.swap s.antidiagonal = s.antidiagonal
⊢ map Prod.swap (a ::ₘ s).antidiagonal = (a ::ₘ s).antidiagonal

Tactic:
simp only [antidiagonal_cons, map_add, map_map, ← Prod.map_comp_swap,
      ← Multiset.map_map _ Prod.swap, ih, add_comm]

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

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

Tactic:
exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm

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 : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
this : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
⊢ (mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}

Tactic:
by_contra

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
this✝ : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
this : ¬(mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}
⊢ False
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:
fun i ↦ comap_map_eq_self (le_iInf_iff.mp h i)

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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
⊢ (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤

Tactic:
rw [iSup_subtype'] at hp ⊢

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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ x, p ↑x = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
⊢ (⨆ x, comap f (p ↑x)) ⊔ f.ker = ⊤
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ (indicator s f) i = if hi : i ∈ s then f i hi else 0

Tactic:
by
  simp only [indicator, ne_eq, coe_mk]
  congr

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

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

Tactic:
suffices g.support ⊆ s ∧ (∀ i (hi : i ∈ s), f i hi = g i) ↔
      (∀ i, if hi : i ∈ s then f i hi = g i else g i = 0) by
    simp only [this, funext_iff, indicator_apply]
    grind

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
⊢ (Function.support g ⊆ ↑s ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case neg
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∉ Set.range ⇑f
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b

Tactic:
simp only [coe_add, Pi.add_apply, embDomain_of_notMem_range _ _ _ h, add_zero]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
a : Option α
⊢ (optionElim y f) a = a.elim y ⇑f

Tactic:
cases a with

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
a : Option α
⊢ (optionElim y f) a = a.elim y ⇑f

Tactic:
cases a with
  | none => exact optionElim_apply_none y f
  | some x => simp only [optionElim_apply_some, Option.elim_some]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ?m.24

pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ ?m.24 = ∑ b ∈ s, single a (f b)

pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ α →₀ M

Tactic:
· apply single_multiset_sum

Goal state after:
α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ (Multiset.map (single a) (Multiset.map (fun b ↦ f b) s.val)).sum = ∑ b ∈ s, single a (f b)
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: case cons
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : ∀ i ∈ cons a s has, 0 ≤ f i
h1 : ∀ i ∈ cons a s has, f i ≤ g i
⊢ ∏ i ∈ cons a s has, f i ≤ ∏ i ∈ cons a s has, g i

Tactic:
simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    gcongr
    exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
  classical
  calc
      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
        le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod <| by simpa only [mem_sdiff, and_imp]
      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset 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 : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' ↑l.support)
⊢ ∀ (a : α), a ∈ l.support.preimage f hf ↔ l (f a) ≠ 0

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

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
y : M
⊢ (∃ a ∈ f.support, f a = y) ↔ y ≠ 0 ∧ y ∈ Set.range ⇑f

Tactic:
exact ⟨fun ⟨x, hx1, hx2⟩ => ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩, fun ⟨hy, x, hx⟩ =>
    ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ (Multiset.map (fun x ↦ g (f x)) s.val).sum = ∑ x ∈ s, g (f x)

Tactic:
Finset.sum_map_val

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ ∑ a ∈ s, g (f a) = ∑ x ∈ s, g (f x)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
s : Set α
M : Type u_12
inst✝¹ : AddCommMonoid M
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ↑s →₀ M
⊢ ↑((restrictSupportEquiv s M).symm f) = f.extendDomain

Tactic:
restrictSupportEquiv,

Goal state after:
α : Type u_1
s : Set α
M : Type u_12
inst✝¹ : AddCommMonoid M
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ↑s →₀ M
⊢ ↑({ toFun := fun f ↦ subtypeDomain (fun x ↦ x ∈ s) ↑f, invFun := fun f ↦ ⟨f.extendDomain, ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }.symm
        f) =
    f.extendDomain
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case hf
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
⊢ x ∉ insert i s → 1 ≤ f x

Tactic:
h'x

Goal state after:
case hf
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : x ∉ insert i s
⊢ 1 ≤ f x
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
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
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
F G : α → M →ₛₗ[σ] N
⊢ { toFun := fun d ↦ d.sum fun i ↦ ⇑((F + G) i), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun d ↦ d.sum fun i ↦ ⇑(F i), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun d ↦ d.sum fun i ↦ ⇑(G i), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext x y
    simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
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
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
F : S
G : α → M →ₛₗ[σ] N
⊢ { toFun := fun d ↦ d.sum fun i ↦ ⇑((F • G) i), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id S) F • { toFun := fun d ↦ d.sum fun i ↦ ⇑(G i), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext x y
    simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
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
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
F : α → M →ₛₗ[σ] N
⊢ (fun F x ↦ F ∘ₛₗ lsingle x) ((fun F ↦ { toFun := fun d ↦ d.sum fun i ↦ ⇑(F i), map_add' := ⋯, map_smul' := ⋯ }) F) = F

Tactic:
by
    ext x y
    simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
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
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
F : (α →₀ M) →ₛₗ[σ] N
⊢ (fun F ↦ { toFun := fun d ↦ d.sum fun i ↦ ⇑(F i), map_add' := ⋯, map_smul' := ⋯ }) ((fun F x ↦ F ∘ₛₗ lsingle x) F) = F

Tactic:
by
    ext x y
    simp

Goal state after:
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 : α → M
s : Set α
x : M
⊢ x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, (linearCombination R v) l = x

Tactic:
by
  rw [span_image_eq_map_linearCombination]
  simp

Goal state after: