mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
⊢ ⨆ a ∈ s, (lsingle a).range ≤ ⨅ a ∈ t, (lapply a).ker

Tactic:
refine iSup_le fun a₁ => iSup_le fun h₁ => range_le_iff_comap.2 ?_
  simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
  intro b _ a₂ h₂
  have : a₂ ≠ a₁ := fun eq => h.le_bot ⟨h₁, eq.symm ▸ h₂⟩
  exact single_eq_of_ne this

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[X]
n : ℕ
⊢ (a ^ n).toFinsupp = a.toFinsupp ^ n

Tactic:
by
  rw [← ofFinsupp_pow]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case single
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : α
b : M
⊢ single a b ∈ span R {x | ∃ i x_1, single i x_1 = x}

Tactic:
| single a b =>

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

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : SMulCommClass S₁ S₂ R
⊢ ∀ (m : S₁) (n : S₂) (a : R[X]), m • n • a = n • m • a

Tactic:
rintro m n ⟨f⟩
    simp_rw [← ofFinsupp_smul, smul_comm m n f]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * (X ^ n * q) = p * q * X ^ n

Tactic:
X_pow_mul,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * (q * X ^ n) = p * q * X ^ n
Module: Mathlib.Algebra.Polynomial.Basic

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

Tactic:
X_pow_mul,

Goal state after:
R : Type u
inst✝ : Semiring R
k n : ℕ
r : R
⊢ (monomial n) r * X ^ k = (monomial (n + k)) r
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f g : ℕ → R → S
⊢ p.sum (f + g) = p.sum f + p.sum g

Tactic:
simp [sum_def, Finset.sum_add_distrib]

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

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := ⋯
⊢ ∀ (x : Finset ((i : ι) → G i)),
    (∀ y ⊂ x, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0) →
      ∀ {B : Finset ((i : ι) → G i)}, x.Nonempty → B.Nonempty → ∃ a0 ∈ x, ∃ b0 ∈ B, UniqueMul x B a0 b0

Tactic:
intro A

Goal state after:
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
⊢ (∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0) →
    ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
u : G
⊢ (Pi.single s 1 * Pi.single x✝¹ 1) u = 0 u

Tactic:
by_cases u = s <;> simp_all

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
x✝¹ x✝ : ι →₀ M →ₗ[R] N
eq : (finsuppLinearMap S) x✝¹ = (finsuppLinearMap S) x✝
i : ι
m : M
⊢ (x✝¹ i) m = (x✝ i) m

Tactic:
exact congr($eq m i)

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

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := ⋯
⊢ ∀ (x : Finset ((i : ι) → G i)),
    (∀ y ⊂ x,
        ∀ {B : Finset ((i : ι) → G i)},
          1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2) →
      ∀ {B : Finset ((i : ι) → G i)},
        1 < #x * #B → ∃ p1 ∈ x ×ˢ B, ∃ p2 ∈ x ×ˢ B, p1 ≠ p2 ∧ UniqueMul x B p1.1 p1.2 ∧ UniqueMul x B p2.1 p2.2

Tactic:
intro A

Goal state after:
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
⊢ (∀ y ⊂ A,
      ∀ {B : Finset ((i : ι) → G i)},
        1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2) →
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ (ofIsCompl hpq φ ψ).range = φ.range ⊔ ψ.range

Tactic:
rw [ofIsCompl_eq_add]

Goal state after:
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
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range = φ.range ⊔ ψ.range
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : Surjective ⇑g
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ Module.Finite R N

Tactic:
refine ⟨(⊤ : Submodule R _).fg_of_fg_map_of_fg_inf_ker g ?_ ?_⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : Surjective ⇑g
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ (map g ⊤).FG

case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : Surjective ⇑g
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ (⊤ ⊓ g.ker).FG
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
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
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
⊢ ∀ (m : R₁) (x : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)),
    ofIsCompl h (m • x).1 (m • x).2 = (RingHom.id R₁) m • ofIsCompl h x.1 x.2

Tactic:
intro c φ

Goal state after:
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
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
c : R₁
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
⊢ ofIsCompl h (c • φ).1 (c • φ).2 = (RingHom.id R₁) c • ofIsCompl h φ.1 φ.2
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)
  · rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, iInf_eq_bot.2, bot_eq_zero]
    exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩
  simp_rw [not_exists, not_lt] at h
  refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
    ENat.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
    add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
    iSup_le fun i ↦ ?_
  rw [← ENat.sub_sub_cancel ha (h _)]
  exact tsub_le_tsub_left (iInf_le (a - f ·) i) _

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : M × P
e : f x.1 + ↑l x.2 = f y.1 + ↑l y.2
this : x.2 = y.2
⊢ f x.1 = f y.1

Tactic:
by rwa [this, add_left_inj] at e

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

Goal state before:
pp: R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a

Tactic:
exact DistribMulActionHom.congr_fun h a

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
⊢ ↑p.length ≤ height x

Tactic:
by
  by_cases hlen0 : p.length ≠ 0
  · let p' := p.eraseLast.snoc x (by
      apply lt_of_lt_of_le
      · apply p.step ⟨p.length - 1, by lia⟩
      · convert! hlast
        simp only [Fin.succ_mk, RelSeries.last, Fin.last]
        congr; lia)
    suffices p'.length ≤ height x by
      simp only [RelSeries.snoc_length, RelSeries.eraseLast_length, Nat.cast_add, ENat.natCast_sub,
        Nat.cast_one, p'] at this
      convert! this
      norm_cast
      lia
    refine le_iSup₂_of_le p' ?_ le_rfl
    simp [p']
  · simp_all

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 : (p.cons x hx).head = f a
⊢ ↑(p.cons x hx).length ≤ coheight a

Tactic:
simp only [RelSeries.head_cons] at hp
    obtain ⟨a', haa', ha'⟩ := h a p.head (by grind)
    grw [RelSeries.cons_length, Nat.cast_add, Nat.cast_one, ih a' ha'.symm]
    exact coheight_add_one_le haa'

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
⊢ s.length < Fintype.card α

Tactic:
by_contra! h
  obtain ⟨i, j, hn, he⟩ := Fintype.exists_ne_map_eq_of_card_lt s (by rw [Fintype.card_fin]; lia)
  wlog hl : i < j generalizing i j
  · exact this j i hn.symm he.symm (by lia)
  exact absurd he (s.strictMono hl).ne

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ ∃ a ∈ Finset.univ, (injStrictMono (Fintype.card α)) a = { length := l, toFun := f, step := mf }

Tactic:
Finset.mem_univ,

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ ∃ a, True ∧ (injStrictMono (Fintype.card α)) a = { length := l, toFun := f, step := mf }
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ ∃ p, RelSeries.head p = a ∧ p.length = m

Tactic:
use { length := m, toFun := fun i => if i = 0 then a else f i, step := ?step }

Goal state after:
case h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ { length := m, toFun := fun i ↦ if i = 0 then a else ↑(f ↑i), step := ?step }.head = a ∧
    { length := m, toFun := fun i ↦ if i = 0 then a else ↑(f ↑i), step := ?step }.length = m

case step
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ ∀ (i : Fin m),
    (if i.castSucc = 0 then a else ↑(f ↑i.castSucc), if i.succ = 0 then a else ↑(f ↑i.succ)) ∈ {(a, b) | a < b}
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
n : ℕ
h' : height (f x) = ↑n
⊢ height x ≤ (↑m + 1) * ↑n + ↑m

Tactic:
induction n using Nat.strong_induction_on generalizing x with | h n ih =>
    refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_
    let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩
    suffices h'' : f (p i) < f x by
      obtain ⟨n', hn'⟩ : ∃ (n' : ℕ), n' = height (f (p i)) := ENat.ne_top_iff_exists.mp
        ((height_mono h''.le).trans_lt (h' ▸ ENat.natCast_lt_top _)).ne
      have h_lt : n' < n := ENat.natCast_lt_natCast.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.natCast_lt_top _))
      have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
      rw [RelSeries.take_length, ENat.natCast_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
      refine not_lt_of_ge ?_ (h_len.trans_le this)
      gcongr
      rwa [← ENat.natCast_one, ← ENat.natCast_add, ENat.natCast_le_natCast]
    refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_
    let q' : LTSeries α := p.drop i
    let q : LTSeries (f ⁻¹' {f x}) := ⟨q'.length, fun j ↦ ⟨q' j, le_antisymm
      (f.monotone (le_trans (b := q'.last) (q'.monotone (Fin.le_last _)) (p.last_drop _ ▸ hp)))
      (le_trans (b := f q'.head) (p.head_drop _ ▸ h'')
        (f.monotone (q'.monotone (Fin.zero_le _))))⟩, fun i ↦ q'.step i⟩
    have := (LTSeries.length_le_krullDim q).trans (h (f x))
    simp only [RelSeries.drop_length, Nat.cast_le, tsub_le_iff_right, q', i, q] at this
    have : p.length > m := ENat.natCast_lt_natCast.mp ((le_add_left le_rfl).trans_lt h_len)
    lia

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

Goal state before:
pp: case insert.mp
ι : 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 : α
⊢ (∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) →
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a

Tactic:
rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩

Goal state after:
case insert.mp
ι : 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
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∃ g_1, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g_1 i_1 ∈ f i_1), g_1 i * ∏ i ∈ is, g_1 i = x * ∏ i ∈ is, g i
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case refine_2
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
t : M ⊗[R] N
⊢ ∀ (x : M) (y : N), x ⊗ₜ[R] y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

pp: case refine_3
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
t : M ⊗[R] N
⊢ ∀ (x y : M ⊗[R] N),
    x ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
      y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → x + y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
· intro m n
    apply Submodule.subset_span
    use m, n

Goal state after:
case refine_3
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
t : M ⊗[R] N
⊢ ∀ (x y : M ⊗[R] N),
    x ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
      y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → x + y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

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

Tactic:
← span_tmul_eq_top,

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

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ (m + n) * p ∈ M * P ⊔ N * P

Tactic:
right_distrib

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ m * p + n * p ∈ M * P ⊔ N * P
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
x✝¹ x✝ : R
⊢ x✝¹ * t ∈ ⨆ i, S i * T → x✝ * t ∈ ⨆ i, S i * T → (x✝¹ + x✝) * t ∈ ⨆ i, S i * T

Tactic:
right_distrib

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
x✝¹ x✝ : R
⊢ x✝¹ * t ∈ ⨆ i, S i * T → x✝ * t ∈ ⨆ i, S i * T → x✝¹ * t + x✝ * t ∈ ⨆ i, S i * T
Module: Mathlib.LinearAlgebra.TensorProduct.Map

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

Tactic:
by
  simp only [← coe_rTensorHom]
  exact (rTensorHom (R := R) (N := N) (P := P) Q).map_sub f g

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

Goal state before:
pp: A : Type u
inst✝¹ : CommRing A
inst✝ : Nontrivial A
a b : ℕ
h : a.Coprime b
⊢ IsCoprime ↑a ↑b

Tactic:
simpa only [map_natCast] using IsCoprime.map (Nat.Coprime.isCoprime h) (Int.castRingHom A)

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
⊢ ∃ tr, ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j

Tactic:
use fun i ↦ (this i).choose

Goal state after:
case h
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := ⋯
sli : List α := ⋯
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
⊢ ∀ (i j : Fin n), val i ≤ val j ↔ (fun i ↦ ↑↑⋯.choose) i ≤ (fun i ↦ ↑↑⋯.choose) j
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
⊢ comap (↑(opLinearEquiv R).symm) 1 = 1

Tactic:
rw [← map_equiv_eq_comap_symm, map_op_one]

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
⊢ map (↑RingEquiv.prodComm) (I.prod J) = J.prod I

Tactic:
refine Trans.trans (ideal_prod_eq _) ?_

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ (map (RingHom.fst S R) (map (↑RingEquiv.prodComm) (I.prod J))).prod
      (map (RingHom.snd S R) (map (↑RingEquiv.prodComm) (I.prod J))) =
    J.prod I
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd a b ∣ a ∧ gcd a b ∣ b

Tactic:
rw [gcd_val]
    exact ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩

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

Goal state before:
pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (a : R),
    ∀ x ∈ span R (↑I • Set.range f),
      (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) →
        ∃ a_2, ∃ (_ : ∀ (i : ι), a_2 i ∈ I), (a_2.sum fun i c ↦ c • f i) = a • x

Tactic:
rintro c x - ⟨a, ha, rfl⟩

Goal state after:
case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∃ a_1, ∃ (_ : ∀ (i : ι), a_1 i ∈ I), (a_1.sum fun i c ↦ c • f i) = c • a.sum fun i c ↦ c • f 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 : x = gcd x y * z
⊢ gcd x y * (y * z) = x * y

Tactic:
by rw [← mul_assoc, mul_right_comm, ← hz]

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ z = x * (g * s) / g * p

Tactic:
rw [mul_left_comm, mul_div_cancel_left₀ _ hxy, ← mul_left_inj' hxy, hp]

Goal state after:
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ x * (g * s) * p = x * s * p * g
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : J.IsTwoSided
a✝ b : R
ha : a✝ ∈ I * J
x y : R
hx : x * b ∈ I * J
hy : y * b ∈ I * J
⊢ (x + y) * b ∈ I * J

Tactic:
right_distrib

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : J.IsTwoSided
a✝ b : R
ha : a✝ ∈ I * J
x y : R
hx : x * b ∈ I * J
hy : y * b ∈ I * J
⊢ x * b + y * b ∈ I * J