mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_2.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
hx : IsUnit x
hy : Prime y
⊢ Prime (x * y)

Tactic:
exact (associated_unit_mul_right y x hx).prime hy

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ Associates.mk (Quot.out (Associates.mk a)) = Associates.mk a

Tactic:
Associates.quot_out

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
⊢ Associates.mk a = Associates.mk a
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 τ₁₂
K : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (f.domRestrict K).range = map f K

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
⊢ 0⁻¹ = 0

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ e.trans e.symm = refl

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ e.symm.trans e = refl

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
inst✝² : CommSemiring R
inst✝¹ : Semiring A₁
inst✝ : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n : ℕ
⊢ ⇑(e ^ Nat.zero) = (⇑e)^[Nat.zero]

Tactic:
by ext; simp

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

Goal state before:
pp: K : Type u_4
V : Type u_8
V₂ : Type u_9
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
⊢ (a • f).range = ⨆ (_ : a ≠ 0), f.range

Tactic:
simpa only [range_eq_map] using Submodule.map_smul' f _ a

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
⊢ ∀ (c : ↥q), (p.subtype.domRestrict q) c ∈ map p.subtype q

Tactic:
by rintro ⟨x, hx⟩; exact ⟨x, hx, rfl⟩

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
p : Submodule R M
⊢ -restrictScalars S p = restrictScalars S (-p)

Tactic:
by ext; simp

Goal state after:
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
α : Type u_4
inst✝⁴ : Monoid α
inst✝³ : SMul α R
inst✝² : DistribMulAction α M
inst✝¹ : SMulCommClass α R M
inst✝ : IsScalarTower α R M
a : α
S : Submodule R M
⊢ a • S ≤ S

Tactic:
rintro y ⟨x, hx, rfl⟩
  exact smul_of_tower_mem _ a hx

Goal state after:
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
s t : Set M
hst : Disjoint (span R s) (span R t)
⊢ Disjoint (s \ {0}) t

Tactic:
rw [disjoint_iff_forall_ne]
  rintro v ⟨hvs, hv0 : v ≠ 0⟩ _ hvt rfl
  exact hv0 <| (disjoint_def.1 hst) v (subset_span hvs) (subset_span hvt)

Goal state after:
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
s : Set (Submodule R M)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

Tactic:
by
  have : Nonempty s := hs.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed _ hdir.directed_val, SetCoe.exists,
    exists_prop]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L

Tactic:
and_congr_right_iff,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ x ∉ K, x ∈ H ∧ H ≠ L)
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K

Tactic:
and_congr_right_iff,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x ∉ H, x ∈ L ∧ H ≠ K)
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) ⊥) = ⊥

Tactic:
simp [bot_ne_top]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) ⊤) = ⊤

Tactic:
simp [bot_ne_top]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case false
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ decide (x = ⊤)) ((fun x ↦ Bool.casesOn x ⊥ ⊤) false) = false

Tactic:
simp [bot_ne_top]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case true
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ decide (x = ⊤)) ((fun x ↦ Bool.casesOn x ⊥ ⊤) true) = true

Tactic:
simp [bot_ne_top]

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

Goal state before:
pp: case insert
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH : ↑t ⊆ ↑(span R s) → ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)
ht : ↑(insert a t) ⊆ ↑(span R s)
⊢ ∃ T, ↑T ⊆ s ∧ ↑(insert a t) ⊆ ↑(span R ↑T)

Tactic:
obtain ⟨T, hTs, htT⟩ := IH (by simp_all [Set.insert_subset_iff])
    obtain ⟨T', hT's, haT'⟩ := mem_span_finite_of_mem_span (ht (Finset.mem_insert_self _ _))
    refine ⟨T ∪ T', by simp_all, ?_⟩
    simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_subset_iff, SetLike.mem_coe]
    exact ⟨mem_sup_right haT', htT.trans (le_sup_left (a := span R _))⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
⊢ ∃ s_1, IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a

Tactic:
refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp +contextual⟩
    rw [isLUB_pi]
    intro i
    simp_rw [isAtom_iff_eq_single]
    refine ⟨?_, ?_⟩
    · rintro _ ⟨_, ⟨⟨_, _, _, rfl⟩, hs⟩, rfl⟩
      exact hs i
    · refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_
      exact hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, by simp [update_le_iff, hx₂]⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ iSupIndep Subtype.val

Tactic:
← coe_comp_rangeFactorization t

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep (Subtype.val ∘ rangeFactorization t)
⊢ iSupIndep Subtype.val
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s ↦ ⨆ i ∈ s, f i
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (range g)

Tactic:
rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s ↦ ⨆ i ∈ s, f i
s t : Finset ι
⊢ ∃ z ∈ range g, (fun x1 x2 ↦ x1 ≤ x2) (g s) z ∧ (fun x1 x2 ↦ x1 ≤ x2) (g t) z
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
h1 : s.mulIndicator f = f
h2 : s ⊆ t
⊢ t.mulIndicator f = f

Tactic:
rw [mulIndicator_eq_self] at h1 ⊢

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
h1 : mulSupport f ⊆ s
h2 : s ⊆ t
⊢ mulSupport f ⊆ t
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝¹ : One M
h : M → β
f : α → M
s : Set α
x : α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x

Tactic:
by
  let := Classical.decPred (· ∈ s)
  convert! s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2

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

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

Tactic:
obtain ⟨t, ⟨hts, htsup⟩⟩ := h (sSup s) s (by rfl)

Goal state after:
case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
this : Disjoint x (sSup ((↑t ∪ {x}) \ {x}))
⊢ x ⊓ sSup s = ⊥

Tactic:
simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
⊢ ⇑1 = 1

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) (s.sup id)

Tactic:
← Finset.sup_erase_bot

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) ((s.erase ⊥).sup id)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) (s.sup id)

Tactic:
← Finset.sup_erase_bot

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) ((s.erase ⊥).sup id)
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
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
⊢ ⊤.prod ⊤ = ⊤

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
⊢ {i}.mulIndicator f = Pi.mulSingle i (f i)

Tactic:
ext j

Goal state after:
ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
⊢ {i}.mulIndicator f j = Pi.mulSingle i (f i) j
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:
by
  induction h with
  | nil => rfl
  | cons x _ ih =>
    grind
  | swap x y l =>
    dsimp [Set.Subsingleton] at hp
    by_cases p x <;> by_cases p y <;> grind
  | trans _ _ ih1 ih2 =>
    refine (ih1 ?_).trans (ih2 ?_) <;> grind

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ onFinset f.support ⇑f ⋯ = f

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
x : ι →₀ M
⊢ mapRange ⇑e.symm ⋯ (mapRange (⇑e) hf x) = x

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
x : ι →₀ N
⊢ mapRange (⇑e) hf (mapRange ⇑e.symm ⋯ x) = x

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_3
M : Type u_4
inst✝ : Zero M
⊢ equiv (Equiv.refl M) ⋯ = Equiv.refl (ι →₀ M)

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
f₂ : N ≃ O
hf₂ : f₂ 0 = 0
⊢ equiv (e.trans f₂) ⋯ = (equiv e hf).trans (equiv f₂ hf₂)

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
⊢ indicator {a} f = single a (f a ⋯)

Tactic:
ext j

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
j : ι
⊢ (indicator {a} f) j = (single a (f a ⋯)) j
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : Zero M
⊢ zeroHom (ZeroHom.id M) = ZeroHom.id (ι →₀ M)

Tactic:
by ext; simp

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) a = b

Tactic:
by
  classical exact Pi.single_eq_same (M := fun _ ↦ M) a b

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = single a b + erase a f

Tactic:
ext j

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
j : ι
⊢ (f.update a b) j = (single a b + erase a f) j
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = erase a f + single a b

Tactic:
ext j

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
j : ι
⊢ (f.update a b) j = (erase a f + single a b) j
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
h : f a = 0
b : M
⊢ f.update a b = f + single a b

Tactic:
rw [update_eq_erase_add_single, erase_of_notMem_support (by simpa)]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
f : N →+ O
g : M →+ N
⊢ addMonoidHom (f.comp g) = (addMonoidHom f).comp (addMonoidHom g)

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
⊢ addEquiv (AddEquiv.refl M) = AddEquiv.refl (ι →₀ M)

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
e₁ : M ≃+ N
e₂ : N ≃+ O
⊢ addEquiv (e₁.trans e₂) = (addEquiv e₁).trans (addEquiv e₂)

Tactic:
by ext; simp

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

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

Tactic:
some_apply

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (embDomain Embedding.some f) (Option.some a✝) = f a✝
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
x : M
⊢ f x = 0

Tactic:
rw [← smul_inv_smul₀ hR x, map_natCast_smul f R S, hS, zero_smul]

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

Goal state before:
pp: case add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ (f₁ + f₂).prod b = b none ((f₁ + f₂) none) * (f₁ + f₂).some.prod fun a ↦ b (Option.some a)

Tactic:
rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]
      · simp only [h_add, Pi.add_apply, Finsupp.coe_add]
        rw [mul_mul_mul_comm]
      all_goals simp [h_zero, h_add]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : α → M →+ N
⊢ (fun F x ↦ F.comp (singleAddHom x))
      ((fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ }) F) =
    F

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : (α →₀ M) →+ N
⊢ (fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ })
      ((fun F x ↦ F.comp (singleAddHom x)) F) =
    F

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G✝ : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F G : α → M →+ N
⊢ { toFun := fun f ↦ f.sum fun x ↦ ⇑((F + G) x), map_zero' := ⋯, map_add' := ⋯ } =
    { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ } +
      { toFun := fun f ↦ f.sum fun x ↦ ⇑(G x), map_zero' := ⋯, map_add' := ⋯ }

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst (map { toFun := fun a ↦ (a, f a), inj' := ⋯ } f.support) = f.support

Tactic:
map_eq_image,

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst (image (⇑{ toFun := fun a ↦ (a, f a), inj' := ⋯ }) f.support) = f.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
⊢ mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) l) = erase 0 l

Tactic:
refine .trans ?_ (mapDomain_comapDomain _ (add_left_injective 1) _ fun _ ↦ ?_)

Goal state after:
case refine_1
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
⊢ mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) l) =
    mapDomain (fun x ↦ x + 1) (comapDomain (fun x ↦ x + 1) (erase 0 l) ⋯)

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
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✝ : AddZeroClass M
x✝¹ x✝ : α × β →₀ M
⊢ curryEquiv.toFun (x✝¹ + x✝) = curryEquiv.toFun x✝¹ + curryEquiv.toFun x✝

Tactic:
by ext; simp

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

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
a : α
⊢ lapply a ∘ₗ lsingle a = LinearMap.id

Tactic:
by ext; simp

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

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₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
x y : β →₀ M
⊢ comapDomain f (x + y) ⋯ = comapDomain f x ⋯ + comapDomain f y ⋯

Tactic:
by ext; simp

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

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₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
c : R
x : β →₀ M
⊢ comapDomain f (c • x) ⋯ = (RingHom.id R) c • comapDomain f x ⋯

Tactic:
by ext; simp

Goal state after: