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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0

Tactic:
by
  simp only [ne_eq, p.eq_bot_iff, not_forall, exists_prop]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ -x ∈ p

Tactic:
← neg_one_smul R

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ -1 • x ∈ p
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
h' : ∀ x ∈ p, (f' ^ n) x ∈ p
x : ↥p
⊢ ↑((f'.restrict h ^ n) x) = ↑(((f' ^ n).restrict h') x)

Tactic:
have : Semiconj (↑) (f'.restrict h) f' := fun _ ↦ coe_restrict_apply _ _

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
h' : ∀ x ∈ p, (f' ^ n) x ∈ p
x : ↥p
this : Semiconj Subtype.val ⇑(f'.restrict h) ⇑f'
⊢ ↑((f'.restrict h ^ n) x) = ↑(((f' ^ n).restrict h') x)
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ f (⨆ i, ⨆ j, g i j) = ⨆ i, ⨆ j, f (g i j)

Tactic:
map_iSup

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

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
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 σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
⊢ ∀ (c : R₂) {x : M₂}, x ∈ ⇑f '' ↑p → c • x ∈ ⇑f '' ↑p

Tactic:
rintro c x ⟨y, hy, rfl⟩

Goal state after:
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
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 σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
c : R₂
y : M
hy : y ∈ ↑p
⊢ c • f y ∈ ⇑f '' ↑p
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0⁻¹ ∈ s.centralizer

Tactic:
rw [inv_zero]
    exact zero_mem_centralizer

Goal state after:
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ False

Tactic:
have :=
    NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)

Goal state after:
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : (0, 1) = 0 ∨ (1, 0) = 0
⊢ False
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
inst✝¹ : NonUnitalNonAssocSemiring R✝
M : Subsemigroup R✝
R : Type u_1
inst✝ : NonUnitalSemiring R
⊢ (center.instNonUnitalCommSemiring R).toNonUnitalSemiring = NonUnitalSubsemiringClass.toNonUnitalSemiring (center R)

Tactic:
with_reducible_and_instances rfl

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalRing R
⊢ (center.instNonUnitalCommRing R).toNonUnitalRing = NonUnitalSubringClass.toNonUnitalRing (center R)

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_4
inst✝¹ : Semiring S
inst✝ : Algebra R S
y : R
hy : y ∈ ↑(IsUnit.submonoid R)
⊢ (algebraMap R S) y ∈ IsUnit.submonoid S

Tactic:
exact hy.map _

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
⊢ center.commSemiring.toSemiring = (center R).toSemiring

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FaithfulSMul R A ↔ Injective ⇑(algebraMap R A)

Tactic:
faithfulSMul_iff_injective_smul_one,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (Injective fun r ↦ r • 1) ↔ Injective ⇑(algebraMap R A)
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (Injective fun r ↦ r • 1) ↔ Injective ⇑(algebraMap R A)

Tactic:
Algebra.algebraMap_eq_smul_one'

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (Injective fun r ↦ r • 1) ↔ Injective fun r ↦ r • 1
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 c : M
hc : p * b = a * c
⊢ p ∣ a ∨ a ∣ b

Tactic:
rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)

Goal state after:
case inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b

case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c : Associates M
ha : a ≠ 0
d : Associates M
hd : a * c = a * b * d
⊢ a * c = a * (b * d)

Tactic:
by rwa [← mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
u : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ q = p * x
⊢ DvdNotUnit p (q * ↑u)

Tactic:
refine ⟨hp, x * u, mt isUnit_of_mul_isUnit_left hx.1, ?_⟩

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
u : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ q = p * x
⊢ q * ↑u = p * (x * ↑u)
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ s / 0 ⊆ 0

Tactic:
by simp [subset_def, mem_div]

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ 0 / s ⊆ 0

Tactic:
by simp [subset_def, mem_div]

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

Goal state before:
pp: case closed_under_smul
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
inst✝ : SMulCommClass S R M
r : S
⊢ ∀ ⦃r_1 : S⦄ ⦃n : M⦄, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ r • N

Tactic:
rintro _ m rfl hm

Goal state after:
case closed_under_smul
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
inst✝ : SMulCommClass S R M
r✝ : S
m : M
hm : m ∈ N
⊢ r✝ • m ∈ r✝ • N
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 ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L

Tactic:
simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
⊢ S = {a | a ≤ sSup S ∧ IsAtom a}

Tactic:
ext a
  refine ⟨fun h => ⟨le_sSup h, hS a h⟩, fun ⟨hale, hatom⟩ => ?_⟩
  obtain ⟨b, hbS, hba⟩ := (IsAtom.le_sSup hatom).mp hale
  obtain rfl | rfl := (hS b hbS).le_iff.mp hba
  · simpa using hatom.1
  assumption

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
constructor
  · intro hk s hs hs' h_le
    exact hk s (sSup s) hs hs' (isLUB_sSup s) h_le
  · intro h s u hs hs' hu h_le
    rw [isLUB_iff_sSup_eq] at hu
    rw [← hu] at h_le
    exact h s hs hs' h_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
a : α
f : α → β → M
b : β
⊢ s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a

Tactic:
by_cases h : a ∈ s <;> simp [h]

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
c₁ c₂ : S
x✝¹ : c₁ ∈ span R s
x✝ : c₂ ∈ span R s
ih₁ : c₁ • x ∈ span R (s • t)
ih₂ : c₂ • x ∈ span R (s • t)
⊢ (c₁ + c₂) • x ∈ span R (s • t)

Tactic:
add_smul

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
c₁ c₂ : S
x✝¹ : c₁ ∈ span R s
x✝ : c₂ ∈ span R s
ih₁ : c₁ • x ∈ span R (s • t)
ih₂ : c₂ • x ∈ span R (s • t)
⊢ c₁ • x + c₂ • x ∈ span R (s • t)
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
s : Finset ι
f : ι → G₀
h : ∏ i ∈ s, f i ≠ 0
⊢ mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f ↑i) ⋯

Tactic:
induction s using Finset.cons_induction_on <;> simp [*]

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
⊢ x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → (x✝ + y✝) • y ∈ span R (s • t)

Tactic:
add_smul

Goal state after:
case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
⊢ x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → x✝ • y + y✝ • y ∈ span R (s • t)
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x✝¹ : (i : ι) → M i
x✝ : ι
⊢ (∏ x, mulSingle x (x✝¹ x)) x✝ = x✝¹ x✝

Tactic:
Fintype.prod_apply

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x✝¹ : (i : ι) → M i
x✝ : ι
⊢ ∏ c, mulSingle c (x✝¹ c) x✝ = x✝¹ x✝
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
by_cases hs : a ∈ s

Goal state after:
case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
Module: Mathlib.Data.List.Find

Goal state before:
pp: case swap
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : {x_1 | x_1 ∈ y :: x :: l ∧ p x_1 = true}.Subsingleton
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

Tactic:
dsimp [Set.Subsingleton] at hp

Goal state after:
case swap
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)
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

Tactic:
dsimp [Set.Subsingleton] at hp

Goal state after:
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 → ∀ ⦃y : α⦄, y ∈ x ::ₘ s ∧ p y → x_1 = y
h✝ : p x
⊢ some x = some a ↔ a ∈ x ::ₘ s ∧ p a
Module: Mathlib.Data.Multiset.Find

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

Tactic:
dsimp [Set.Subsingleton] at hp

Goal state after:
case cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = none ↔ ∀ (a : α), a ∈ s → ¬p a
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ x ::ₘ s ∧ p x_1 → ∀ ⦃y : α⦄, y ∈ x ::ₘ s ∧ p y → x_1 = y
⊢ (if h : p x then some x else find? p s ⋯) = none ↔ ∀ (a : α), a ∈ x ::ₘ s → ¬p a
Module: Mathlib.Data.Finsupp.Single

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

Tactic:
classical simp [single_apply, eq_comm]

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
hf : x ∈ f.support
hg : x ∈ g.support
⊢ (f + g) x = (g + f) x

Tactic:
exact h _ (mem_inter_of_mem hf hg)

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (s ∩ t).indicator (fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
← Set.indicator_indicator

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ s.indicator (t.indicator fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i
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 : α
⊢ (Multiset.map (single a) (Multiset.map (fun b ↦ f b) s.val)).sum = ∑ b ∈ s, single a (f b)

Tactic:
rw [Multiset.map_map]

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 ∘ fun b ↦ f b) s.val).sum = ∑ b ∈ s, single a (f b)
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: 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 : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
this : ∀ (y : M), f y = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
by rw [this, this, smul_zero]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
M' : Type u_3
inst✝ : One M'
f : α → M
g : α → M'
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ HasFiniteMulSupport fun a ↦ (f a, g a)

Tactic:
simp only [HasFiniteMulSupport] at hf hg ⊢

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : One M
M' : Type u_3
inst✝ : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport fun a ↦ (f a, g a)).Finite
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_1 = (a, m)) → f a = m ∧ m ≠ 0

pp: case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ f a = m ∧ m ≠ 0 → ∃ a_2, f a_2 ≠ 0 ∧ { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_2 = (a, m)

Tactic:
· rintro ⟨b, ha, rfl, -⟩
    exact ⟨rfl, ha⟩

Goal state after:
case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ f a = m ∧ m ≠ 0 → ∃ a_2, f a_2 ≠ 0 ∧ { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_2 = (a, m)
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulMono R
F : Type u_2
L : Type u_3
inst✝ : FunLike F L R
f : F
r : R
a✝ : List L
hf0 : ∀ (x : L), x ∈ ⟦a✝⟧ → 0 ≤ f x
hf : ∀ (x : L), x ∈ ⟦a✝⟧ → f x ≤ r
⊢ (map ⇑f ⟦a✝⟧).prod ≤ r ^ card ⟦a✝⟧

Tactic:
simp_all [List.prod_map_le_pow_length₀]

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ ∀ (i : ι), i ∈ s → f i ≤ g i

Tactic:
intro i hi
        apply le_of_lt
        apply h
        simp [hi]

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

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
a✝ : x a = 0
⊢ 0 (f a) = 0

Tactic:
coe_zero,

Goal state after:
case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
a✝ : x a = 0
⊢ 0 (f a) = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ (comapDomain f (single (f a) m) hif).support ⊆ {a} ∧ (comapDomain f (single (f a) m) hif) a = m

Tactic:
comapDomain_apply,

Goal state after:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ (comapDomain f (single (f a) m) hif).support ⊆ {a} ∧ (single (f a) m) (f a) = m
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
a✝ : α
⊢ (comapDomain f (mapDomain f l) ⋯) a✝ = l a✝

Tactic:
comapDomain_apply,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
a✝ : α
⊢ (mapDomain f l) (f a✝) = l a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p 0 = 0

Tactic:
rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x

Tactic:
have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι : Type u_4
M : Type u_5
N : Type u_6
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : AddCommMonoid N
f : (i : ι) × αs i → M → N
⊢ l.sum f = ∑ i ∈ l.splitSupport, (l.split i).sum fun a b ↦ f ⟨i, a⟩ b

Tactic:
simp only [sum, sigma_support, sum_sigma, split_apply]

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

Goal state before:
pp: case e_g
α : 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✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m✝ : ι →₀ M
i : ι
m : M
⊢ f (single i (r • m)) = r • f (single i m)

Tactic:
exact (f.comp <| lsingle i).map_smul_of_tower r m

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
⊢ l ∈ ⊥

Tactic:
simp only [mem_bot]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
⊢ l = 0
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
l : α →₀ R
s : Finset α
hs : l ∈ supported R R ↑s
x : α
x✝ : x ∈ s
hxg : x ∉ l.support
⊢ l x • v x = 0

Tactic:
notMem_support_iff.1 hxg,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
l : α →₀ R
s : Finset α
hs : l ∈ supported R R ↑s
x : α
x✝ : x ∈ s
hxg : x ∉ l.support
⊢ 0 • v x = 0
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ succ '' Iio i = Ioo 0 i.succ

Tactic:
refine Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_lt_succ_iff.2 hj⟩) ?_

Goal state after:
n : ℕ
i : Fin n
⊢ Ioo 0 i.succ ⊆ succ '' Iio i