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

Goal state before:
pp: case cons.inl
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = L.prod
⊢ C hd.prod

Tactic:
rw [HP]
    clear HP HL hd
    induction L with
    | nil => exact h1
    | cons hd tl ih =>
      rw [List.forall_mem_cons] at HL'
      rw [List.prod_cons]
      exact hs _ HL'.1 _ (ih HL'.2)

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b c : M
h : b ~ᵤ c
⊢ a * b ~ᵤ a * c

Tactic:
obtain ⟨d, rfl⟩ := h

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
d : Mˣ
⊢ a * b ~ᵤ a * (b * ↑d)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
c : M
⊢ a * c ~ᵤ b * c

Tactic:
obtain ⟨d, rfl⟩ := h

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a c : M
d : Mˣ
⊢ a * c ~ᵤ a * ↑d * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
c : M
⊢ a * c ~ᵤ b * c

Tactic:
obtain ⟨d, rfl⟩ := h; exact ⟨d, mul_right_comm _ _ _⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
u : (Associates M)ˣ
⊢ ↑u = 1

Tactic:
by
  simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : Associates.mk a = Associates.mk (a₁ * a₂)
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
obtain ⟨u, rfl⟩ := mk_eq_mk_iff_associated.mp eq.symm
    exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩

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✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f : M →ₛₗ[σ₁₂] M₂
g✝ : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h✝ : M₂ →ₛₗ[σ₂₃] M₃
p q : Submodule R M
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
g : M₂ → M
h : LeftInverse g ⇑f
x : ↥f.range
x' : M
hx' : f x' = ↑x
⊢ f (g ↑x) = ↑x

Tactic:
rw [← hx', h x']

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x z y : α
⊢ z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z

Tactic:
simp_rw [inf_comm x, sup_comm _ z]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x z y : α
⊢ z ≤ x → (z ⊔ y) ⊓ x ≤ z ⊔ y ⊓ x
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case add
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x x✝ y✝ : M
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
h₁ : x✝ ∈ closure (univ • s)
h₂ : y✝ ∈ closure (univ • s)
⊢ x✝ + y✝ ∈ closure (univ • s)

Tactic:
exact add_mem h₁ h₂

Goal state after:
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
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk i) (g i)
⊢ 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 v := t.biUnion (fun j => (g j).map (Function.Embedding.sigmaMk j))

Goal state after:
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
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk i) (g i)
v : Finset ((x : ι) × β x) := t.biUnion fun j ↦ map (Function.Embedding.sigmaMk j) (g j)
⊢ Disjoint ((fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩) i) (t.sup fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
⊢ Disjoint (t k) (⨆ j, ⨆ (_ : j ≠ k), t j)

Tactic:
refine h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le ?_)

Goal state after:
case mpr.inr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
j : ι
hj : j ≠ k
⊢ t j = t i
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
A : Type w
M : Type v₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : MulAction A M
inst✝ : SMul R M
h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x
r : R
a : A
x : M
⊢ (r • a) • x = r • a • x

Tactic:
by rw [Algebra.smul_def, mul_smul, h]

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

Goal state before:
pp: R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m : M
hm : m ∈ restrictScalars R (span A X)
⊢ m ∈ span R X

Tactic:
refine span_induction subset_span (zero_mem _) (fun _ _ _ _ => add_mem) (fun a m _ hm => ?_) hm

Goal state after:
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m✝ : M
hm✝ : m✝ ∈ restrictScalars R (span A X)
a : A
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
⊢ a • m ∈ span R X
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
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ U.ite ((fun x ↦ a) ⁻¹' s) ((fun x ↦ 1) ⁻¹' s) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
Set.preimage_const,

