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

Goal state before:
pp: case mem.mul
R : Type u
inst✝ : NonAssocRing R
s : Set R
x✝¹ x x✝ y✝ : R
hx✝ : x✝ ∈ Submonoid.closure s
hy✝ : y✝ ∈ Submonoid.closure s
h₁ : x✝ ∈ closure s
h₂ : y✝ ∈ closure s
⊢ x✝ * y✝ ∈ closure s

Tactic:
exact mul_mem h₁ h₂

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

Goal state before:
pp: case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ a ^ 0
⊢ p ∣ a

Tactic:
rw [pow_zero] at h
    have := isUnit_of_dvd_one h
    have := not_isUnit hp
    contradiction

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

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

Tactic:
Units.mul_inv_cancel_right

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
x y : M
⊢ Irreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x

Tactic:
by
  constructor
  · refine fun h => Or.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) (h.isUnit_or_isUnit rfl).symm
    · rwa [irreducible_mul_isUnit h'] at h
    · rwa [irreducible_isUnit_mul h'] at h
  · rintro (⟨ha, hb⟩ | ⟨hb, ha⟩)
    · rwa [irreducible_mul_isUnit hb]
    · rwa [irreducible_isUnit_mul ha]

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

Goal state before:
pp: case mpr.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
hy : IsUnit y
⊢ y ∣ x

pp: case mpr.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x

Tactic:
· exact hy.dvd

Goal state after:
case mpr.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰

Tactic:
rw [mem_nonZeroDivisors_iff_right, mem_nonZeroDivisors_iff_right]

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ∀ (x : M₀), x * a = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mp.mk.refine_2
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x ≠ 0

Tactic:
· rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
h : p * b ~ᵤ p
hp : p ≠ 0
⊢ IsUnit b

Tactic:
by
  obtain ⟨a, ha⟩ := h
  refine .of_mul_eq_one a ((mul_right_inj' hp).mp ?_)
  rwa [← mul_assoc, mul_one]

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
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
⊢ r • m ∈ s • N

Tactic:
mem_set_smul_def,

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
⊢ r • m ∈ sInf {p | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}
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
hx : x✝ ∈ ∅ • N
⊢ x✝ ∈ ⊥

Tactic:
mem_set_smul_def,

Goal state after:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
x✝ : M
hx : x✝ ∈ sInf {p | ∀ ⦃r : S⦄ {n : M}, r ∈ ∅ → n ∈ N → r • n ∈ p}
⊢ x✝ ∈ ⊥
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case le
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
⊢ (DistribSMul.toLinearMap R M r) m ∈ {r} • N

Tactic:
mem_set_smul_def,

Goal state after:
case le
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
⊢ (DistribSMul.toLinearMap R M r) m ∈ sInf {p | ∀ ⦃r_1 : S⦄ {n : M}, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ p}
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : ¬(⨅ a, b ⊓ bif g a then a else aᶜ) = ⊥
⊢ (⨅ a, b ⊓ bif g a then a else aᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨆ g, ⨅ a, b ⊓ bif g a then a else aᶜ}

Tactic:
refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : ¬(⨅ a, b ⊓ bif g a then a else aᶜ) = ⊥
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
⊢ c = ⊥
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.sup g).SupIndep f

Tactic:
rw [sup_eq_biUnion]

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.biUnion g).SupIndep f
Module: Mathlib.Order.SupIndep

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

Tactic:
let u := (g i).map (Function.Embedding.sigmaMk i)
    let v := t.biUnion (fun j => (g j).map (Function.Embedding.sigmaMk j))
    suffices Disjoint (u.sup f) (v.sup f) by simpa only [sup_map, sup_biUnion, u, v]
    apply SupIndep.disjoint_sup_sup h <;> grind [disjoint_left]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
x✝² : u ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ u
⊢ Disjoint ((fun i ↦ t.sup fun i' ↦ f (i, i')) i) (u.sup fun i ↦ t.sup fun i' ↦ f (i, i'))

Tactic:
suffices Disjoint ((t.image ((i, ·))).sup f) ((u ×ˢ t).sup f) by
      simpa only [sup_image, sup_product_left]

Goal state after:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
x✝² : u ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ u
⊢ Disjoint ((image (fun x ↦ (i, x)) t).sup f) ((u ×ˢ t).sup f)
Module: Mathlib.Order.CompactlyGenerated.Basic

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

Tactic:
· rw [ht₂]
    exact hsc.finsetSup_mem h ht₁

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ t.mulIndicator 1 ⁻¹' s ∈ {univ, ∅}

Tactic:
mulIndicator_one',

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ 1 ⁻¹' s ∈ {univ, ∅}
Module: Mathlib.Order.CompactlyGenerated.Basic

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

Tactic:
Set.not_nonempty_iff_eq_empty

Goal state after:
case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s = ∅
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = 0

Tactic:
· obtain ⟨i, hi, hj⟩ := by simpa using hj
    exact Finset.prod_eq_zero hi <| Set.indicator_of_notMem hj _

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

Goal state before:
pp: case h
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a✝ : List R
h : ∀ (b : R), b ∈ ⟦a✝⟧ → Commute a b
⊢ Commute a (sum ⟦a✝⟧)

Tactic:
rw [quot_mk_to_coe, sum_coe]

Goal state after:
case h
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a✝ : List R
h : ∀ (b : R), b ∈ ⟦a✝⟧ → Commute a b
⊢ Commute a a✝.sum
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (sSup '' c)

Tactic:
· rw [directedOn_image]
      exact hc2.directedOn.mono @fun s t => sSup_le_sSup

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

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

Tactic:
by
  rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_notMem h, 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✝ : 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
hv : a ∈ s
⊢ False

Tactic:
exact ha hv

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

Goal state before:
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:
simp_rw [ih]

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
⊢ a ∈ s ∧ p a ↔ a ∈ x ::ₘ s ∧ p a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝¹ : CommMonoid β
f : ι → κ
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
⊢ ∏ x ∈ image f (s.preimage f hf), g x = ∏ x ∈ s with x ∈ Set.range f, g x

Tactic:
image_preimage

Goal state after:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝¹ : CommMonoid β
f : ι → κ
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
⊢ ∏ x ∈ s with x ∈ Set.range f, g x = ∏ x ∈ s with x ∈ Set.range f, g x
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : 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) = P

Tactic:
by ext <;> simp [Finsupp.update]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
ι : Type u_3
inst✝ : Finite α
f : ι → α → M
hf : ∀ (a : α), HasFiniteMulSupport fun x ↦ f x a
⊢ HasFiniteMulSupport f

Tactic:
simp only [HasFiniteMulSupport] at hf ⊢

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : One M
ι : Type u_3
inst✝ : Finite α
f : ι → α → M
hf : ∀ (a : α), (mulSupport fun x ↦ f x a).Finite
⊢ (mulSupport f).Finite
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, HasFiniteMulSupport (f i)
hs : s.Nonempty
⊢ HasFiniteMulSupport fun a ↦ s.sup' hs fun x ↦ f x a

Tactic:
simp only [HasFiniteMulSupport] at hf ⊢

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
⊢ (mulSupport fun a ↦ s.sup' hs fun x ↦ f x a).Finite
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, HasFiniteMulSupport (f i)
hs : s.Nonempty
⊢ HasFiniteMulSupport fun a ↦ s.inf' hs fun x ↦ f x a

Tactic:
simp only [HasFiniteMulSupport] at hf ⊢

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
⊢ (mulSupport fun a ↦ s.inf' hs fun x ↦ f x a).Finite
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
a : α
inst✝ : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ a ^ s.card ≤ s.prod

Tactic:
by
  rw [← Multiset.prod_replicate, ← Multiset.map_const]
  exact prod_map_le_prod _ h

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

Goal state before:
pp: α : Type u_2
inst✝³ : CommMonoid α
m : Multiset α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : IsOrderedMonoid α
l : List α
⊢ prod ⟦l⟧ = 1 ↔ ∀ (x : α), x ∈ ⟦l⟧ → x = 1

Tactic:
simpa using List.prod_eq_one_iff

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) 0).support)
⊢ comapDomain f (single (f a) 0) hif = single a 0

Tactic:
simp_rw [single_zero, comapDomain_zero]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
⊢ MulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (f i)

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
⊢ MulLECancellable (∏ i ∈ ∅, f i) ↔ ∀ ⦃i : ι⦄, i ∈ ∅ → MulLECancellable (f i)

case cons
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : MulLECancellable (∏ i ∈ s✝, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s✝ → MulLECancellable (f i)
⊢ MulLECancellable (∏ i ∈ cons a✝¹ s✝ h✝, f i) ↔ ∀ ⦃i : ι⦄, i ∈ cons a✝¹ s✝ h✝ → MulLECancellable (f i)
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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄,
    (∃ a_1 ∈ f.support, (Embedding.subtype P) a_1 = a) → ¬∃ a_2 ∈ g.support, (Embedding.subtype fun a ↦ ¬P a) a_2 = a

Tactic:
forall_exists_index,

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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄ (x : Subtype P),
    x ∈ f.support ∧ (Embedding.subtype P) x = a → ¬∃ a_1 ∈ g.support, (Embedding.subtype fun a ↦ ¬P a) a_1 = a
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

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

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

Tactic:
· simp [Finset.insert_subset_iff, h, ht]

Goal state after:
case hf
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∀ i_1 ∈ t, i_1 ∉ insert i s → 1 ≤ f i_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
αs : ι → Type u_12
inst✝² : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝¹ : Fintype η
ιs : η → Type u_14
inst✝ : Zero α
f : (j : η) × ιs j →₀ α
⊢ (fun f ↦ onFinset (univ.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f.split = f

Tactic:
ext
    simp [split]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
αs : ι → Type u_12
inst✝² : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝¹ : Fintype η
ιs : η → Type u_14
inst✝ : Zero α
f : (j : η) → ιs j →₀ α
⊢ ((fun f ↦ onFinset (univ.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f).split = f

Tactic:
ext
    simp [split]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ 1 • f = f

Tactic:
by rw [comapSMul_def, one_smul_eq_id, mapDomain_id]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
α' : Type u_7
s : Set α
t : Set α'
e : ↑s ≃ ↑t
this✝ : DecidablePred fun x ↦ x ∈ s
this : DecidablePred fun x ↦ x ∈ t
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)

Tactic:
exact Finsupp.supportedEquivFinsupp s ≪≫ₗ
    (Finsupp.domLCongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),

Goal state after:
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ᶠ (a : α), g a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),

Goal state after:
α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ᶠ (a : α), g a
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
r : R
f : α → R
⊢ ∑ i, (r • f) i • v i = (RingHom.id R) r • ∑ i, f i • v i

Tactic:
Finset.smul_sum,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
r : R
f : α → R
⊢ ∑ i, (r • f) i • v i = ∑ x, (RingHom.id R) r • f x • v x
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ HasFiniteMulSupport fun j ↦ ∏ᶠ (_ : j ∈ s), f j

Tactic:
simpa only [finprod_eq_mulIndicator_apply, HasFiniteMulSupport, mulSupport_mulIndicator]

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r ↦ r • mi) ∈ span R s
A : ↥c.support ≃ Fin c.support.card
⊢ ∑ i, (fun i ↦ c ↑(A.symm i)) i • ↑((fun i ↦ ⟨↑(A.symm i), ⋯⟩) i) = c.sum fun mi r ↦ r • mi

Tactic:
Finsupp.sum,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r ↦ r • mi) ∈ span R s
A : ↥c.support ≃ Fin c.support.card
⊢ ∑ i, (fun i ↦ c ↑(A.symm i)) i • ↑((fun i ↦ ⟨↑(A.symm i), ⋯⟩) i) = ∑ a ∈ c.support, c a • a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ a ∉ {b}

pp: case hs
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ {b}.Finite

Tactic:
exacts [h, finite_singleton b]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Icc a b) = ↑b + 1 - ↑a

Tactic:
← Nat.card_Icc,

Goal state after:
n : ℕ
a b : Fin n
⊢ #(Icc a b) = #(Icc ↑a ↑b)
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Ico a b) = ↑b - ↑a

Tactic:
rw [← Nat.card_Ico, ← map_valEmbedding_Ico, card_map]

Goal state after: