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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : x = f a
⊢ f a < p.head

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : x = f a
a' : α
haa' : a < a'
ha' : f a' = p.head
⊢ ↑(p.length + 1) ≤ coheight a

Tactic:
Nat.cast_add,

Goal state after:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : x = f a
a' : α
haa' : a < a'
ha' : f a' = p.head
⊢ ↑p.length + ↑1 ≤ coheight a
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.Order.KrullDimension

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

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

Tactic:
· simp

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ + 1 ≤ ↑n ↔ ↑a✝ < ↑n
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ.refine_1.refine_1
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length) j.castSucc
⊢ Fin.last { length := n + 1, toFun := s, step := h }.length = j.castSucc

pp: case succ.refine_1.refine_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length) j.castSucc
⊢ j.castSucc = Fin.last { length := n + 1, toFun := s, step := h }.length

Tactic:
all_goals
        rw [Fin.snoc_castSucc] at eq
        obtain rfl : m = 0 := by simpa [t₃] using! (congr_arg Fin.val eq).trans_lt (i j).2
        cases (h (.last _)).ne' (h₂.symm.trans h₁)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
l : Fin (0 + 1) → α
h : ∀ (i : Fin 0), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
⊢ ↑{ length := 0, toFun := l, step := h }.length ≤ 0

pp: case succ
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
n : ℕ
l : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
⊢ ↑{ length := n + 1, toFun := l, step := h }.length ≤ 0

Tactic:
· simp

Goal state after:
case succ
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
n : ℕ
l : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
⊢ ↑{ length := n + 1, toFun := l, step := h }.length ≤ 0
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m₁ m₂ : M
n : N
⊢ (SMul.aux r) (FreeAddMonoid.of (m₁, n) + FreeAddMonoid.of (m₂, n)) = (SMul.aux r) (FreeAddMonoid.of (m₁ + m₂, n))

Tactic:
simp_rw [map_add, SMul.aux_of, smul_add, add_tmul]

Goal state after:
Module: Mathlib.Order.RelSeries

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

Tactic:
rw [← h₁, RelSeries.head, RelSeries.head, ← hi₁, ← hit, Function.comp]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_7
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_22
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
s : S
m : M
⊢ s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

Tactic:
nth_rw 1 [← mul_one s, ← smul_eq_mul, smul_tmul']

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length - ↑(m + 1) ≤ (↑m + 1) * ↑n' + ↑m
⊢ False

Tactic:
Nat.cast_add,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length - (↑m + ↑1) ≤ (↑m + 1) * ↑n' + ↑m
⊢ False
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r x y : R
hr : r ∈ R⁰
⊢ x * r ∣ y * r ↔ x ∣ y

Tactic:
simp_rw [← mul_comm r, dvd_cancel_left_mem_nonZeroDivisors hr]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : IdemSemiring α
n x : ℕ
hmn✝ : 1 ≤ x
hx : ↑x = 1
⊢ ↑(x + 1) = 1

Tactic:
Nat.cast_add,

Goal state after:
case succ
α : Type u_1
inst✝ : IdemSemiring α
n x : ℕ
hmn✝ : 1 ≤ x
hx : ↑x = 1
⊢ ↑x + ↑1 = 1
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ m • np ∈ M • N ⊔ M • P

Tactic:
by
    refine closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)
    · rintro x (hx | hx)
      exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx),
        le_sup_right (a := M • N) (smul_mem_smul hm hx)]
    · apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem
    · intro _ _ _ _ h1 h2; rw [smul_add]; exact add_mem h1 h2

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
x y : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x ≠ 0 ∨ y ≠ 0

Tactic:
apply not_or_of_imp

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
x y : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x = 0 → y ≠ 0
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
by rwa [mul_right_comm, mul_assoc]

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

Goal state before:
pp: case succ.succ
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
n : ℕ
ih : n + 1 ≠ 0 → (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
h : n + 1 + 1 ≠ 0
⊢ (M ^ (n + 1)).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid

Tactic:
| succ n =>

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

Goal state before:
pp: case cons
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)
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)

Tactic:
| cons a t hat h ih =>

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
⊢ ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i)

Tactic:
by
  let := Classical.decEq ι
  refine Finset.induction_on s ?_ ?_
  · simp [one_eq_span, Set.singleton_one]
  · intro _ _ H ih
    rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]

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

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
⊢ span (∅ ×ˢ ∅) = (span ∅).prod (span ∅)

Tactic:
· simp

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 S
h : (⊤.prod I).IsPrime
⊢ I.IsPrime

Tactic:
apply isPrime_of_isPrime_prod_top (S := R)
  rw [← map_prodComm_prod]
  -- Note: couldn't synthesize the right instances without the `R` and `S` hints
  exact map_isPrime_of_equiv (RingEquiv.prodComm (R := R) (S := S))

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
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
⊢ Injective ⇑f

Tactic:
replace hi : Injective i' := by simpa [i'] using hi

Goal state after:
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
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
⊢ Injective ⇑f
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
m : ℕ
f' : (Fin m → R) →ₗ[R] M
hf' : Surjective ⇑f'
⊢ ∃ P x x_1, ∃ (_ : Free R P) (_ : Module.Finite R P), ∃ f, Surjective ⇑f

Tactic:
let f := f'.comp ((Finsupp.mapRange.linearEquiv (Shrink.linearEquiv.{v} R R)).trans
      (Finsupp.linearEquivFunOnFinite R R (Fin m))).1

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
m : ℕ
f' : (Fin m → R) →ₗ[R] M
hf' : Surjective ⇑f'
f : (Fin m →₀ Shrink.{v, u} R) →ₗ[R] M :=
  f' ∘ₗ ↑(Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) ≪≫ₗ Finsupp.linearEquivFunOnFinite R R (Fin m))
⊢ ∃ P x x_1, ∃ (_ : Free R P) (_ : Module.Finite R P), ∃ f, Surjective ⇑f
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 ι
inst✝ : ∀ (i : ι), IsPrincipalIdealRing (R i)
I : Ideal ((i : ι) → R i)
⊢ Submodule.IsPrincipal I

Tactic:
rw [← piOrderIso.symm_apply_apply I]
    exact ⟨_, congr(pi $(funext fun i ↦
      (Submodule.IsPrincipal.span_singleton_generator _).symm)).trans pi_span⟩

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I ↔ ∃ x ∈ I, e x = y

Tactic:
by
  constructor
  · intro h
    simp_rw [show map e I = _ from map_comap_of_equiv (RingEquivClass.toRingEquiv e : R ≃+* S)] at h
    exact ⟨(EquivLike.toEquiv e).symm y, h, (EquivLike.toEquiv e).apply_symm_apply y⟩
  · rintro ⟨x, hx, rfl⟩
    exact mem_map_of_mem e hx

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
J : Ideal S
K : Ideal R
h : φ J < K
⊢ J < map f K

Tactic:
← J.map_comap_of_surjective f hf

Goal state after:
case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
J : Ideal S
K : Ideal R
h : φ J < K
⊢ map f (comap f J) < map f K
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : EuclideanDomain R
a b d : R
hbd : d ∣ b
hac : 0 ∣ a
⊢ a * b / (0 * d) = a / 0 * (b / d)

pp: case inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
· simp

Goal state after:
case inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inr.inl
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)

pp: case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
· simp

Goal state after:
case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
Module: Mathlib.RingTheory.Ideal.Maps

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

Tactic:
intro a x _ hx

Goal state after:
case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
a : R
x : M
hx✝ : x ∈ span R s
hx : r • x = 0
⊢ r • a • x = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case mpr.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ 0 → x = 0) → gcd 0 = 0

pp: case mpr.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → x = 0) → s.gcd = 0) → (∀ (x : α), x ∈ a ::ₘ s → x = 0) → (a ::ₘ s).gcd = 0

Tactic:
· simp

Goal state after:
case mpr.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → x = 0) → s.gcd = 0) → (∀ (x : α), x ∈ a ::ₘ s → x = 0) → (a ::ₘ s).gcd = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
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
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : map f I = ⊤
⊢ ⊤ ≤ I

Tactic:
replace h := congr_arg (comap f) h
    rw [comap_map_of_surjective _ hf, comap_top] at h
    exact h ▸ sup_le (le_of_eq rfl) hk

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

Goal state before:
pp: case inl
h : 0 ≤ 0
⊢ normalize 0 = -0

pp: case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ normalize z = -z

Tactic:
· simp

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

Goal state before:
pp: ⊢ Associates ℤ ≃ ℕ

Tactic:
refine ⟨(·.out.natAbs), (Associates.mk ·), ?_, fun n ↦ ?_⟩
  · refine Associates.forall_associated.2 fun a ↦ ?_
    refine Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, ?_⟩
    simp [Int.natCast_natAbs, Int.abs_eq_normalize, normalize_apply]
  · dsimp only [Associates.out_mk]
    rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ I = span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

Tactic:
simp only [le_antisymm_iff, le_span_singleton_mul_iff, span_singleton_mul_le_iff]

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

Goal state before:
pp: case refine_2.refine_1
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ {x ∈ ∅ | f x = 0}.gcd f = 0

pp: case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ ∀ (a : β) (s : Finset β), a ∉ s → {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0

Tactic:
· simp

Goal state after:
case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ ∀ (a : β) (s : Finset β), a ∉ s → {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
⊢ (if f a = 0 then insert a ({x ∈ s | f x = 0}) else {x ∈ s | f x = 0}).gcd f = 0

Tactic:
split_ifs with h1

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
h1 : f a = 0
⊢ (insert a ({x ∈ s | f x = 0})).gcd f = 0

case neg
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
h1 : ¬f a = 0
⊢ {x ∈ s | f x = 0}.gcd f = 0
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_1
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∅.gcd fun x ↦ a * f x) = normalize a * ∅.gcd f

pp: case refine_2
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ ∀ (a_1 : β) (s : Finset β),
    a_1 ∉ s →
      (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f →
        ((insert a_1 s).gcd fun x ↦ a * f x) = normalize a * (insert a_1 s).gcd f

Tactic:
· simp

Goal state after:
case refine_2
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ ∀ (a_1 : β) (s : Finset β),
    a_1 ∉ s →
      (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f →
        ((insert a_1 s).gcd fun x ↦ a * f x) = normalize a * (insert a_1 s).gcd f