Goal state after:
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ U.ite (if a ∈ s then univ else ∅) ((fun x ↦ 1) ⁻¹' s) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ t, ↑t ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ t.sup id
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
refine (le_inf hcinf.1 ht2).trans ?_

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ t, ↑t ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ t.sup id
⊢ a ⊓ t.sup id ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
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 : ∃ x, ∃ (_ : ¬f x = ⊥), ∃ x_1, ∃ (_ : ¬f x_1 = ⊥) (_ : f x = f x_1), ¬x = x_1
⊢ False

Tactic:
obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i x₁ : ι
hx₁ : ¬f x₁ = ⊥
x₂ : ι
hx₂ : ¬f x₂ = ⊥
hfeq : f x₁ = f x₂
hneq : ¬x₁ = x₂
⊢ False
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
this : map q.subtype (span S (range ⇑(inclusion h₁))) = q
⊢ map q.subtype (span S (range ⇑(inclusion h₁))) = map q.subtype ⊤

Tactic:
this,

Goal state after:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
this : map q.subtype (span S (range ⇑(inclusion h₁))) = q
⊢ q = map q.subtype ⊤
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s t : Set M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ ∀ (c : R) {x : M × M'}, x ∈ ↑p ×ˢ ↑q₁ → c • x ∈ ↑p ×ˢ ↑q₁

Tactic:
by rintro a ⟨x, y⟩ ⟨hx, hy⟩; exact ⟨smul_mem _ a hx, smul_mem _ a hy⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
⊢ f x * g x = f x

Tactic:
this,

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
⊢ f x * 1 = f x
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ f x * g x = g x

Tactic:
this,

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ 1 * g x = g x
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
l : List α
hp : {x | x ∈ ⟦l⟧ ∧ p x}.Subsingleton
⊢ find? p ⟦l⟧ hp = some a → p a

Tactic:
simp only [quot_mk_to_coe, find?_coe _ _ hp]

Goal state after:
case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
l : List α
hp : {x | x ∈ ⟦l⟧ ∧ p x}.Subsingleton
⊢ List.find? (fun a ↦ decide (p a)) l = some a → p a
Module: Mathlib.Data.Finsupp.Ext

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
⊢ f = g

Tactic:
by
      have := addHom_ext (f := f.toAdditiveRight) (g := g.toAdditiveRight) H
      ext
      rw [DFunLike.ext_iff] at this
      apply this

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

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
n k : ℕ
⊢ ∏ i ∈ range k, (↑n - ↑i) = ↑(∏ i ∈ range k, (n - i))

Tactic:
prod_natCast

Goal state after:
R : Type u_4
inst✝ : CommRing R
n k : ℕ
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a = a' then b else 0

Tactic:
simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a = a' then b else 0

Tactic:
by
  classical
  simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint {i} (single j b').support ↔ i ≠ j

Tactic:
support_single _ hb',

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint {i} {j} ↔ i ≠ j
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : s = a
⊢ (erase a (f + f')) s = (erase a f + erase a f') s

Tactic:
rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ (∀ (x : ι), (single k u + single l v) x = (single m u + single n v) x) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
coe_add,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ (∀ (x : ι), (⇑(single k u) + ⇑(single l v)) x = (⇑(single m u) + ⇑(single n v)) x) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
Module: Mathlib.Algebra.Order.Group.Indicator

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

Tactic:
by_cases hx : x ∈ ⋃ i, s i
  · rw [mulIndicator_of_mem hx]
    rw [mem_iUnion] at hx
    refine le_antisymm ?_ (iSup_le fun i ↦ mulIndicator_le_self' (fun x _ ↦ h1 ▸ bot_le) x)
    rcases hx with ⟨i, hi⟩
    exact le_iSup_of_le i (ge_of_eq <| mulIndicator_of_mem hi _)
  · rw [mulIndicator_of_notMem hx]
    simp only [mem_iUnion, not_exists] at hx
    simp [hx, ← h1]

Goal state after:
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:
this,

Goal state after:
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
⊢ 0 = (↑n)⁻¹ • f x
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
⊢ 0 = (↑n)⁻¹ • f x

Tactic:
this,

Goal state after:
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
⊢ 0 = (↑n)⁻¹ • 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ (embDomain f v).prod g = v.prod fun a b ↦ g (f a) b

Tactic:
prod,

Goal state after:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ a ∈ (embDomain f v).support, g a ((embDomain f v) a) = v.prod fun a b ↦ g (f a) b
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ a ∈ (embDomain f v).support, g a ((embDomain f v) a) = v.prod fun a b ↦ g (f a) b

Tactic:
prod,

Goal state after:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ a ∈ (embDomain f v).support, g a ((embDomain f v) a) = ∏ a ∈ v.support, g (f a) (v a)
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 ⊢
  rw [mulSupport_prodMk f g]
  exact hf.union hg

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

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ ∏ a ∈ (f1 + f2).support, g a ((f1 + f2) a) =
    (∏ x ∈ f1.support, g x (f1 x + f2 x)) * ∏ x ∈ f2.support, g x (f1 x + f2 x)

Tactic:
support_add_eq hd,

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ ∏ x ∈ f1.support ∪ f2.support, g x ((f1 + f2) x) =
    (∏ x ∈ f1.support, g x (f1 x + f2 x)) * ∏ x ∈ f2.support, g x (f1 x + f2 x)
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
n : α
a✝ : List α
h : ∀ (x : α), x ∈ ⟦a✝⟧ → x ≤ n
⊢ prod ⟦a✝⟧ ≤ n ^ card ⟦a✝⟧

Tactic:
simpa using List.prod_le_pow_card _ _ h

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < (x :: xs).prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1

Tactic:
simp_rw [List.prod_cons, List.forall_mem_cons, CanonicallyOrderedAdd.mul_pos,
    list_prod_pos]

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

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)) →
        (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)

Tactic:
intro a s ha ih H

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
⊢ ∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, 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
inst✝¹ : AddZeroClass M
p✝ : α → Prop
v v' : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f g : α →₀ M
⊢ ⇑(filter p (f + g)) = ⇑(filter p f + filter p g)

Tactic:
coe_add,

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✝¹ : AddZeroClass M
p✝ : α → Prop
v v' : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f g : α →₀ M
⊢ ⇑(filter p (f + g)) = ⇑(filter p f) + ⇑(filter p g)
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
this : Multiset.map (fun x ↦ b • f x) s.val = Multiset.map (fun x ↦ b • x) (Multiset.map f s.val)
⊢ b ^ s.val.card • (Multiset.map f s.val).prod = (Multiset.map (fun x ↦ b • f x) s.val).prod

Tactic:
this,

Goal state after:
M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
this : Multiset.map (fun x ↦ b • f x) s.val = Multiset.map (fun x ↦ b • x) (Multiset.map f s.val)
⊢ b ^ s.val.card • (Multiset.map f s.val).prod = (Multiset.map (fun x ↦ b • x) (Multiset.map f s.val)).prod
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
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ↑s →₀ M
⊢ ↑((supportedEquivFinsupp s).symm f) = f.extendDomain

Tactic:
by
  convert! restrictSupportEquiv_symm_apply_coe ..

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

Goal state before:
pp: case inr
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
f : ι → R
x : M
hx : x ≠ 0
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x

Tactic:
· exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
s : Set α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = s.mulIndicator f a

Tactic:
convert! finprod_eq_if (M := M) (p := a ∈ s) (x := f a)

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport f
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
classical rw [finprod_def, dif_pos hf]

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

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 1)
hj₀ : 0 < j
hj : j ≤ i.succ
⊢ j ∈ succ '' Iic i

Tactic:
rcases exists_succ_eq_of_ne_zero hj₀.ne' with ⟨j, rfl⟩

Goal state after:
n : ℕ
i j : Fin n
hj₀ : 0 < j.succ
hj : j.succ ≤ i.succ
⊢ j.succ ∈ succ '' Iic i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 1)
hj₀ : 0 < j
hj : j < i.succ
⊢ j ∈ succ '' Iio i

Tactic:
rcases exists_succ_eq_of_ne_zero hj₀.ne' with ⟨j, rfl⟩

Goal state after:
n : ℕ
i j : Fin n
hj₀ : 0 < j.succ
hj : j.succ < i.succ
⊢ j.succ ∈ succ '' Iio i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ 1 < ∏ᶠ (i : ι), f i

Tactic:
by
  rw [← finprod_mem_univ]
  apply one_lt_finprod_cond <;> simpa

Goal state after:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
⊢ image val univ = range n

Tactic:
by
  ext
  simp [Fin.exists_iff]

Goal state after: