mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
σ : R →+* R
ι : Sort u_9
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
⊢ ∀ (v : M), (∀ (i : ι), v ∈ p i) → ∀ (i : ι), f v ∈ p i

Tactic:
exact fun v a i ↦ hf i v (a i)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ x
d : M
hd : x = p * d
⊢ a = p ^ (k + 1) * d

Tactic:
by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ y
d : M
hd : y = p * d
⊢ b = p ^ (l + 1) * d

Tactic:
by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]

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✝ e : A₁ ≃ₐ[R] A₂
r : R
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂) r) = (algebraMap R A₁) r

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

Goal state after:
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) = e.toRingEquiv.symm (e.toRingEquiv ((algebraMap R A₁) r))
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₁
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass S R M₁
inst✝³ : SMulCommClass S R M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M₁
inst✝ : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x✝ : R
⊢ e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁)) x✝) = (algebraMap R (Module.End S M₂)) x✝

Tactic:
by ext; change e.restrictScalars R _ = _; simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p₁ p₂ : Submodule R ↥p
⊢ ↑({ toFun := fun p' ↦ ⟨map p.subtype p', ⋯⟩, invFun := fun q ↦ comap p.subtype ↑q, left_inv := ⋯, right_inv := ⋯ }
          p₁) ≤
      ↑({ toFun := fun p' ↦ ⟨map p.subtype p', ⋯⟩, invFun := fun q ↦ comap p.subtype ↑q, left_inv := ⋯, right_inv := ⋯ }
          p₂) ↔
    p₁ ≤ p₂

Tactic:
dsimp

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p₁ p₂ : Submodule R ↥p
⊢ map p.subtype p₁ ≤ map p.subtype p₂ ↔ p₁ ≤ p₂
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y, O.subtype y ∈ N ∧ ϕ y = x

Tactic:
rintro ⟨y, yO, yN, h⟩

Goal state after:
case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : ϕ ⟨y, yO⟩ = x
⊢ ∃ y, O.subtype y ∈ N ∧ ϕ y = x
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: 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
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄, r ∈ s → ∀ a ∈ N, r • a ∈ p} = {x | ∀ i ∈ s, i • N ≤ x}

Tactic:
exact Set.ext fun _ => forall₂_congr (fun _ _ => Iff.symm map_le_iff_le_comap)

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
N : Submodule R M
x✝ : M
⊢ x✝ ∈ ∅ • N → x✝ ∈ ⊥

pp: case mpr
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
N : Submodule R M
x✝ : M
⊢ x✝ ∈ ⊥ → x✝ ∈ ∅ • N

Tactic:
· intro hx
    rw [mem_set_smul_def, Submodule.mem_sInf] at hx
    exact hx ⊥ (fun r _ hr ↦ hr.elim)

Goal state after:
case mpr
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
N : Submodule R M
x✝ : M
⊢ x✝ ∈ ⊥ → x✝ ∈ ∅ • N
Module: Mathlib.Order.ModularLattice

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

Tactic:
dsimp

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

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

Tactic:
dsimp

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

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (x ⊔ y) ≤ c (c x ⊔ y)

Tactic:
← c.le_closure x

Goal state after:
α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (x ⊔ y) ≤ c (x ⊔ y)
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
this : l a' = l a
haa' : a = a'
⊢ IsAtom a

Tactic:
exact haa'.symm ▸ ha'

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
by
  classical
    rw [isCompactElement_iff_le_of_directed_sSup_le]
    constructor
    · intro hk s hsup
      -- Consider the set of finite joins of elements of the (plain) set s.
      let S : Set α := { x | ∃ t : Finset α, ↑t ⊆ s ∧ x = t.sup id }
      -- S is directed, nonempty, and still has sup above k.
      have dir_US : DirectedOn (· ≤ ·) S := by
        rintro x ⟨c, hc⟩ y ⟨d, hd⟩
        use x ⊔ y
        constructor
        · use c ∪ d
          constructor
          · simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
          · simp only [hc.right, hd.right, Finset.sup_union]
        simp only [and_self_iff, le_sup_left, le_sup_right]
      have sup_S : sSup s ≤ sSup S := by
        apply sSup_le_sSup
        intro x hx
        use {x}
        simpa only [and_true, id, Finset.coe_singleton, eq_self_iff_true,
          Finset.sup_singleton, Set.singleton_subset_iff]
      have Sne : S.Nonempty := by
        suffices ⊥ ∈ S from Set.nonempty_of_mem this
        use ∅
        simp
      -- Now apply the defn of compact and finish.
      obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
      obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
      use t
      exact ⟨htS, by rwa [← htsup]⟩
    · intro hk s hne hdir hsup
      obtain ⟨t, ht⟩ := hk s hsup
      -- certainly every element of t is below something in s, since ↑t ⊆ s.
      have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
      obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
      exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩

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

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

Tactic:
rw [Finset.sup_empty] at ht₂
    rw [ht₂]
    simp [eq_singleton_bot_of_sSup_eq_bot_of_nonempty ht₂ hne]

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

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

Tactic:
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc

Goal state after:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b
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:
Submodule.span_image

Goal state after:
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 ∈ map f (span R s)
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
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
⊢ ∃ x_1 ∈ d, R ∙ x ≤ x_1

Tactic:
have : x ∈ (sSup d) := (SetLike.le_def.mp hsup) (mem_span_singleton_self x)

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
this : x ∈ sSup d
⊢ ∃ x_1 ∈ d, R ∙ x ≤ x_1
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Iic b }
hc : IsCompl ⟨sSup {a | IsAtom a ∧ a ≤ b}, hle⟩ c
a : { x // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ False

Tactic:
· apply ha.1
        rw [eq_bot_iff]
        apply le_trans (le_inf _ hac) hc.disjoint.le_bot
        rw [← Subtype.coe_le_coe, Subtype.coe_mk]
        exact le_sSup ⟨ha.of_isAtom_coe_Iic, a.2⟩

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 ⋯)
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
v : ι
hv : v ∈ s
⊢ a ≠ ↑⟨v, hv⟩

Tactic:
rintro rfl; exact ha hv

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
⊢ f a = g a

Tactic:
have hf : f a = 0 := notMem_support_iff.1 h

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
⊢ f a = g a
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
b : β
⊢ (embDomain f v) b = if h : ∃ a, f a = b then v h.choose else 0

Tactic:
simp only [embDomain, coe_mk]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
b : β
⊢ (match Multiset.find? (fun a ↦ f a = b) v.support.val ⋯ with
    | some a => v a
    | none => 0) =
    if h : ∃ a, f a = b then v h.choose else 0
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
⊢ single a ((single a' b) a) = (single a' (single a' b)) a

Tactic:
by
  classical
  grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ (single a b).support ⊆ {a}

Tactic:
by
  classical
  grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
x : α
⊢ (single a b) x ∈ {0, b}

Tactic:
by
  classical
  grind

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (f + single a b).support = cons a f.support ha

Tactic:
by
  classical
  have H := support_single a hb
  rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_right]

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

Goal state before:
pp: α : Type u_1
N : Type u_7
P : Type u_8
inst✝¹ : Zero N
inst✝ : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
⊢ e ((single a n) b) = (single a (e n)) b

Tactic:
by
  classical
  grind

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
j : ι
h : j ≠ a
⊢ (f.update a b) j = (single a b + erase a f) j

Tactic:
· simp [h, erase_ne]

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
j : ι
h : j ≠ a
⊢ (f.update a b) j = (erase a f + single a b) j

Tactic:
· simp [h, erase_ne]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
⊢ f.update a (f a) = f

Tactic:
by
  classical
  grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a₁ a₂ : α
h : a₁ ≠ a₂
m₁ m₂ : M
⊢ (f.update a₁ m₁).update a₂ m₂ = (f.update a₂ m₂).update a₁ m₁

Tactic:
by
  classical
  grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b c : M
⊢ (f.update a b).update a c = f.update a c

Tactic:
by
  classical
  grind

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

Goal state before:
pp: case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ a ∉ f.support.erase a

Tactic:
mem_erase

Goal state after:
case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
⊢ zipWith f hf (single a m) (single a n) = single a (f m n)

Tactic:
by
  classical
  grind

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
⊢ motive f

Tactic:
have hs' : (erase a f).support = s := by
      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
    rw [← single_add_erase a f]
    refine single_add _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
    rw [← mem_support_iff, hs]
    exact mem_insert_self a s

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

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

Tactic:
simp [Finsupp.update]

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

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
⊢ ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P)) none = P none

Tactic:
simp [Finsupp.update]

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

Goal state before:
pp: case some
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
a : α
⊢ ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P)) (Option.some a) =
    P (Option.some a)

Tactic:
simp [Finsupp.update]

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

Goal state before:
pp: case fst
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
⊢ ((fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P)).1 = P.1

Tactic:
simp [Finsupp.update]

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

Goal state before:
pp: case snd
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
a✝ : α
⊢ ((fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P)).2 a✝ = P.2 a✝

Tactic:
simp [Finsupp.update]

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

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

Tactic:
rw [mulIndicator_of_notMem hx]

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ i, s i
⊢ 1 = ⨆ i, (s i).mulIndicator f x
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ i, s i
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x

Tactic:
rw [mulIndicator_of_notMem hx]

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ i, s i
⊢ 1 = ⨅ i, (s i).mulIndicator f x
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

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

pp: case neg
α : 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
hyf : y ∉ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
· exact Finsupp.mul_prod_erase f y g hyf

Goal state after:
case neg
α : 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
hyf : y ∉ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s✝ : Multiset M
a✝ : α
a : M
s : Multiset M
ih : single a✝ s.sum = (Multiset.map (single a✝) s).sum
⊢ single a✝ a + (Multiset.map (single a✝) s).sum = (Multiset.map (single a✝) (a ::ₘ s)).sum

Tactic:
Multiset.map_cons,

Goal state after:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s✝ : Multiset M
a✝ : α
a : M
s : Multiset M
ih : single a✝ s.sum = (Multiset.map (single a✝) s).sum
⊢ single a✝ a + (Multiset.map (single a✝) s).sum = (single a✝ a ::ₘ Multiset.map (single a✝) s).sum
Module: Mathlib.Algebra.GroupWithZero.Indicator

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

Tactic:
by
  classical simp [indicator_apply, imp_false]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = (Multiset.map (fun g ↦ g.sum h) s).sum
⊢ (a + s.sum).sum h = (Multiset.map (fun g ↦ g.sum h) (a ::ₘ s)).sum

Tactic:
Multiset.map_cons,

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = (Multiset.map (fun g ↦ g.sum h) s).sum
⊢ (a + s.sum).sum h = (a.sum h ::ₘ Multiset.map (fun g ↦ g.sum h) s).sum
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case cons
R : Type u_5
S : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : PartialOrder S
abv : AbsoluteValue R S
inst✝ : AddLeftMono S
head : R
tail : List R
ih : abv tail.sum ≤ (List.map (⇑abv) tail).sum
⊢ abv (head :: tail).sum ≤ (List.map (⇑abv) (head :: tail)).sum

Tactic:
| cons head tail ih =>

Goal state after: