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
⊢ (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2

Tactic:
let F (p : M × M) : R := if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
  calc
    (x * y).coeff m = ∑ m₁ ∈ x.coeff.support, ∑ m₂ ∈ y.coeff.support, F (m₁, m₂) := coeff_mul ..
    _ = ∑ p ∈ x.coeff.support ×ˢ y.coeff.support with p.1 * p.2 = m, x.coeff p.1 * y.coeff p.2 := by
      rw [Finset.sum_filter, Finset.sum_product]
    _ = ∑ p ∈ s with p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support, x.coeff p.1 * y.coeff p.2 := by
      congr! 1; ext; simp only [mem_filter, mem_product, hs, and_comm]
    _ = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2 :=
      sum_subset (filter_subset _ _) fun p hps hp => by
        simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : x.coeff p.1 = 0
        · rw [h1, zero_mul]
        · rw [hp hps h1, mul_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ AddMonoidHom.mul.compr₂ curryAddEquiv.toAddMonoidHom =
    (AddMonoidHom.mul.comp curryAddEquiv.toAddMonoidHom).compl₂ curryAddEquiv.toAddMonoidHom

Tactic:
ext ⟨m₁, n₁⟩ r₁ ⟨m₂, n₂⟩ r₂

Goal state after:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x y : R[M]
r r₁✝ r₂✝ : R
m m' m₁✝ m₂✝ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
m₁ : M
n₁ : N
r₁ : R
m₂ : M
n₂ : N
r₂ : R
a✝¹ : M
a✝ : N
⊢ ((((((AddMonoidHom.mul.compr₂ curryAddEquiv.toAddMonoidHom).comp (singleAddHom (m₁, n₁))) r₁).comp
                (singleAddHom (m₂, n₂)))
              r₂).coeff
          a✝¹).coeff
      a✝ =
    (((((((AddMonoidHom.mul.comp curryAddEquiv.toAddMonoidHom).compl₂ curryAddEquiv.toAddMonoidHom).comp
                      (singleAddHom (m₁, n₁)))
                    r₁).comp
                (singleAddHom (m₂, n₂)))
              r₂).coeff
          a✝¹).coeff
      a✝
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : Subsingleton G
⊢ UniqueMul A B a0 b0

Tactic:
simp [UniqueMul, eq_iff_true_of_subsingleton]

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

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ s.sort r ~ s.toList

Tactic:
rw [← Multiset.coe_eq_coe]
  simp only [coe_toList, sort_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ map (s.orderEmbOfFin h).toEmbedding univ = s

Tactic:
by
  simp [map_eq_image]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.support = ∅ ↔ p = 0

Tactic:
rcases p with ⟨⟩
  simp [support]

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

Goal state before:
pp: 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
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * (a' * (b' * b⁻¹)) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2

Tactic:
← mul_assoc a',

Goal state after:
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
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * (a' * b' * b⁻¹) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ C a * X ^ (n + 1) = (monomial (n + 1)) a

Tactic:
by
    rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : 0 = 1
p : R[X]
⊢ p = 0

Tactic:
by
  rw [← one_smul R p, ← h, zero_smul]

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

Goal state before:
pp: R : Type u
a b : R
inst✝ : Ring R
n : ℕ
⊢ (monomial n) (a - b) = (monomial n) a - (monomial n) b

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
a b : R
inst✝ : Ring R
n : ℕ
⊢ (monomial n) (a + -b) = (monomial n) a - (monomial n) b
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case left
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Injective ⇑(p.subtype.coprod q.subtype)

Tactic:
rw [← ker_eq_bot, ker_coprod_of_disjoint_range, ker_subtype, ker_subtype, prod_bot]

Goal state after:
case left.hd
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Disjoint p.subtype.range q.subtype.range
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i

Tactic:
· norm_cast

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

Goal state before:
pp: R : Type u_8
N : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : Submodule R N
⊢ Q = Q.subtype.range

Tactic:
Submodule.range_subtype Q

Goal state after:
R : Type u_8
N : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : Submodule R N
⊢ Q = Q
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
κ : ι → Sort u_4
f : (i : ι) → κ i → ℕ∞
⊢ a + ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a + f i j

Tactic:
by
  simp [add_iInf]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).succ =
    q.head

Tactic:
convert! Fin.append_right p q _; rfl

Goal state after:
Module: Mathlib.Order.RelSeries

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

Tactic:
delta last

Goal state after:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (p.append q connect).toFun (Fin.last (p.append q connect).length) = q.toFun (Fin.last q.length)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : 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 : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m < ↑i
⊢ y = p.toFun ⟨↑m, ⋯⟩.succ

Tactic:
· change Fin.insertNth _ _ _ _ = _
        rw [Fin.insertNth_apply_below]
        pick_goal 2
        · change m.1 + 1 < i.1 + 1; rwa [add_lt_add_iff_right]
        simp; rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
d : ℕ
hd : (p : RelSeries r) → p.length = d → motive p
p : RelSeries r
heq : p.length = d + 1
lq : (p.tail ⋯).length = d + 1 - 1
⊢ p = (p.tail ⋯).cons p.head ⋯

Tactic:
exact (p.cons_self_tail (heq ▸ d.zero_ne_add_one.symm)).symm

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
⊢ height a ≤ n

Tactic:
apply height_le_iff.mpr
  intro p hlast
  wlog hlenpos : p.length ≠ 0
  · simp_all
  -- We replace the last element in the series with `a`
  let p' := p.eraseLast.snoc a (lt_of_lt_of_le (p.eraseLast_last_rel_last (by simp_all)) hlast)
  rw [show p.length = p'.length by simp [p']; lia]
  apply h
  simp [p']

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range ≤ g.ker
⊢ (f.range.liftQ g h).ker = ⊥ ↔ g.ker = f.range

Tactic:
by
  simp only [Submodule.ext_iff, mem_ker, Submodule.mem_bot, mem_range]
  constructor
  · intro hfg x
    simpa using hfg (Submodule.Quotient.mk x)
  · intro hfg x
    obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ x
    simpa using hfg x

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ height a
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
rw [ha, Nat.cast_le] at h

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ + 1 ≤ ↑n ↔ ↑a✝ < ↑n

Tactic:
· norm_cast

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ ↑(coheight ⊥) = krullDim α

Tactic:
by
  rw [← krullDim_orderDual]
  exact height_top_eq_krullDim (α := αᵒᵈ)

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P₂
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
x : M ⊗[R] N
p : M
q : N
⊢ (liftAux f') (r • p ⊗ₜ[R] q) = σ₁₂ r • (liftAux f') (p ⊗ₜ[R] q)

Tactic:
simp_rw [← tmul_smul, liftAux_tmul, (f' p).map_smulₛₗ]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a

Tactic:
rw [add_le_iff] at this
    nth_rw 1 [← one_mul a∗]
    exact (mul_left_mono this.1).trans (mul_kstar_le_self this.2)

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
s : Set R
⊢ closure s ^ 0 = closure (s ^ 0)

Tactic:
by rw [pow_zero, pow_zero, one_eq_closure_one_set]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime y z
hdvd : x ∣ y
⊢ IsCoprime x z

Tactic:
obtain ⟨d, rfl⟩ := hdvd
  exact IsCoprime.of_mul_left_left h

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

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime (x + -(y * z)) y ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime (x + -(z * y)) y ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime x (y + -(x * z)) ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime x (y + -(z * x)) ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime x (x * z + -y) ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime x (z * x + -y) ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (x + -(y * z)) y ↔ IsRelPrime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (x + -(z * y)) y ↔ IsRelPrime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x (y + -(x * z)) ↔ IsRelPrime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x (y + -(z * x)) ↔ IsRelPrime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x (x * z + -y) ↔ IsRelPrime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x (z * x + -y) ↔ IsRelPrime x y
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
x : I
hx : x ∈ t
⊢ a ∈ insert a t \ {x}

Tactic:
rw [mem_sdiff, mem_singleton]

Goal state after:
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
x : I
hx : x ∈ t
⊢ a ∈ insert a t ∧ ¬a = x
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M ≤ map (↑(opLinearEquiv R)) (M * N)

Tactic:
refine mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)
    rw [Submodule.mem_map_equiv] at hm hn ⊢
    exact mul_mem_mul hn hm

Goal state after:
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
M : Submodule R A
n : ℕ
⊢ map (↑(opLinearEquiv R)) (M ^ n) = map (↑(opLinearEquiv R)) M ^ n

Tactic:
rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]

Goal state after:
Module: Mathlib.RingTheory.OrzechProperty

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
⊢ Injective ⇑f

Tactic:
by
  obtain ⟨n, g, hg⟩ := Module.Finite.exists_fin' R M
  have := small_of_surjective hg
  let := Equiv.addCommMonoid (equivShrink M).symm
  let := Equiv.module R (equivShrink M).symm
  let j : Shrink.{u} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
  have := Module.Finite.equiv j.symm
  let i' := j.symm.toLinearMap ∘ₗ i
  replace hi : Injective i' := by simpa [i'] using hi
  let f' := j.symm.toLinearMap ∘ₗ f ∘ₗ (LinearEquiv.ofInjective i' hi).symm.toLinearMap
  replace hf : Surjective f' := by simpa [f'] using hf
  simpa [f'] using injective_of_surjective_of_submodule' f' hf

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ ⇑f '' s ⊆ ↑(Submodule.span S (⇑f '' s))

Tactic:
exact subset_span

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

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
⊢ (comap (Pi.evalRingHom R i) I).IsMaximal

Tactic:
refine isMaximal_iff.mpr ⟨I.ne_top_iff_one.mp h.ne_top, fun J x le hxI hxJ ↦ ?_⟩

Goal state after:
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
⊢ 1 ∈ J
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)

Tactic:
rw [mul_div_cancel_left₀ _ b0]

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

Goal state before:
pp: case refine_1
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r = s

pp: case refine_2
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ a ∈ ⊥

Tactic:
· rw [← sub_eq_zero]
    exact H (Module.mem_annihilator (r := r - s).mpr
      (by simp only [sub_smul, H', sub_self, implies_true]))

Goal state after:
case refine_2
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ a ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ ⨅ i, (↑i).annihilator = ⨅ x ∈ {N, P}, x.annihilator

Tactic:
iInf_subtype'

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ ⨅ i, (↑i).annihilator = ⨅ x, (↑x).annihilator
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
i : R
hi : ∃ y ∈ I, ∃ z ∈ J, y + z = i
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
obtain ⟨i', hi', j, hj, rfl⟩ := hi

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
i' : R
hi' : i' ∈ I
j : R
hj : j ∈ J
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + j
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ span {x} ⊔ span {y} = ⊤ ↔ IsCoprime x y

Tactic:
by
  rw [eq_top_iff_one, Submodule.mem_sup]
  constructor
  · rintro ⟨u, hu, v, hv, h1⟩
    rw [mem_span_singleton'] at hu hv
    rw [← hu.choose_spec, ← hv.choose_spec] at h1
    exact ⟨_, _, h1⟩
  · exact fun ⟨u, v, h1⟩ =>
      ⟨_, mem_span_singleton'.mpr ⟨_, rfl⟩, _, mem_span_singleton'.mpr ⟨_, rfl⟩, h1⟩

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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ x * I + y * J

Tactic:
rw [hxy]

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ s.inf' ⋯ (⇑radicalInfTopHom ∘ f) = (f i).radical

Tactic:
exact Finset.inf'_eq_of_forall _ _ hs

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
⊢ ∃ x ∈ I, Prime x

Tactic:
by
  obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
  replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
  obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
    (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
  exact ⟨p, hp₂, prime_of_factor p hp₁⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ WfDvdMonoid α

Tactic:
have : WellFounded (α := {I : Ideal α // I.IsPrincipal}) (· > ·) := h
  constructor
  convert! InvImage.wf (fun a => ⟨Ideal.span ({ a } : Set α), _, rfl⟩) this
  ext
  exact Ideal.span_singleton_lt_span_singleton.symm

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a

Tactic:
apply WfDvdMonoid.exists_factors a

Goal state after: