mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
⊢ height (p.toFun i) = ↑↑i

Tactic:
refine le_antisymm (height_le ?_) (index_le_height p i)
  intro p' hp'
  have hp'' := length_le_height_last (p := p'.smash (p.drop i) (by simpa))
  simp [← h] at hp''; clear h
  norm_cast at *
  lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderBot α
h : ⊥ < x
⊢ ¬IsMin x

Tactic:
grind [not_isMin_iff]

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

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

Tactic:
induction t using Finset.induction_on generalizing a with
    | empty =>
      simp_rw [Finset.prod_empty, Set.mem_one]
      exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.notMem_empty _ hi), h.symm⟩,
        fun ⟨_, _, hf⟩ ↦ hf.symm⟩
    | 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.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
α : Type u_22
s : Finset α
m : α → M
n : N
⊢ (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n

Tactic:
classical
    induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, add_tmul, ih]

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

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

Tactic:
rw [add_le_iff]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a * a∗ ≤ a∗
Module: Mathlib.Algebra.Order.Kleene

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

Tactic:
rw [add_le_iff]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a∗ * a ≤ a∗
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a∗ * a ≤ a∗

Tactic:
exact ⟨one_le_kstar, kstar_mul_le_kstar⟩

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 ↔ IsCoprime x y

Tactic:
neg_left_iff

Goal state after:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime 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 ↔ IsRelPrime x y

Tactic:
neg_left_iff

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x y ↔ IsRelPrime x y
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
⊢ ∃ tr, ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j

Tactic:
let li := List.ofFn val
  let sli := li.mergeSort
  have (i : Fin n) : ∃ j : Fin sli.length, sli[j] = val i := by
    apply List.get_of_mem
    rw [List.Perm.mem_iff (List.mergeSort_perm _ _)]
    simp [li]
  use fun i ↦ (this i).choose
  intro i j
  simp only [Fin.getElem_fin, Int.ofNat_le]
  by_cases h_eq : val i = val j
  · simp [h_eq]
  generalize_proofs _ hi hj
  rw [← hi.choose_spec, ← hj.choose_spec] at h_eq
  conv_lhs => rw [← hi.choose_spec, ← hj.choose_spec]
  have := li.pairwise_mergeSort (le := fun a b ↦ decide (a ≤ b))
      (fun a b c ↦ by simpa using le_trans) (by simpa using le_total)
  rw [List.pairwise_iff_get] at this
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · contrapose! h
    exact lt_of_le_of_ne (by simpa using (this hj.choose hi.choose (by simpa)))
      (fun h ↦ h_eq (h.symm))
  · simpa using this hi.choose hj.choose (by apply lt_of_le_of_ne h; contrapose h_eq; simp [h_eq])

Goal state after:
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
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • m₁ + r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
exact (A'.1 • M'.1).add_mem h₁ h₂

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

Goal state before:
pp: case cons.mp.refine_2.refine_1
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 * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
⊢ (μ a * ∏ i ∈ t \ {b}, s i) * s b + (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) * s a = 1

Tactic:
mul_assoc,

Goal state after:
case cons.mp.refine_2.refine_1
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 * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
⊢ μ a * ((∏ i ∈ t \ {b}, s i) * s b) + (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) * s a = 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
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
⊢ (S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ↔
    S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

Tactic:
constructor <;> rintro ⟨y, hy⟩

Goal state after:
case mp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
⊢ S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

case mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy : (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y = S
⊢ S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)
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
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ ↑(opLinearEquiv R) (m * n) ∈ comap (↑(opLinearEquiv R).symm) N * map (↑(opLinearEquiv R)) M

Tactic:
map_equiv_eq_comap_symm

Goal state after:
case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ ↑(opLinearEquiv R) (m * n) ∈ comap (↑(opLinearEquiv R).symm) N * comap (↑(opLinearEquiv R).symm) M
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h
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}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)

Tactic:
mul_assoc,

Goal state after:
case h
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}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * (μ x * ∏ j ∈ insert a t \ {x}, s j)) =
    v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)
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
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R)) (M ^ n) = comap (↑(opLinearEquiv R)) M ^ n

Tactic:
comap_op_pow

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R)) M ^ n = comap (↑(opLinearEquiv R)) M ^ n
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ I = (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)

Tactic:
apply Ideal.ext

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ ∀ (x : R × S), x ∈ I ↔ x ∈ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
⊢ IsNoetherian R M ↔ IsNoetherian S P

Tactic:
simp_rw [isNoetherian_iff']

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
⊢ WellFoundedGT (Submodule R M) ↔ WellFoundedGT (Submodule S P)
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
inst✝ : RingHomClass F R S
ι : Type u_4
s : Finset ι
K : ι → Ideal S
⊢ comap f (s.inf K) = s.inf fun i ↦ comap f (K i)

Tactic:
simp [Finset.inf_eq_iInf, comap_iInf]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (⨆ a ∈ ⇑(algebraMap R S) '' ↑I, a • N) = ⨆ a ∈ ↑I, a • Submodule.restrictScalars R N

Tactic:
← element_smul_restrictScalars,

Goal state after:
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (⨆ a ∈ ⇑(algebraMap R S) '' ↑I, a • N) =
    ⨆ a ∈ ↑I, Submodule.restrictScalars R ((algebraMap R S) a • N)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inr
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * b * d / a = b * d

Tactic:
mul_assoc,

Goal state after:
case inr
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * (b * d) / a = b * d
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
x : R
⊢ f x ∈ map f I ↔ x ∈ I

Tactic:
rw [← comap_symm, Ideal.mem_comap, f.symm_apply_apply]

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 : ¬gcd x y = 0
z : R
hz : y = gcd x y * z
⊢ x * gcd x y * z = x * y

Tactic:
mul_assoc,

Goal state after:
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 * (gcd x y * z) = x * y
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ comap f (map f p) = p ↔ ∃ q, q.IsPrime ∧ comap f q = p

Tactic:
refine ⟨fun hp ↦ ?_, ?_⟩
  · obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_le_prime_disjoint _ _
      (disjoint_map_primeCompl_iff_comap_le.mpr hp.le)
    exact ⟨q, hq₁, le_antisymm (disjoint_map_primeCompl_iff_comap_le.mp hq₃)
      (map_le_iff_le_comap.mp hq₂)⟩
  · rintro ⟨q, hq, rfl⟩
    simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
⊢ 1 ≤ J ^ 0

Tactic:
Submodule.pow_zero

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
⊢ 1 ≤ 1
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
⊢ g * (g * r * y / g) = g * r * y

Tactic:
mul_assoc,

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
⊢ g * (g * (r * y) / g) = g * (r * y)
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:
exact add_mul_div_left _ _ _ h1 h2

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

Tactic:
mul_assoc,

Goal state after:
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)) + t * y * (z / t) = t * x + y * z
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 * x + y * t * (z / t) = t * x + y * z

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ t * x + y * (t * (z / t)) = t * x + y * z
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) - t * y * (z / t) = t * x - y * z

Tactic:
mul_assoc,

Goal state after:
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)) - t * y * (z / t) = t * x - y * z
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 * x - y * t * (z / t) = t * x - y * z

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ t * x - y * (t * (z / t)) = t * x - y * z
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
⊢ t * a * y = t * (y * a)

Tactic:
mul_assoc,

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:
rw [mul_comm, annihilator_mul]

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✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst✝² : EquivLike F' R S
inst✝¹ : RingEquivClass F' R S
f : F'
I : Ideal R
inst✝ : I.IsPrime
h : map f I = map (↑↑f) I
⊢ (map (↑↑f) I).IsPrime

Tactic:
map_comap_of_equiv (RingEquivClass.toRingEquiv f : R ≃+* S)

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst✝² : EquivLike F' R S
inst✝¹ : RingEquivClass F' R S
f : F'
I : Ideal R
inst✝ : I.IsPrime
h : map f I = map (↑↑f) I
⊢ (comap (↑f).symm I).IsPrime
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
hn : 0 ≠ 0
⊢ ↑0 = ⊤

Tactic:
exact (hn rfl).elim

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

Goal state before:
pp: case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ z * ↑(-1) = -z

Tactic:
Units.val_neg,

Goal state after:
case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ z * -↑1 = -z
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case h
a : ℤ
h : a = -↑a.natAbs
⊢ ↑a.natAbs = -1 * a

Tactic:
rw [← neg_eq_iff_eq_neg.mpr h]

Goal state after:
case h
a : ℤ
h : a = -↑a.natAbs
⊢ -a = -1 * a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I ⊔ J = ⊤
⊢ 1 * I + 1 * J = 1

Tactic:
simpa only [one_eq_top, top_mul, Submodule.add_eq_sup]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ ↑u * b * (f.erase b).prod = f.prod * ↑u

Tactic:
mul_assoc,

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ ↑u * (b * (f.erase b).prod) = f.prod * ↑u
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
by_cases h : a = 0 ∨ b = 0
  · rcases h with (rfl | rfl) <;>
      simp +contextual only [iff_def, lcm_zero_left, lcm_zero_right,
        zero_dvd_iff, dvd_zero, and_true, imp_true_iff]
  · obtain ⟨h1, h2⟩ := not_or.1 h
    have h : gcd a b ≠ 0 := fun H => h1 ((gcd_eq_zero_iff _ _).1 H).1
    rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]

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

Goal state before:
pp: case pos
α : 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
⊢ Associated (b * lcm a b) (a * b)

pp: case pos
α : 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
⊢ Associated (a * lcm a b) (a * b)

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
⊢ Associated (Classical.choose ⋯ * lcm a b) (a * b)

Tactic:
· rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]

Goal state after:
case pos
α : 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
⊢ Associated (a * lcm a b) (a * b)

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
⊢ Associated (Classical.choose ⋯ * lcm a b) (a * b)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ (↑(f b) ∪ ↑(f i)) ∪ ⋃ x ∈ ↑t, ↑(f x)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)

Tactic:
Set.union_eq_self_of_subset_left Hb

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)