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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ ∀ (c : R) {x : M}, x ∈ ⋂ s ∈ S, ↑s → c • x ∈ ⋂ s ∈ S, ↑s

Tactic:
simp +contextual [smul_mem]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ ∀ (c : R) {x : M}, x ∈ ↑p ∩ ↑q → c • x ∈ ↑p ∩ ↑q

Tactic:
simp +contextual [smul_mem]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ f.ker ≤ (c • f).ker

Tactic:
by
  simpa only [ker] using Submodule.comap_le_comap_smul _ _ _

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑(Int.negSucc n) * (x✝¹ * x✝) = ↑(Int.negSucc n) * x✝¹ * x✝

Tactic:
by
      rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
by
  refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  let U : NonUnitalSubsemiring R :=
    NonUnitalSubsemiring.mk' (⋃ i, (S i : Set R))
      (⨆ i, (S i).toSubsemigroup) (Subsemigroup.coe_iSup_of_directed hS)
      (⨆ i, (S i).toAddSubmonoid) (AddSubmonoid.coe_iSup_of_directed hS)
  suffices ⨆ i, S i ≤ U by simpa [U] using @this x
  exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ M.subsemiringClosure = Subsemiring.closure ↑M

Tactic:
ext
  refine
    ⟨fun hx => ?_, fun hx =>
      (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => ?_⟩
  <;> rintro - ⟨H1, rfl⟩
  <;> rintro - ⟨H2, rfl⟩
  · exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2
  · exact H2 sM

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

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

Tactic:
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

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

Goal state before:
pp: case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x = 0

Tactic:
apply h.2

Goal state after:
case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x * (a * b) = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x = 0

Tactic:
apply h.2

Goal state after:
case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x * (a * b) = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
⊢ (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : M), Irreducible (Associates.mk a) ↔ Prime (Associates.mk a)

Tactic:
irreducible_mk,

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
⊢ (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : M), Irreducible a ↔ Prime (Associates.mk a)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).toAddSubmonoid = closure (univ • s)

Tactic:
by
  refine le_antisymm (fun x (hx : x ∈ span R s) ↦ ?of_mem_span) (fun x hx ↦ ?of_mem_closure)
  case of_mem_span =>
    induction hx using span_induction with
    | mem x hx => exact subset_closure ⟨1, trivial, x, hx, one_smul R x⟩
    | zero => exact zero_mem _
    | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
    | smul r₁ y _h hy =>
      clear _h
      induction hy using closure_induction with
      | mem _ h =>
        obtain ⟨r₂, -, x, hx, rfl⟩ := h
        exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
      | zero => simp only [smul_zero, zero_mem]
      | add _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂
  case of_mem_closure =>
    refine closure_le.2 ?_ hx
    rintro - ⟨r, -, x, hx, rfl⟩
    exact smul_mem _ _ (subset_span hx)

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
⊢ b ⊓ ((d ⊔ a) ⊓ c) = a

pp: case refine_2
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
⊢ b ⊔ (d ⊔ a) ⊓ c = c

Tactic:
· simpa [← inf_assoc, ← inf_sup_assoc_of_le _ hb, hdisjoint.eq_bot] using hb.trans hc

Goal state after:
case refine_2
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
⊢ b ⊔ (d ⊔ a) ⊓ c = c
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ a', Disjoint a a' ∧ a ⊔ a' = b

Tactic:
simp_rw [disjoint_iff]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ a', a ⊓ a' = ⊥ ∧ a ⊔ a' = b
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∀ (a : R), ∀ x ∈ R ∙ y, (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x

Tactic:
· rintro a _ - ⟨b, rfl⟩
      exact ⟨a * b, by simp [smul_smul]⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ ⨆ a, ↑a ∈ s

Tactic:
exact hs.iSup_mem hbot (by simpa)

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
⊢ sSup t ∈ s

Tactic:
have := ht.to_subtype
  rw [sSup_eq_iSup']
  exact hs.iSup_mem hbot (by simpa)

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : j ∉ s
⊢ Disjoint (f j) (s.sup f)

Tactic:
by
    rw [eq_empty_of_ssubset_singleton ⟨hs, fun h => hj (h hji)⟩, sup_empty]
    exact disjoint_bot_right

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
x : R
⊢ (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)

Tactic:
rw [algebraMap_eq R S A, RingHom.comp_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
this : Decidable (a ∈ s) := Classical.dec (a ∈ s)
⊢ ¬a ∈ s → 1 = f a ↔ ¬a ∈ s → f a = 1

Tactic:
@eq_comm _ (f a)

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
this : Decidable (a ∈ s) := Classical.dec (a ∈ s)
⊢ ¬a ∈ s → 1 = f a ↔ ¬a ∈ s → 1 = f a
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:
by
  classical
    rw [mulIndicator_const_preimage_eq_union]
    split_ifs <;> simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
this : ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩
⊢ f = g

Tactic:
ext ⟨x, hx⟩

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
this : ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩
x : M
hx : x ∈ span R S
⊢ f ⟨x, hx⟩ = g ⟨x, hx⟩
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
x y : M
⊢ (∃ z, z • x = y) → R ∙ x = R ∙ y

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
case mpr
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
x : M
u : Rˣ
⊢ R ∙ x = R ∙ u • x
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: case nil
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a : R
h : ∀ (b : R), b ∈ [] → Commute a b
⊢ Commute a [].sum

Tactic:
exact Commute.zero_right _

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ x ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))

Tactic:
suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
    simpa only [map_iSup, biSup_congr this]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ∀ i ∈ s, map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.pi fun x ↦ {True, False}, (fun a_1 x ↦ a_1 ∈ {a_2 ∈ s | ∃ (h : a_2 ∈ s), a a_2 h}) = a

Tactic:
simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
⊢ embDomain f (single a m) = single (f a) m

Tactic:
by
  classical
    ext b
    by_cases h : b ∈ Set.range f <;> grind

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

Tactic:
by
  refine Finset.prod_eq_single a (fun b hb₁ hb₂ => ?_) (fun h => ?_)
  · exact h₀ b (mem_support_iff.mp hb₁) hb₂
  · simp only [notMem_support_iff] at h
    rw [h]
    exact h₁ h

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
f g : ι → M₀
x : ι
hfg : x ∈ support fun x ↦ f x * g x
hg : g x = 0
⊢ (fun x ↦ f x * g x) x = 0

Tactic:
simp only [hg, mul_zero]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Tactic:
exact (h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod).trans
      (by gcongr; exacts [h0 _, hs hps])

Goal state after:
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:
rw [comapDomain_apply, mapDomain_apply hf]

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
inst✝ : AddCommMonoid M
e : α ≃ β
v : α →₀ M
⊢ equivMapDomain (Equiv.refl α) v = v

Tactic:
exact equivMapDomain_refl _

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
inst✝ : AddCommMonoid M
e : α ≃ β
v : β →₀ M
⊢ equivMapDomain (Equiv.refl β) v = v

Tactic:
exact equivMapDomain_refl _

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

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
· refine le_of_mul_le_mul_of_pos_left
      (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2) ?_) h
    calc
      _ = ∑ i ∈ s, 2 * r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j) := by
          simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
      _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) := by
          gcongr with i hi
          have ht : (r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j)) ^ 2 ≤
              (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, r j) ^ 2) := by
            grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]
            exact sq_nonneg _
          refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_le_mul
            (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
          repeat rw [mul_assoc]
      _ = _ := by simp_rw [sum_add_distrib, ← sum_mul]; ring

Goal state after:
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
⊢ span R (Set.range v) = ⊤ ↔ Function.Surjective ⇑(linearCombination R v)

Tactic:
rw [← LinearMap.range_eq_top, range_linearCombination]

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
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i * g i = (∏ᶠ (i : α), f i) * ∏ᶠ (i : α), g i

Tactic:
rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf Finset.subset_union_left,
      finprod_eq_prod_of_mulSupport_toFinset_subset g hg Finset.subset_union_right, ←
      Finset.prod_mul_distrib]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i * g i = ∏ x ∈ Finite.toFinset hf ∪ Finite.toFinset hg, f x * g x
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ (fun f i ↦ f (b i)) ((fun f ↦ linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr) f) = f

Tactic:
by
    ext
    simp

Goal state after:
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
v : α → M
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), ∃ c, ∑ i, c i • v i = x

Tactic:
simp_rw [← mem_span_range_iff_exists_fun]
  exact ⟨fun h x => h trivial, fun h x _ => h x⟩

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

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ((mapDomain f (↑b.repr x)).sum fun i a ↦ a • id i) = (b.repr x).sum fun b a ↦ a • f b

Tactic:
rw [Finsupp.sum_mapDomain_index] <;> simp [add_smul]

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

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

Tactic:
card_attachFin,

Goal state after:
n : ℕ
a : Fin n
⊢ #(Ico (↑a) n) = n - ↑a
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ (a + b).rev = a.rev - b

Tactic:
cases n
  · exact a.elim0
  rw [← last_sub, ← last_sub, sub_add_eq_sub_sub]

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

Goal state before:
pp: N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ ∏ c ∈ Finite.toFinset ⋯, f c a = ∏ c ∈ Finite.toFinset ⋯, f c a

Tactic:
apply Finset.prod_subset

Goal state after:
case h
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ Finite.toFinset ⋯ ⊆ Finite.toFinset ⋯

case hf
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ ∀ x ∈ Finite.toFinset ⋯, x ∉ Finite.toFinset ⋯ → f x a = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
x : ℕ∞
h : x ≠ 0
z : ℕ∞
a✝ : ℕ
y_z : ↑a✝ ≤ z
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) z

Tactic:
induction z

Goal state after:
case coe.top
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

case coe.coe
x : ℕ∞
h : x ≠ 0
a✝¹ a✝ : ℕ
y_z : ↑a✝¹ ≤ ↑a✝
⊢ (fun y ↦ x ^ y) ↑a✝¹ ≤ (fun y ↦ x ^ y) ↑a✝
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.coe
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ (↑a✝ + z) = x ^ ↑a✝ * x ^ z

Tactic:
induction z

Goal state after:
case inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ (↑a✝ + ⊤) = x ^ ↑a✝ * x ^ ⊤

case inr.inr.coe.coe
x y z : ℕ∞
x_2 : 1 < x
a✝¹ a✝ : ℕ
⊢ x ^ (↑a✝¹ + ↑a✝) = x ^ ↑a✝¹ * x ^ ↑a✝
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y z : ℕ∞
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
induction z

Goal state after:
case top
x y z : ℕ∞
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

case coe
x y z : ℕ∞
a✝ : ℕ
⊢ (x * y) ^ ↑a✝ = x ^ ↑a✝ * y ^ ↑a✝
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.coe
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝ * z) = (x ^ ↑a✝) ^ z

Tactic:
induction z

Goal state after:
case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ x ^ (↑a✝ * ⊤) = (x ^ ↑a✝) ^ ⊤

case inr.inr.inr.inr.coe.coe
x y z : ℕ∞
x_2 : 1 < x
a✝¹ : ℕ
y_0 : ↑a✝¹ ≠ 0
a✝ : ℕ
z_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝¹ * ↑a✝) = (x ^ ↑a✝¹) ^ ↑a✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
hv : ∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i
f g : ι → R
hfg : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = g i

Tactic:
simp_rw [← s.sum_attach] at hfg

Goal state after:
case mp
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
hv : ∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i
f g : ι → R
i : ι
hi : i ∈ s
hfg : ∑ x ∈ s.attach, f ↑x • v ↑x = ∑ x ∈ s.attach, g ↑x • v ↑x
⊢ f i = g i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Ico a.succ b.succ, f i = ∏ i ∈ Ico a b, f i.succ

Tactic:
by
  simp [← map_succEmb_Ico]

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ ∃ i, i < n ∧ ∃ m, a - b = (m * ↑n + ↑i) • p

Tactic:
refine ⟨(k % n).toNat, ?_⟩

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ (k % ↑n).toNat < n ∧ ∃ m, a - b = (m * ↑n + ↑(k % ↑n).toNat) • p
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.Coprime (n + k * m) ↔ m.Coprime n

Tactic:
by
  rw [Coprime, Coprime, gcd_add_mul_right_right]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inr
n a b : ℕ
h : a ≡ b [MOD n]
h0 : b ≤ a
⊢ n ∣ b - a

Tactic:
rw [Nat.sub_eq_zero_of_le h0]

Goal state after:
case inr
n a b : ℕ
h : a ≡ b [MOD n]
h0 : b ≤ a
⊢ n ∣ 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := ⋯
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m ∣ ↑c * (↑b - ↑a)

Tactic:
Int.mul_sub

Goal state after:
case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m ∣ ↑c * ↑b - ↑c * ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ≡ b [MOD m] ∧ a ≡ b [MOD n]
⊢ a ≡ b [MOD m * n]

Tactic:
by
    rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast,
      ← Int.dvd_natAbs, Int.natCast_dvd_natCast] at h
    rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]
    exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
⊢ ↑↑x = (x % ↑n).toNat

Tactic:
rw [Fin.intCast_def']
  split <;> rename_i h
  · simp [Int.emod_natAbs_of_nonneg h]
  · simp only [Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]
    split <;> rename_i h
    · rw [← Int.natCast_dvd] at h
      rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]
    · rw [Int.emod_natAbs_of_neg (by lia) (NeZero.ne n),
        if_neg (by rwa [← Int.natCast_dvd] at h)]
      have : x % n < n := Int.emod_lt_of_pos x (by have := NeZero.ne n; lia)
      lia

Goal state after: