mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ ∑ p ∈ x.coeff.support ×ˢ y.coeff.support with p.1 * p.2 = m, x.coeff p.1 * y.coeff p.2 =
    ∑ p ∈ s with p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support, x.coeff p.1 * y.coeff p.2

Tactic:
congr! 1

Goal state after:
case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ {p ∈ x.coeff.support ×ˢ y.coeff.support | p.1 * p.2 = m} = {p ∈ s | p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support}
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
x✝¹ : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
x✝ : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
⊢ p1 = p2

Tactic:
have h1 := h ha1 hb1 he1; have h2 := h ha2 hb2 he2
    grind

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ k ≤ #univ

Tactic:
card_univ,

Goal state after:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ k ≤ Fintype.card (Fin k)
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
⊢ f ∈ Set.center (End R M) ↔ ∃ α, ∃ (hα : α ∈ Set.center R), f = smulLeft α hα

Tactic:
simp only [Semigroup.mem_center_iff, LinearMap.ext_iff, mul_apply]

Goal state after:
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
⊢ (∀ (g : End R M) (x : M), g (f x) = f (g x)) ↔
    ∃ α, ∃ (h : ∀ (g : R), g * α = α * g), ∀ (x : M), f x = (smulLeft α ⋯) x
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∈ t
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ (lapply i).ker

Tactic:
exact (hs.le_bot ⟨his, hit⟩).elim

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
⊢ ∃ p1,
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ ∃ p2, (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
refine ⟨(_, _), ⟨ha0, hb0⟩, (a, b), ⟨ha, hb⟩, ?_, fun a' b' ha' hb' he => ?_, hu⟩

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
⊢ (a0, b0) ≠ (a, b)

case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ map ((lsum R) fun x ↦ f x • φ) ⊤ = Set.range f • map φ ⊤

Tactic:
← span_single_eq_top,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ map ((lsum R) fun x ↦ f x • φ) (span R {x | ∃ i x_1, single i x_1 = x}) = Set.range f • map φ ⊤
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ (C a).coeff n = if n = 0 then a else 0

Tactic:
convert! coeff_monomial (a := a) (m := n) (n := 0) using 2

Goal state after:
case e'_3.h₁
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ n = 0 ↔ 0 = n
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (p.projection q hpq) x = x ↔ x ∈ p

Tactic:
eq_comm,

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ x = (p.projection q hpq) x ↔ x ∈ p
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : IsEmpty ι
this : a ≠ 0
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
simpa [iInf_of_empty, ite_eq_right_iff, mul_top']

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ×ˢ t ⊆ SetRel.id
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∃ x, s = {x} ∧ t = {x}

Tactic:
simp only [Set.prod_subset_iff, mem_id] at hst

Goal state after:
α : Type u_1
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y
⊢ ∃ x, s = {x} ∧ t = {x}
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝¹ a₁ a₂ : α
b✝ : β
c✝¹ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a✝ b c✝ a c : α
⊢ (a, c) ∈ R ○ R.inv → (c, a) ∈ R ○ R.inv

Tactic:
by rintro ⟨b, hab, hbc⟩; exact ⟨b, hbc, hab⟩

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

Goal state before:
pp: case refine_1
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he✝ : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
hne : (a2, b2) ≠ (a0, b0)
he : a0 * b0 = (a2, b2).1 * (a2, b2).2
⊢ (a2, b2) = (a0, b0)

Tactic:
exact Prod.ext_iff.mpr (this h2.1 h2.2 he.symm)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
⊢ (p.append (singleton r newLast) rel).head = p.head

Tactic:
rw [head_append]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ∀ (x : RelSeries {(a, b) | a < b}),
    ⨆ (_ : a ≤ ({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).head),
        ↑({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).length =
      ⨆ (_ : x.last ≤ a), ↑x.length

Tactic:
congr! 1

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case neg
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : ¬i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd (q.length + 1) ⟨↑i + 1, ⋯⟩) = p.toFun i.succ

Tactic:
· apply Fin.addCases_left

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ∧ height x ≤ ↑n + 1 ↔ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n

Tactic:
congr! 1

Goal state after:
case e'_1
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ↔ ∃ y < x, height y = ↑n

case e'_2
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x ≤ ↑n + 1 ↔ ∀ y < x, height y ≤ ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y ↦ ↑y
⊢ ↑(p.map (fun x_1 ↦ ↑x_1) mono).length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
refine le_iSup₂ (f := fun p hp ↦ (p.length : ℕ∞)) (p.map (fun x ↦ x.1) mono) ?_

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y ↦ ↑y
⊢ RelSeries.last (p.map (fun x_1 ↦ ↑x_1) mono) ≤ x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ krullDim α = 1 ↔ IsSimpleOrder α

Tactic:
rw [le_antisymm_iff, krullDim_le_one_iff_of_boundedOrder, WithBot.one_le_iff_pos,
    Order.krullDim_pos_iff_of_orderBot, isSimpleOrder_iff, and_comm]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i ↦ (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
this : ↑p'.length ≤ height (RelSeries.last p')
⊢ ↑p.length ≤ height x

Tactic:
rw [hlast'] at this

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i ↦ (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
this : ↑p'.length ≤ height x
⊢ ↑p.length ≤ height x
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤

Tactic:
rw [← top_le_iff, ← span_tmul_eq_top, Submodule.map₂_eq_span_image2]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ Submodule.span R (Set.image2 (fun m n ↦ ((mk R M N) m) n) ↑⊤ ↑⊤)
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : r ^ n = r ^ n * r ^ l
⊢ n = n + l

Tactic:
eq_comm,

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : r ^ n * r ^ l = r ^ n
⊢ n = n + l
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁸ : Semiring R
A : Type v
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
M✝¹ : Type u_1
inst✝⁵ : AddCommMonoid M✝¹
inst✝⁴ : Module R M✝¹
inst✝³ : Module A M✝¹
inst✝² : IsScalarTower R A M✝¹
inst✝¹ : IsScalarTower R A A
S T : Set A
M✝ N P Q : Submodule R A
m n : A
ι : Sort uι
inst✝ : IsReduced A
M : Submodule R A
hM : IsNilpotent M
⊢ M = 0

Tactic:
Submodule.zero_eq_bot,

Goal state after:
R : Type u
inst✝⁸ : Semiring R
A : Type v
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
M✝¹ : Type u_1
inst✝⁵ : AddCommMonoid M✝¹
inst✝⁴ : Module R M✝¹
inst✝³ : Module A M✝¹
inst✝² : IsScalarTower R A M✝¹
inst✝¹ : IsScalarTower R A A
S T : Set A
M✝ N P Q : Submodule R A
m n : A
ι : Sort uι
inst✝ : IsReduced A
M : Submodule R A
hM : IsNilpotent M
⊢ M = ⊥
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case succ
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx

Tactic:
pow_succ'

Goal state after:
case succ
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M * M ^ n), C (n + 1) x ⋯
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
r : R
h : R ∙ (algebraMap R A) r = 1
⊢ ∃ r_1, (algebraMap R A) r = (algebraMap R A) ↑r_1

Tactic:
have ⟨r', eq⟩ := mem_span_singleton.mp (h ▸ algebraMap_mem 1)

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
r : R
h : R ∙ (algebraMap R A) r = 1
r' : R
eq : r' • (algebraMap R A) r = (algebraMap R A) 1
⊢ ∃ r_1, (algebraMap R A) r = (algebraMap R A) ↑r_1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
r : R
h : R ∙ (algebraMap R A) r = 1
r' : R
eq : (algebraMap R A) (r' * r) = (algebraMap R A) 1
⊢ ∃ r_1, (algebraMap R A) r = (algebraMap R A) ↑r_1

Tactic:
(FaithfulSMul.algebraMap_injective R A).eq_iff

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
r : R
h : R ∙ (algebraMap R A) r = 1
r' : R
eq : r' * r = 1
⊢ ∃ r_1, (algebraMap R A) r = (algebraMap R A) ↑r_1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ x✝ ∈ Submonoid.map (algebraMap R A) (IsUnit.submonoid R)

Tactic:
simp_rw [Submonoid.mem_map, IsUnit.mem_submonoid_iff, IsUnit, existsAndEq, true_and, eq_comm]

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ ∃ u, x✝ = (algebraMap R A) ↑u
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
r : R
x : A
hx : x ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ r • x * y ∈ I

Tactic:
rw [Algebra.smul_mul_assoc]
        exact Submodule.smul_mem _ _ (hx _ hy)

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

Goal state before:
pp: case inl.e_I
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ map (RingHom.fst R S) (span (s ×ˢ t)) = span s

pp: case inl.e_J
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ map (RingHom.snd R S) (span (s ×ˢ t)) = span t

Tactic:
· rw [Ideal.map_span]
      simp [Set.fst_image_prod _ ht]

Goal state after:
case inl.e_J
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ map (RingHom.snd R S) (span (s ×ˢ t)) = span t
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ (x, 1) * (y, 1) ∈ I.prod ⊤

Tactic:
rw [Prod.mk_mul_mk, mul_one, mem_prod]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ (x * y, 1).1 ∈ I ∧ (x * y, 1).2 ∈ ⊤
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x✝¹ : 1 ∉ I ∧ 1 ∉ J
x✝ : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (0, 1) ∉ I.prod J

Tactic:
simp [hJ]

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

Goal state before:
pp: case mp.inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
hI : ((map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)).IsPrime
h : map (RingHom.snd R S) I = ⊤
⊢ (∃ 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

Tactic:
· left
      rw [h] at hI ⊢
      exact ⟨_, ⟨isPrime_of_isPrime_prod_top hI, rfl⟩⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : IsNoetherian R M
inst✝ : Module.Finite R N
⊢ IsNoetherian R (N →ₗ[R] M)

Tactic:
obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R N

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : IsNoetherian R M
inst✝ : Module.Finite R N
n : ℕ
f : (Fin n → R) →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ IsNoetherian R (N →ₗ[R] M)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ comap f K

Tactic:
by rw [mem_comap, map_one]; exact (ne_top_iff_one _).1 hK

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

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
⊢ x * y / z = x * (y / z)

Tactic:
subst hz
    rw [div_zero, div_zero, mul_zero]

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
x : R
hx : f x = 0
⊢ x ∈ ⊥

Tactic:
← map_zero f

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
x : R
hx : f x = f 0
⊢ x ∈ ⊥
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'
x✝ : R
⊢ x✝ ∈ annihilator R (M × M') ↔ x✝ ∈ annihilator R M ⊓ annihilator R M'

Tactic:
simp_rw [Ideal.mem_inf, mem_annihilator,
    Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ← forall_and_right]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ x = y / z ↔ z * x = y

Tactic:
eq_comm,

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ y / z = x ↔ z * x = y
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (a ∣ s.gcd ↔ ∀ (b : α), b ∈ s → a ∣ b) → (a ∣ (a_1 ::ₘ s).gcd ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → a ∣ b)

Tactic:
by simp +contextual [or_imp, forall_and, dvd_gcd_iff]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
m : Ideal R
inst✝ : m.IsMaximal
hk : RingHom.ker f ≤ m
⊢ (map f m).IsMaximal

Tactic:
by
  refine m.map_eq_top_or_isMaximal_of_surjective f hf ‹_› |>.resolve_left fun h => ?_
  apply congr_arg (comap f) at h
  rw [comap_map_of_surjective _ hf, comap_top, ← RingHom.ker_eq_comap_bot, sup_of_le_left hk] at h
  exact IsMaximal.ne_top ‹_› h

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ s₂.lcm f = GCDMonoid.lcm (∅.lcm f) (s₂.lcm f)

Tactic:
lcm_empty,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ s₂.lcm f = GCDMonoid.lcm 1 (s₂.lcm f)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : ∏ i ∈ s, J i = ⨅ i ∈ s, J i
hp : (↑s).Pairwise (IsCoprime on J) ∧ ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ J a * ⨅ i ∈ s, J i = J a ⊓ ⨅ x ∈ s, J x

Tactic:
obtain ⟨hp1, hp2⟩ := hp

Goal state after:
case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : ∏ i ∈ s, J i = ⨅ i ∈ s, J i
hp1 : (↑s).Pairwise (IsCoprime on J)
hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ J a * ⨅ i ∈ s, J i = J a ⊓ ⨅ x ∈ s, J x
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg.succ
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b * b ^ k) ∣ gcd a b ^ (k + 1)

Tactic:
pow_succ'

Goal state after:
case neg.succ
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b * b ^ k) ∣ gcd a b * gcd a b ^ k
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Subsingleton α
⊢ Associated (0 ^ k) a

Tactic:
Subsingleton.elim a (0 ^ k)

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Subsingleton α
⊢ Associated (0 ^ k) (0 ^ k)