mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : Subsingleton M
z : M ⊗[R] N
x : M
y : N
⊢ x ⊗ₜ[R] y = 0

Tactic:
rw [Subsingleton.elim x 0, zero_tmul]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMax x

Tactic:
simp only [krullDim, iSup_le_iff, isMax_iff_forall_not_lt]
  refine ⟨fun H x y h ↦ (H ⟨1, ![x, y],
    fun i ↦ by obtain rfl := Subsingleton.elim i 0; simpa⟩).not_gt (by simp), ?_⟩
  · rintro H ⟨_ | n, l, h⟩
    · simp
    · cases H (l 0) (l 1) (h 0)

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

Goal state before:
pp: R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : 0 • x = 0
ihy : 0 • y = 0
⊢ 0 • (x + y) = 0

Tactic:
rw [TensorProduct.smul_add, ihx, ihy, add_zero]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
x : α
⊢ ↑(height x) = krullDim ↑(Set.Ici x)

Tactic:
← krullDim_orderDual,

Goal state after:
α : Type u_3
inst✝ : Preorder α
x : α
⊢ ↑(height x) = krullDim (↑(Set.Ici x))ᵒᵈ
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case ind
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n = ↑n

Tactic:
| ind n ih =>

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
e : α ↪o β
⊢ krullDim α ≤ krullDim β

Tactic:
have (b : β) : Subsingleton (e ⁻¹' {b}) := Set.Subsingleton.coe_sort <|
    Set.Subsingleton.preimage Set.subsingleton_singleton e.injective
  simpa using Order.krullDim_le_of_krullDim_preimage_le' e e.monotone fun _ ↦
    Order.krullDim_nonpos_of_subsingleton

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ a ∈ ∏ i ∈ insert i is, f i ↔ ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), ∏ i ∈ insert i is, g i = a

Tactic:
| insert i is hi ih =>

Goal state after:
case insert
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ a ∈ ∏ i ∈ insert i is, f i ↔ ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), ∏ i ∈ insert i is, g i = a
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ (fun x1 x2 ↦ x1 * x2) a c + (fun x1 x2 ↦ x1 * x2) a b = (fun x1 x2 ↦ x1 * x2) a c

Tactic:
rw [← mul_add, hbc.add_eq_left]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ lTensor M (-f) = -lTensor M f

Tactic:
simp only [← coe_lTensorHom]
  exact (lTensorHom (R := R) (N := N) (P := P) M).map_neg f

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
x✝ : IsCoprime x x
a b : R
h : a * x + b * x = 1
⊢ x * (a + b) = 1

Tactic:
mul_comm,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
x✝ : IsCoprime x x
a b : R
h : a * x + b * x = 1
⊢ (a + b) * x = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
H : IsUnit x
b : R
hb : b * x = 1
⊢ 1 * 0 + b * x = 1

Tactic:
one_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
H : IsUnit x
b : R
hb : b * x = 1
⊢ 0 + b * x = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
⊢ 1 * 1 + 0 * x = 1

Tactic:
one_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
⊢ 1 + 0 * x = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
⊢ 0 * x + 1 * 1 = 1

Tactic:
one_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
⊢ 0 * x + 1 = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
⊢ IsCoprime |x| y ↔ IsCoprime x y

Tactic:
cases le_or_gt 0 x with
  | inl h => rw [abs_of_nonneg h]
  | inr h => rw [abs_of_neg h, IsCoprime.neg_left_iff]

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

Goal state before:
pp: case h
x y : ℤ
h : IsCoprime x y
⊢ x.gcdA y * x + y * x.gcdB y = 1

Tactic:
mul_comm,

Goal state after:
case h
x y : ℤ
h : IsCoprime x y
⊢ x * x.gcdA y + y * x.gcdB y = 1
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
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ p x hx

Tactic:
refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H
  exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩)
    fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩

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

Goal state before:
pp: case e'_2.e'_6
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)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ (∏ x ∈ (insert a t \ {x}) \ {a}, s x) * s a = (fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j

Tactic:
mul_comm,

Goal state after:
case e'_2.e'_6
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)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ s a * ∏ x ∈ (insert a t \ {x}) \ {a}, s x = (fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_2
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
N : Submodule R M
m : M
hm : m ∈ N
⊢ 1 • m ∈ 1 • N

Tactic:
exact smul_mem_smul (one_le.mp le_rfl) hm

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

Goal state before:
pp: case succ.zero
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
ih : 0 ≠ 0 → (M ^ 0).toAddSubmonoid = M.toAddSubmonoid ^ 0
h : 0 + 1 ≠ 0
⊢ toAddSubmonoid 1 * M.toAddSubmonoid = 1 * M.toAddSubmonoid

Tactic:
one_mul,

Goal state after:
case succ.zero
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
ih : 0 ≠ 0 → (M ^ 0).toAddSubmonoid = M.toAddSubmonoid ^ 0
h : 0 + 1 ≠ 0
⊢ toAddSubmonoid 1 * M.toAddSubmonoid = M.toAddSubmonoid
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
⊢ 1 = (Algebra.linearMap R A).range

Tactic:
by
  rw [one_eq_span, LinearMap.span_singleton_eq_range,
    LinearMap.toSpanSingleton_one_eq_algebraLinearMap]

Goal state after:
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 : R × S
h : x ∈ I.prod J
⊢ (RingHom.snd R S) x ∈ J

Tactic:
exact h.2

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:
by
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R N
  let g : (N →ₗ[R] M) →ₗ[R] (Fin n → R) →ₗ[R] M := (LinearMap.llcomp R (Fin n → R) N M).flip f
  exact isNoetherian_of_injective g hf.injective_linearMapComp_right

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

Goal state before:
pp: case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r ↦ r • mi) • n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ (a✝¹ * c i * i) • n ∈ s • N

Tactic:
mul_comm,

Goal state after:
case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r ↦ r • mi) • n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ (i * (a✝¹ * c i)) • n ∈ s • N
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
f : R →ₗ[R] M
⊢ map f I ≤ I • ⊤

Tactic:
rintro _ ⟨y, hy, rfl⟩

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ f y ∈ I • ⊤
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case h
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = p / q * q

Tactic:
mul_comm,

Goal state after:
case h
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = q * (p / q)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case h
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = q * p / q

Tactic:
mul_comm,

Goal state after:
case h
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = p * q / q
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✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
⊢ r ∈ pi ((fun I i ↦ map (Pi.evalRingHom R i) I) I) ↔ r ∈ I

Tactic:
simp_rw [mem_pi, mem_map_iff_of_surjective (Pi.evalRingHom R _) (Function.surjective_eval _)]

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✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
⊢ (∀ (i : ι), ∃ x ∈ I, (Pi.evalRingHom R i) x = r i) ↔ r ∈ I
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : y = gcd x y * z
⊢ x * z * gcd x y = x * y

Tactic:
rw [mul_right_comm, mul_assoc, ← hz]

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

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

Tactic:
obtain _ | m := m
  · rw [Submodule.pow_zero, one_eq_top]; exact le_top
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
  rw [add_comm, Submodule.pow_add _ m.add_one_ne_zero]
  exact mul_le_right

Goal state after:
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:
by
  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
a b c : R
ha : a ≠ 0
hcb : c ∣ b
⊢ a * b / (a * c) = b / c

Tactic:
by_cases hc : c = 0; · simp [hc]
  refine eq_div_of_mul_eq_right hc (mul_left_cancel₀ ha ?_)
  rw [← mul_assoc, ← mul_div_assoc _ (by gcongr), mul_div_cancel_left₀ _ (mul_ne_zero ha hc)]

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

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

Tactic:
rw [eq_comm]
  apply eq_div_of_mul_eq_right h1
  rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]

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
⊢ (z * x + y) / z = x + y / z

Tactic:
rw [eq_comm]
  apply eq_div_of_mul_eq_right h1
  rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]

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

Goal state before:
pp: case h
R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
a : R
ha : z = t * a
⊢ y * (t * a) = t * (y * a)

Tactic:
mul_comm,

Goal state after:
case h
R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
a : R
ha : z = t * a
⊢ t * a * y = t * (y * a)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I * annihilator I = ⊥

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ annihilator I * I = ⊥
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ 0 = ⊤

Tactic:
simp [J.pow_zero]

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ 0 = ⊤

Tactic:
simp [J.pow_zero]

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)

Tactic:
map_pmap

Goal state after:
case neg.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = pmap (fun a h ↦ s.gcd * f h) s ⋯
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
h : m ⊔ comap f ⊥ = ⊤
⊢ False

Tactic:
← RingHom.ker_eq_comap_bot,

Goal state after:
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
h : m ⊔ RingHom.ker f = ⊤
⊢ False
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)

Tactic:
map_pmap

Goal state after:
case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = pmap (fun a h ↦ s.gcd * f h) s ⋯
Module: Mathlib.Algebra.GCDMonoid.Finset

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

Tactic:
by
  by_cases h : b ∈ s
  · rw [insert_eq_of_mem h,
      (lcm_eq_right_iff (f b) (s.lcm f) (Multiset.normalize_lcm (s.1.map f))).2 (dvd_lcm h)]
  apply fold_insert h

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
I : Ideal R
⊢ x ∈ span {y} * I ↔ ∃ z ∈ I, y * z = x

Tactic:
by
  simp only [mul_comm, mem_mul_span_singleton]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
x y : B
⊢ g (f_inv (x * y)) = g (f_inv x) * g (f_inv y)

Tactic:
rw [← map_mul g, ← sub_eq_zero, ← map_sub g, ← mem_ker]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
x y : B
⊢ f_inv (x * y) - f_inv x * f_inv y ∈ ker g
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
ha : ↑a ≠ 0
⊢ a ∈ nonunits ↥S ↔ (↑a)⁻¹ ∉ S

Tactic:
by
  rw [mem_nonunits_iff_or, or_iff_right ha]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ (factors a).card = 1

Tactic:
by
  have hf : factors a ≠ 0 := by
    intro hf
    simpa [hf, Associated.comm, ha.not_isUnit] using factors_prod ha.ne_zero
  obtain ⟨b, hb⟩ := exists_mem_of_ne_zero hf
  obtain ⟨f, hf⟩ := exists_cons_of_mem hb
  rw [hf, card_cons, add_eq_right, card_eq_zero, eq_zero_iff_forall_notMem]
  intro c hc
  obtain ⟨f, rfl⟩ := exists_cons_of_mem hc
  replace hb := (irreducible_of_factor b hb).not_isUnit
  replace hc := (irreducible_of_factor c (hf ▸ mem_cons_of_mem hc)).not_isUnit
  simp [← (factors_prod ha.ne_zero).irreducible_iff, hf, irreducible_mul_iff, hb, hc] at ha

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
x✝ : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
⊢ normalize ↑(Units.mkOfMulEqOne b d ⋯) = 1

Tactic:
normalize_coe_units

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
x✝ : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
⊢ 1 = 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
hgcd : gcd = gcd
a b : α
⊢ lcm a b = lcm a b

Tactic:
refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
S : Ideal K
⊢ IsPrincipal S

Tactic:
rcases Ideal.eq_bot_or_top S with (rfl | rfl)
    · apply bot_isPrincipal
    · apply top_isPrincipal

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ a * b ∣ lcm a b * a

Tactic:
mul_comm,

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ b * a ∣ lcm a b * a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ d * a ∣ c * d

Tactic:
mul_comm,

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ a * d ∣ c * d