mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ ∀ (x : G₀ˣ), (∀ (g : G₀ˣ), g * x = x * g) → ∀ (g : G₀), g * ↑x = ↑x * g

Tactic:
intro u hu a

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
⊢ a * ↑u = ↑u * a
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
S : NonUnitalSubring R
⊢ S.toAddSubgroup = ⊤ ↔ S = ⊤

Tactic:
by
  simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Subring R
⊢ S.toSubsemiring = ⊤ ↔ S = ⊤

Tactic:
by
  simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Subring R
⊢ S.toAddSubgroup = ⊤ ↔ S = ⊤

Tactic:
by
  simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ M₀⁰ ↔ ∀ (x : M₀), r * x = 0 → x = 0

Tactic:
← nonZeroDivisorsLeft_eq_nonZeroDivisors

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (x : M₀), r * x = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) → ∀ ⦃a_2 b : M⦄, a = a_2 * b → IsUnit a_2 ∨ IsUnit b

pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b) → ∀ (a_2 a_3 : M), a_2 * a_3 ~ᵤ a → IsUnit a_2 ∨ IsUnit a_3

Tactic:
· rintro h x y rfl
    exact h _ _ <| .refl _

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b) → ∀ (a_2 a_3 : M), a_2 * a_3 ~ᵤ a → IsUnit a_2 ∨ IsUnit a_3
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a b : Associates M
hlt : a < b
⊢ DvdNotUnit a b

Tactic:
by
  constructor
  · rintro rfl
    apply not_lt_of_ge _ hlt
    apply dvd_zero
  rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩
  refine ⟨x, ?_, rfl⟩
  contrapose ndvd
  rcases ndvd with ⟨u, rfl⟩
  simp

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

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
⊢ f.ker ≤ p

Tactic:
SetLike.le_def

Goal state after:
case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
⊢ ∀ ⦃x : M⦄, x ∈ f.ker → x ∈ p
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: α : Type u_2
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
⊢ s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i ↦ f i.1 ⊓ g i.2

Tactic:
simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left, sup_product_left]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R ↑p ⊔ p'
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
← span_eq p',

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R ↑p ⊔ span R ↑p'
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
⊢ y₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)

Tactic:
by
        rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm y₂]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid

Tactic:
mem_toAddSubmonoid,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ p ⊔ p' ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1
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
⊢ ∀ x ∈ {y}, ∃ a, a • y = x

pp: case refine_2
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, a • y = 0

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

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 y (rfl | ⟨⟨_⟩⟩)
      exact ⟨1, by simp⟩

Goal state after:
case refine_2
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, a • y = 0

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

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
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ {x} ⊆ S

Tactic:
Set.singleton_subset_iff

Goal state after:
case refine_1.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ S
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
⊢ (s.attach.SupIndep fun a ↦ f ↑a) ↔ s.SupIndep f

Tactic:
simpa [Finset.attach_map_val] using! (supIndep_map (s := s.attach) (g := .subtype _)).symm

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

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

Tactic:
intro h s u hs hs' hu h_le

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hu : IsLUB s u
h_le : k ≤ u
⊢ ∃ x ∈ s, k ≤ x
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)
a : A
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
⊢ a • m ∈ span R X

Tactic:
obtain ⟨r, rfl⟩ := hsur a

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)
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
r : R
⊢ (algebraMap R A) r • m ∈ span R X
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ False

Tactic:
replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t := by
      have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.sdiff (Finset.finite_toSet _)
      obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
      exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
⊢ False
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
ι : Sort u_8
p : ι → Submodule R M
x : M
⊢ x ∈ (span R (⋃ i, ↑(p i))).toAddSubmonoid → x ∈ AddSubmonoid.closure (⋃ i, ↑(p i).toAddSubmonoid)

Tactic:
mem_toAddSubmonoid,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x : M
⊢ x ∈ span R (⋃ i, ↑(p i)) → x ∈ AddSubmonoid.closure (⋃ i, ↑(p i).toAddSubmonoid)
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_8
inst✝ : NonAssocSemiring R
x : ι → R
⊢ x = ∑ i, x i • Pi.single i 1

Tactic:
convert! pi_eq_sum_univ x

Goal state after:
case a
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_8
inst✝ : NonAssocSemiring R
x : ι → R
x✝¹ : ι
a✝ : x✝¹ ∈ Finset.univ
x✝ : ι
⊢ Pi.single x✝¹ 1 x✝ = if x✝¹ = x✝ then 1 else 0
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
s : Multiset (Multiset α)
a₀ a₁ : Multiset α
x✝ pi : Multiset (Multiset α)
⊢ (a₀.bind fun a ↦ map (cons a) (a₁.bind fun a ↦ map (cons a) pi)) ≍
    a₁.bind fun a ↦ map (cons a) (a₀.bind fun a ↦ map (cons a) pi)

Tactic:
by
    simp [map_bind, bind_bind a₀ a₁, cons_swap]

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

Goal state before:
pp: case zero_left
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y v : N
hv : v ∈ span R t
⊢ (B 0) v ∈ P'

Tactic:
| zero_left v hv =>

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
s : Finset ι
inst✝ : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
y : R
hy : y ∈ Multiset.map (fun i ↦ f i) s.val
⊢ a ∣ y

Tactic:
rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩

Goal state after:
ι : Type u_1
R : Type u_4
s : Finset ι
inst✝ : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
x : ι
hx : x ∈ s.val
hy : f x ∈ Multiset.map (fun i ↦ f i) s.val
⊢ a ∣ f x
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
⊢ s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g

Tactic:
ext x
  by_cases h : x ∈ s
  · rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
      Set.mulIndicator_of_notMem (Set.notMem_compl_iff.2 h), mul_one]
  · rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
⊢ map f (⨅ i, p i) = ⨅ i, map f (p i)

Tactic:
conv_rhs => rw [← map_comap_eq_of_surjective hf (⨅ _, _), comap_iInf]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
⊢ map f (⨅ i, p i) = map f (⨅ i, comap f (map f (p i)))
Module: Mathlib.Algebra.Group.Finsupp

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

Tactic:
by_cases hs : s = a

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

case neg
ι : 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
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
a : M
⊢ (f.update none a).some = f.some

Tactic:
by
  ext
  simp [Finsupp.update]

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

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
⊢ s.mulIndicator f a ≤ y

Tactic:
by_cases ha : a ∈ s
  · simpa [ha] using hfg ha
  · simpa [ha] using hg ha

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j

Tactic:
simp_rw [indicator, mem_prod_eq]

Goal state after:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (if i ∈ s ∧ j ∈ t then 1 (i, j) else 0) = (if i ∈ s then 1 i else 0) * if j ∈ t then 1 j else 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
⊢ v₂ ∈ {w | ↑w.support ⊆ S} → mapDomain f v₁ = mapDomain f v₂ → v₁ = v₂

Tactic:
hv₂

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
⊢ mapDomain f v₁ = mapDomain f v₂ → v₁ = v₂
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i

Tactic:
classical
  simp_rw [prod_eq_mul_prod_sdiff_singleton_of_mem hi]
  refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
  · rw [right_distrib]
    gcongr with j hj <;> aesop
  · apply prod_nonneg
    simp only [and_imp, mem_sdiff, mem_singleton]
    exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)

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✝¹ : Zero γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
⊢ ∀ (x y : α ⊕ β →₀ M),
    sumFinsuppEquivProdFinsupp.toFun (x + y) = sumFinsuppEquivProdFinsupp.toFun x + sumFinsuppEquivProdFinsupp.toFun y

Tactic:
intros
      ext <;>
        simp only [Equiv.toFun_as_coe, Prod.fst_add, Prod.snd_add, add_apply,
          snd_sumFinsuppEquivProdFinsupp, fst_sumFinsuppEquivProdFinsupp]

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

Goal state before:
pp: M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ_inv
inst✝ : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
i : ι
m : M
⊢ (lcongr e₁ e₂) (single i m) = single (e₁ i) (e₂ m)

Tactic:
simp [lcongr]

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.Data.Fin.VecNotation

Goal state before:
pp: case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩

Tactic:
· simp only [← Nat.add_assoc, Nat.add_right_comm, cons_val_succ',
      vecAlt0]

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

Goal state before:
pp: n✝ n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : Fin n
a : ℕ
ha : a < n
b : ℕ
hb : b < n
⊢ ↑(⟨a, ha⟩ - ⟨b, hb⟩) = ↑(⟨a, ha⟩ + -⟨b, hb⟩)

Tactic:
simp [Fin.sub_def, Fin.neg_def, Fin.add_def, Nat.add_comm]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 4 → M
⊢ (∏ i, f i.castSucc) * f (last 3) = f 0 * f 1 * f 2 * f 3

Tactic:
prod_univ_three

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : Fin 4 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (last 3) = f 0 * f 1 * f 2 * f 3
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (v '' s))
⊢ InjOn ⇑f ↑(span R (Set.range fun i ↦ v ↑i))

Tactic:
rwa [← image_eq_range]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rcases eq_zero_or_pos a with rfl | ha0

Goal state after:
case inl
b c : ℕ
⊢ (0 ^ c - 1) % (0 ^ b - 1) = 0 ^ (c % b) - 1

case inr
a b c : ℕ
ha0 : a > 0
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ a ≤ i.castSucc

Tactic:
simp only [le_def, val_succ, val_castSucc]

Goal state after:
case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ ↑a ≤ ↑i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ a.succ ≤ i.castSucc.castSucc

Tactic:
simp only [le_def, val_succ, val_castSucc]

Goal state after:
case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ ↑a + 1 ≤ ↑i
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoidWithOne M
a b n : ℕ
h : a ≡ b [MOD n]
⊢ ↑a ≡ ↑b [PMOD ↑n]

Tactic:
← modEq_iff_natModEq

Goal state after:
M : Type u_1
inst✝ : AddCommMonoidWithOne M
a b n : ℕ
h : a ≡ b [PMOD n]
⊢ ↑a ≡ ↑b [PMOD ↑n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : l ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
⊢ a = 0

Tactic:
linearIndependent_iffₛ.1 hv l (Finsupp.single i a) (by simp [e])

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
⊢ a = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ (∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j) → i.Maximal

Tactic:
intro p w i' h

Goal state after:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
⊢ range v = w
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 : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m / ↑d ∣ ↑c / ↑d * (↑b - ↑a)

pp: case refine_2
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 / ↑d).gcd (↑c / ↑d) = 1

Tactic:
· show (m / d : ℤ) ∣ c / d * (b - a)
    rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]
    apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)
    rw [Int.mul_sub]
    exact modEq_iff_dvd.mp h

Goal state after:
case refine_2
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 / ↑d).gcd (↑c / ↑d) = 1
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x + ∑ x_1, (↑a / ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2)) % xs x_1 * ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2) = ↑a

Tactic:
Fin.prod_univ_succ,

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x +
      ∑ x_1,
        ↑a / (Fin.cons x xs (Fin.castLE ⋯ 0) * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) % xs x_1 *
          (Fin.cons x xs (Fin.castLE ⋯ 0) * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) =
    ↑a