mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.zero_left
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝ x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ 0 * x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
| zero_left =>

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p : M
hp : Irreducible p
q' : M
hq : Irreducible (p * q')
⊢ p * q' ∣ p

Tactic:
rw [IsUnit.mul_right_dvd (Or.resolve_left (of_irreducible_mul hq) hp.not_isUnit)]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

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

Tactic:
← u.isUnit_units_mul

Goal state after:
case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit (↑u * A) ∨ IsUnit B
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)

Goal state after:
case succ.inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : p * q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

case succ.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g ∘ₛₗ f = 0
x : M₂
hx : x ∈ f.range
y : M
hy : f y = x
⊢ (g ∘ₛₗ f) y = 0

Tactic:
h,

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g ∘ₛₗ f = 0
x : M₂
hx : x ∈ f.range
y : M
hy : f y = x
⊢ 0 y = 0
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
⊢ f - (f ∘ₗ g) ∘ₗ f = 0

Tactic:
h,

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
⊢ f - id ∘ₗ f = 0
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₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁' →ₐ[R] A₂'
⊢ (↑e₂).comp ((↑e₂.symm).comp (f.comp (AlgHom.id R A₁'))) = f

Tactic:
simp only [← AlgHom.comp_assoc, comp_symm, AlgHom.id_comp, AlgHom.comp_id]

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
x y : M
⊢ (∃ a, a • y = x) → x ∈ R ∙ y

Tactic:
rintro ⟨a, y, rfl⟩

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : M
a : R
⊢ a • y ∈ R ∙ y
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ ∀ (y : ι), update v j (v j + r • v i) y ∈ span R (range v)

Tactic:
intro k

Goal state after:
case refine_1
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
⊢ update v j (v j + r • v i) k ∈ span R (range v)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ ∀ (y : ι), v y ∈ span R (range (update v j (v j + r • v i)))

Tactic:
intro k

Goal state after:
case refine_2
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
⊢ v k ∈ span R (range (update v j (v j + r • v i)))
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
⊢ (∃ a, IsAtom a ∧ a ≤ y) → ∃ a, IsCoatom a ∧ x ≤ a

Tactic:
rintro ⟨a, ha, ay⟩

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
⊢ ∃ a, IsCoatom a ∧ x ≤ a
Module: Mathlib.Order.SupIndep

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

Tactic:
h,

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
ht : Disjoint (t j) (t j)
⊢ t j = ⊥
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ s.mulIndicator ((mulSupport f).mulIndicator f) = s.mulIndicator f

Tactic:
mulIndicator_mulSupport

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ s.mulIndicator f = s.mulIndicator f
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : ℕ →o α
⊢ sSup (range ⇑a) ∈ range ⇑a

Tactic:
by
    apply h _ (range_nonempty a)
    rintro x ⟨m, rfl⟩ y ⟨n, rfl⟩
    exact ⟨_, map_sup a m n⟩

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap R S)
f : A →ₐ[R] B
⊢ ∀ (r : S), (↑↑f.toRingHom).toFun ((algebraMap S A) r) = (algebraMap S B) r

Tactic:
by simp [h.forall, ← IsScalarTower.algebraMap_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
⊢ (U.mulIndicator fun x ↦ a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}

Tactic:
classical
    rw [mulIndicator_const_preimage_eq_union]
    split_ifs <;> simp

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
r : M
s : Set α
f : α → M
⊢ r ∈ range (s.mulIndicator f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s

Tactic:
by
  simp [mulIndicator, ite_eq_iff, exists_or, eq_univ_iff_forall, and_comm, or_comm,
    @eq_comm _ r 1]

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
⊢ (∏ x ∈ s.erase i, f x) * f i = 0

Tactic:
h,

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝ : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
⊢ (∏ x ∈ s.erase i, f x) * 0 = 0
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
t : β
ht : t ∈ s
⊢ (∏ i ∈ v, f i) t = (∏ i ∈ v, f' i) t

Tactic:
by simp [funext fun i ↦ h i ht]

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

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
⊢ (∃ (hx : x ∈ ⨆ i, p i), motive x hx) →
    (∃ (hx : y ∈ ⨆ i, p i), motive y hx) → ∃ (hx : x + y ∈ ⨆ i, p i), motive (x + y) hx

Tactic:
· rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, add _ _ _ _ Cx Cy⟩

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

Goal state before:
pp: case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
b✝ : (i : ι) → κ i
a✝¹ : b✝ ∈ s
a✝ : b✝ i ∈ Finset.image (fun x ↦ x i) s
⊢ ⨅ i, f i (b✝ i) ≤ f i (b✝ i)

Tactic:
exact iInf_le _ _

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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p : Submodule R₂ M₂
⊢ IsCoatom (comap f p) ↔ IsCoatom p

Tactic:
by
  have := comap_injective_of_surjective hf
  rw [IsCoatom, IsCoatom, ← comap_top f, this.ne_iff]
  refine and_congr_right fun _ ↦
    ⟨fun h m hm ↦ this (h _ <| comap_strictMono_of_surjective hf hm), fun h m hm ↦ ?_⟩
  rw [← h _ (lt_map_of_comap_lt_of_surjective hf hm),
    comap_map_eq_self ((comap_mono bot_le).trans hm.le)]

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

Goal state before:
pp: case inr
α : 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)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
h,

Goal state after:
case inr
α : 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)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ Disjoint x (sSup (s \ {x} ∪ {a}))
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)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ sSup (insert x (s \ {x})) ≤ sSup s

Tactic:
Set.insert_sdiff_singleton,

Goal state after:
α : 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)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ sSup (insert x s) ≤ sSup s
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₂
S : Submodule R M
⊢ (f.domRestrict S).range = f.range ↔ Codisjoint S f.ker

Tactic:
simp [map_eq_range_iff]

Goal state after:
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case cons.isTrue
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = some a ↔ a ∈ s ∧ p a
hp : {x_1 | x_1 ∈ x ::ₘ s ∧ p x_1}.Subsingleton
h✝ : p x
⊢ some x = some a ↔ a ∈ x ::ₘ s ∧ p a

pp: case cons.isFalse
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = some a ↔ a ∈ s ∧ p a
hp : {x_1 | x_1 ∈ x ::ₘ s ∧ p x_1}.Subsingleton
h✝ : ¬p x
⊢ find? p s ⋯ = some a ↔ a ∈ x ::ₘ s ∧ p a

Tactic:
· dsimp [Set.Subsingleton] at hp
      specialize hp ⟨mem_cons_self _ _, ‹p x›⟩
      grind

Goal state after:
case cons.isFalse
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = some a ↔ a ∈ s ∧ p a
hp : {x_1 | x_1 ∈ x ::ₘ s ∧ p x_1}.Subsingleton
h✝ : ¬p x
⊢ find? p s ⋯ = some a ↔ a ∈ x ::ₘ s ∧ p a
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Tactic:
classical simp only [add_comm (1 : R), prod_add, prod_const_one, mul_one]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
⊢ ∏ i ∈ insert a s, (f i + g i) =
    ∏ i ∈ insert a s, f i +
      ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j

Tactic:
have ha' : a ∉ s := fun ha' => lt_irrefl a (ha a ha')

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ ∏ i ∈ insert a s, (f i + g i) =
    ∏ i ∈ insert a s, f i +
      ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Submodule R M
x : M
⊢ Disjoint (R ∙ x) s ↔ ∀ (r : R), r • x ∈ s → r • x = 0

Tactic:
simp +contextual [disjoint_def, mem_span_singleton]

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
f₂ : N ≃ O
hf₂ : f₂ 0 = 0
⊢ (e.trans f₂) 0 = 0

Tactic:
by rw [Equiv.trans_apply, hf, hf₂]

Goal state after:
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
a : α
⊢ { support := map f v.support,
        toFun := fun b ↦
          match Multiset.find? (fun a ↦ f a = b) v.support.val ⋯ with
          | some a => v a
          | none => 0,
        mem_support_toFun := ⋯ }
      (f a) =
    v a

Tactic:
coe_mk

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
g : ι → α
i : ι
⊢ (indicator s fun i x ↦ g i) i = (↑s).indicator g i

Tactic:
simp [indicator_apply, Set.indicator_apply]

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ b₁ = b₂

Tactic:
h,

Goal state after:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₂ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ b₁ = b₂
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ (single f₁ g₁ + single f₂ g₂).support = {f₁, f₂}

Tactic:
by
  rw [support_add_eq, support_single _ hg₁, support_single _ hg₂]
  · simp
  · simp [support_single, *]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : Nonempty α
f : α →₀ M
⊢ #f.support ≤ 1 ↔ ∃ a, f = single a (f a)

Tactic:
simp only [card_le_one_iff_subset_singleton, support_subset_singleton]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a a' : α
f : α →₀ M
⊢ { support := f.support.erase a, toFun := fun a' ↦ if a' = a then 0 else f a', mem_support_toFun := ⋯ } a' =
    if a' = a then 0 else f a'

Tactic:
coe_mk

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a a' : α
f : α →₀ M
⊢ (if a' = a then 0 else f a') = if a' = a then 0 else f a'
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : 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
⊢ (embDomain f l).support = {a}

Tactic:
h,

Goal state after:
α : 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
⊢ (single a b).support = {a}
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 = Option.elim' y (⇑f) a

Tactic:
rw [optionElim_apply_eq_elim, Option.elim'_eq_elim]

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✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
classical exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a

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

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun a ↦ r a • f a) a = r a • s.indicator f a

Tactic:
by
  dsimp only [indicator]
  split_ifs
  exacts [rfl, (smul_zero (r a)).symm]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, { support := if m = 0 then ∅ else {j}, toFun := Pi.single j m, mem_support_toFun := ⋯ } i = m

Tactic:
coe_mk

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x, Pi.single x m i = m
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
inst✝ : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : (s.sup' hs fun x ↦ f x a) ≠ 1
⊢ ∃ i ∈ s, f i a ≠ 1

Tactic:
contrapose! ha

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : One M
inst✝ : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : ∀ i ∈ s, f i a = 1
⊢ (s.sup' hs fun x ↦ f x a) = 1
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
inst✝ : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : (s.inf' hs fun x ↦ f x a) ≠ 1
⊢ ∃ i ∈ s, f i a ≠ 1

Tactic:
contrapose! ha

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : One M
inst✝ : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : ∀ i ∈ s, f i a = 1
⊢ (s.inf' hs fun x ↦ f x a) = 1
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Monoid M
f : α → M
g : α → ℕ
hg : HasFiniteSupport g
a : α
ha : a ∈ mulSupport fun a ↦ f a ^ g a
⊢ a ∈ support g

Tactic:
contrapose! ha

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Monoid M
f : α → M
g : α → ℕ
hg : HasFiniteSupport g
a : α
ha : a ∉ support g
⊢ a ∉ mulSupport fun a ↦ f a ^ g a
Module: Mathlib.Data.Finsupp.Basic

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

Tactic:
h,

Goal state after:
α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ image Prod.fst g.graph = g.support
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:
rw [Finset.mem_preimage]

Goal state after:
α : 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 : α
⊢ f a ∈ l.support ↔ l (f a) ≠ 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hf : Injective f
⊢ Surjective fun l ↦ comapDomain f l ⋯

Tactic:
intro l'
  use l'.embDomain ⟨f, hf⟩
  exact Finsupp.comapDomain_embDomain ..

Goal state after: