mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
S₁ : Type u_6
S₂ : Type u_7
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Ring R
inst✝⁸ : Module R M
inst✝⁷ : Semiring R₁
inst✝⁶ : Module R₁ M
inst✝⁵ : Semiring R₂
inst✝⁴ : Module R₂ M
inst✝³ : Semiring S₁
inst✝² : Module S₁ M
inst✝¹ : Semiring S₂
inst✝ : Module S₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
l₁'' : NF S₁ M
l₂'' : NF S₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁''.eval
hx₂ : x₂ = l₂''.eval
h₁' : l₁'.eval = l₁''.eval
h₂' : l₂'.eval = l₂''.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval - l₂'.eval = l.eval

Tactic:
← h₂,

Goal state after:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
S₁ : Type u_6
S₂ : Type u_7
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Ring R
inst✝⁸ : Module R M
inst✝⁷ : Semiring R₁
inst✝⁶ : Module R₁ M
inst✝⁵ : Semiring R₂
inst✝⁴ : Module R₂ M
inst✝³ : Semiring S₁
inst✝² : Module S₁ M
inst✝¹ : Semiring S₂
inst✝ : Module S₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
l₁'' : NF S₁ M
l₂'' : NF S₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁''.eval
hx₂ : x₂ = l₂''.eval
h₁' : l₁'.eval = l₁''.eval
h₂' : l₂'.eval = l₂''.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval - l₂.eval = l.eval
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₁
inst✝² : Module R₁ M
inst✝¹ : Semiring R₂
inst✝ : Module R₂ M
l₁ l₂ : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval = l₂.eval
⊢ l₁.eval = l₂'.eval

Tactic:
← h₂,

Goal state after:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₁
inst✝² : Module R₁ M
inst✝¹ : Semiring R₂
inst✝ : Module R₂ M
l₁ l₂ : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval = l₂.eval
⊢ l₁.eval = l₂.eval
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : ∀ (j : ι), r * l' j - (single i (r * l' i)) j + l' i * l j = 0
⊢ l' = 0

Tactic:
grind [mem_nonZeroDivisors_iff]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s : R
⊢ (ψ.mulShift r).mulShift s = ψ.mulShift (r * s)

Tactic:
ext
  simp only [mulShift_apply, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
x y : R[M]
⊢ mapDomain f (x + y) = mapDomain f x + mapDomain f y

Tactic:
by
  ext; simp [Finsupp.mapDomain_add]

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ' : Type u_6
δ : Type u_7
ε : Type u_9
inst✝³ : DecidableEq β'
inst✝² : DecidableEq γ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
⊢ ↑(image₂ f s (image₂ g t u)) ⊆ ↑(image₂ g' (image₂ f₁ s t) (image₂ f₂ s u))

Tactic:
by
    push_cast
    exact Set.image2_distrib_subset_left h_distrib

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec (n + 1) s) = ↑s ^ (n + 1)

Tactic:
rw [npowRec, pow_succ, coe_mul, ih]

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ (lmapDomain R R u).range = span R (Set.range fun x ↦ single (u x) 1)

Tactic:
refine le_antisymm ?_ ?_
  · rintro x ⟨x, rfl⟩
    induction x using induction_linear with
    | single i s =>
        rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]
        exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
    | zero => simp
    | add f g hf hg =>
        rw [map_add]
        exact Submodule.add_mem _ hf hg
  · rw [Submodule.span_le, Set.range_subset_iff]
    intro i
    exact ⟨Finsupp.single i 1, by simp⟩

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

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
s : Finset (Submodule R M)
hsS : ↑s ⊆ S
hs : m ∈ ⨆ i ∈ s, i
⊢ m ∈ ⨆ i ∈ s.preimage Subtype.val ⋯, ↑i

Tactic:
have : ⨆ (i) (_ : i ∈ S ∧ i ∈ s), i = ⨆ (i) (_ : i ∈ s), i := by convert! rfl; grind

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
s : Finset (Submodule R M)
hsS : ↑s ⊆ S
hs : m ∈ ⨆ i ∈ s, i
this : ⨆ i, ⨆ (_ : i ∈ S ∧ i ∈ s), i = ⨆ i ∈ s, i
⊢ m ∈ ⨆ i ∈ s.preimage Subtype.val ⋯, ↑i
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support ⊆ {n}

Tactic:
rw [← ofFinsupp_single, support]
  exact Finsupp.support_single_subset

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ ∀ x ∈ support 1, coeff 1 x ∈ {1}

Tactic:
simp_all [coeff_one]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
this : ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f
⊢ Submodule.map (↑e) p ≤ Submodule.comap ((↑e ∘ₗ f) ∘ₗ ↑e.symm) (Submodule.map (↑e) p) ↔ p ≤ Submodule.comap f p

Tactic:
Submodule.map_le_iff_le_comap,

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
this : ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f
⊢ p ≤ Submodule.comap (↑e) (Submodule.comap ((↑e ∘ₗ f) ∘ₗ ↑e.symm) (Submodule.map (↑e) p)) ↔ p ≤ Submodule.comap f p
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: case h
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
h3 : φ (Pi.single s 1) = 1
t : G
⊢ φ.toLinearMap ((Pi.basisFun k G) t) = (Pi.evalAlgHom k (fun i ↦ k) s).toLinearMap ((Pi.basisFun k G) t)

Tactic:
by_cases t = s <;> simp_all

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

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : ι
⊢ i ∈ Set.range u ⊔ Set.range v

Tactic:
codisjoint_iff.mp h.2

Goal state after:
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : ι
⊢ i ∈ ⊤
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : ¬A' = A
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0

Tactic:
· exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ ↑t2 ⊆ ↑s

Tactic:
intro x hx
      have : x ∈ span R t2 := subset_span hx
      rw [ht2] at this
      exact this.1

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.left
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (l.sum fun a m ↦ m • id (g a)) ∈ s

Tactic:
refine s.sum_mem ?_
      intro y hy
      exact s.smul_mem _ (hg y (hl1 hy)).1

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : Surjective ⇑g
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ Module.Finite R N

Tactic:
by
  refine ⟨(⊤ : Submodule R _).fg_of_fg_map_of_fg_inf_ker g ?_ ?_⟩
  · rw [← LinearMap.range_eq_top] at h_surj
    rw [Submodule.map_top, h_surj]
    exact Module.Finite.fg_top
  · simp [LinearMap.exact_iff.1 h_exact]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length = 0
⊢ {x | x ∈ s}.Subsingleton

Tactic:
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩

Goal state after:
α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length = 0
i j : Fin (s.length + 1)
⊢ s.toFun i = s.toFun j
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := ⋯
y : α := ⋯
hm : ↑m = ↑i
⊢ ↑m = ↑i.castSucc

Tactic:
exact hm

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ i 0 = 0 ∧ i (Fin.last s.length) = Fin.last t.length

Tactic:
obtain ⟨n, s, h⟩ := s
  induction n with
  | zero => exact ⟨⟨0, s, nofun⟩, (Equiv.refl _).toEmbedding, rfl, rfl, rfl⟩
  | succ n IH =>
    obtain ⟨t₁, i, ht, hi₁, hi₂⟩ := IH (s ∘ Fin.castSucc) fun _ ↦ h _
    obtain ⟨t₂, h₁, m, h₂, ht₂⟩ :=
      exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le (h (.last _)).le
    let t₃ : RelSeries {(a, b) : α × α | a ⋖ b} := ⟨m, (t₂ ·), fun i ↦ by simpa using! ht₂ i⟩
    have H : t₁.last = t₂ 0 := (congr(t₁ $hi₂.symm).trans (congr_fun ht _)).trans h₁.symm
    refine ⟨t₁.smash t₃ H, ⟨Fin.snoc (Fin.castLE (by simp) ∘ i) (.last _), ?_⟩, ?_, ?_, ?_⟩
    · refine Fin.lastCases (Fin.lastCases (fun _ ↦ rfl) fun j eq ↦ ?_) fun j ↦ Fin.lastCases
        (fun eq ↦ ?_) fun k eq ↦ Fin.ext (congr_arg Fin.val (by simpa using! eq) :)
      on_goal 2 => rw [eq_comm] at eq
      all_goals
        rw [Fin.snoc_castSucc] at eq
        obtain rfl : m = 0 := by simpa [t₃] using! (congr_arg Fin.val eq).trans_lt (i j).2
        cases (h (.last _)).ne' (h₂.symm.trans h₁)
    · refine funext (Fin.lastCases ?_ fun j ↦ ?_)
      · convert! h₂; simpa using! RelSeries.last_smash ..
      convert! congr_fun ht j using 1
      simp [RelSeries.smash_castLE]
    all_goals simp [Fin.snoc, Fin.castPred_zero, hi₁]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case refine_2
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.last = ⊤

Tactic:
← h₂,

Goal state after:
case refine_2
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.last = RelSeries.last s
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
r s : R'
x✝ x y : M ⊗[R] N
ihx : (r * s) • x = r • s • x
ihy : (r * s) • y = r • s • y
⊢ (r * s) • (x + y) = r • s • (x + y)

Tactic:
by
        simp_rw [TensorProduct.smul_add]
        rw [ihx, ihy]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n✝ n : ℕ
⊢ mulLeft R a ^ (n + 1) = mulLeft R (a ^ (n + 1))

Tactic:
by rw [pow_succ, pow_succ, mulLeft_mul, Module.End.mul_eq_comp, pow_mulLeft]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j

Tactic:
by
  by_cases h : i = j <;> aesop

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j

Tactic:
by
  by_cases h : i = j <;> aesop

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
x✝ : 1 ≠ 0
⊢ ↑(p ^ 1) = ↑p ^ 1

Tactic:
pow_one,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
x✝ : 1 ≠ 0
⊢ ↑p = ↑p ^ 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime (z * y - x) y ↔ IsCoprime x y

Tactic:
rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (z * y - x) y ↔ IsRelPrime x y

Tactic:
rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ (∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i)

Tactic:
by
  simpa only [isCoprime_comm] using IsCoprime.prod_left (R := R)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ I.IsPrime → (∃ p, p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ p, p.IsPrime ∧ I = ⊤.prod p

Tactic:
ideal_prod_eq I

Goal state after:
case mp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ ((map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)).IsPrime →
    (∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) = p.prod ⊤) ∨
      ∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) = ⊤.prod p
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map (↑f.symm) (map (↑f) I) = I

Tactic:
rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ ↑I
s : R
hsj : s ∈ ↑J
⊢ f (r * s) ∈ ↑(map f (I * J))

Tactic:
exact mem_map_of_mem f (mul_mem_mul hri hsj)

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * gcd x y

Tactic:
rw [gcd_eq_gcd_ab, mul_add]

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : x ∈ Module.annihilator R M
⊢ x ∈ Module.annihilator R M'

Tactic:
by
  rw [Module.mem_annihilator] at h ⊢
  intro m; obtain ⟨m, rfl⟩ := hf m
  rw [← map_smul, h, f.map_zero]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ I ^ 0

Tactic:
rw [Submodule.pow_zero, one_eq_top]; exact le_top

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
⊢ y = 0

Tactic:
by_cases hgxy : gcd x y = 0

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : gcd x y = 0
⊢ y = 0

case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
⊢ y = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
obtain rfl | h := eq_or_ne n 0
  · rw [add_zero, Submodule.pow_zero, IsTwoSided.mul_one]
  · exact Submodule.pow_add _ h

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ t * y * (x / y + z / t) = t * x + y * z

Tactic:
rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ n ∈ span R s, r • n = 0) → ∀ (n : ↑s), r • ↑n = 0

Tactic:
intro h n

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ n ∈ span R s, r • n = 0
n : ↑s
⊢ r • ↑n = 0
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℤ
⊢ Associated (↑(a.gcd b) * ↑(a.lcm b)) (a * b)

Tactic:
← Int.natCast_mul,

Goal state after:
a b : ℤ
⊢ Associated (↑(a.gcd b * a.lcm b)) (a * b)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ ↑(u * Exists.choose ⋯) = ↑(Exists.choose ⋯)

Tactic:
rw [Units.val_mul, ← (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero ha).eq_iff,
        (assoc a).choose_spec, ← mul_assoc, (assoc _).choose_spec,
        Associates.mk_eq_mk_iff_associated.mpr (associated_mul_unit_right a u u.isUnit)]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ 0 = gcd 0 0 * 1

Tactic:
by rw [h, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ R ∙ x ≤ span {normalize x}

Tactic:
simp [Ideal.mem_span_singleton]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ span {normalize x} ≤ R ∙ x

Tactic:
simp [Ideal.mem_span_singleton]

Goal state after: