mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case pos
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

pp: case neg
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : ¬x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

Tactic:
· rw [h1, zero_mul]

Goal state after:
case neg
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : ¬x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩ ≤ s.min' H

Tactic:
have : s.min' H ∈ l := (s.mem_sort (· ≤ ·)).mpr (s.min'_mem H)
    obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this
    rw [← hi]
    exact (s.pairwise_sort (· ≤ ·)).rel_get_of_le (Nat.zero_le 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
x y : G × H
⊢ (fun t ↦ Bool.rec { down := (x * y).1 } { down := (x * y).2 } t) =
    (fun t ↦ Bool.rec { down := x.1 } { down := x.2 } t) * fun t ↦ Bool.rec { down := y.1 } { down := y.2 } t

Tactic:
by ext (_ | _) <;> rfl

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℕ
⊢ ↑(s ^ Int.negSucc n) = ↑s ^ Int.negSucc n

Tactic:
refine (coe_inv _).trans ?_
    exact congr_arg Inv.inv (coe_pow _ _)

Goal state after:
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
f : α →₀ M
x✝ : f ∈ ⊤
⊢ f ∈ ⨆ a, (lsingle a).range

Tactic:
rw [← sum_single f]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α →₀ M
x✝ : f ∈ ⊤
⊢ f.sum single ∈ ⨆ a, (lsingle a).range
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 : Set M
a : α
⊢ span R (single a '' s) = map (lsingle a) (span R s)

Tactic:
by
  rw [← span_image]; rfl

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:
by
    rintro m n ⟨f⟩
    simp_rw [← ofFinsupp_smul, smul_comm m n f]

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L = M ↔ L = map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M

Tactic:
← coe_inj

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ ↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L) = ↑M ↔
    ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M)
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ pi univ L = ⊥ ↔ ∃ i, L i = ⊥

Tactic:
← coe_inj

Goal state after:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ ↑(pi univ L) = ↑⊥ ↔ ∃ i, ↑(L i) = ↑⊥
Module: Mathlib.Algebra.Polynomial.Basic

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

Tactic:
rw [← C_mul_X_pow_eq_monomial, pow_one]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a} = ⊤

Tactic:
apply top_unique
  rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ← addSubmonoidClosure_single,
    AddMonoidHom.map_mclosure]
  refine AddSubmonoid.closure_mono (Set.image_subset_iff.2 ?_)
  rintro _ ⟨n, a, rfl⟩
  exact ⟨n, a, Polynomial.ofFinsupp_single _ _⟩

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl p q

Tactic:
simp [isCompl_iff]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R N
e : M ≃ₗ[R] N
p : Submodule R M
⊢ Submodule.map (↑e) p ∈ f.invtSubmodule ↔ p ∈ (e.symm.conj f).invtSubmodule

Tactic:
by
  simp [← e.map_mem_invtSubmodule_conj_iff]

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 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ 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)
hA : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
⊢ B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
hB

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)
ihA : ∀ 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)
hA : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
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)
⊢ ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
classical
    let _ := isWellFounded_ssubset (α := ∀ i, G i) -- why need this?
    apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B hA
    apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hB
    by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1
    · exact of_card_le_one hA hB hc.1 hc.2
    obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)
    obtain ⟨ai, hA, bi, hB, hi⟩ := uniqueMul_of_nonempty (hA.image (· i)) (hB.image (· i))
    rw [mem_image, ← filter_nonempty_iff] at hA hB
    let A' := {a ∈ A | a i = ai}; let B' := {b ∈ B | b i = bi}
    obtain ⟨a0, ha0, b0, hb0, hu⟩ : ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0 := by
      rcases hc with hc | hc; · exact ihA A' (hc.2 ai) hA hB
      by_cases hA' : A' = A
      · rw [hA']
        exact ihB B' (hc.2 bi) hB
      · exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB
    rw [mem_filter] at ha0 hb0
    exact ⟨a0, ha0.1, b0, hb0.1, of_image_filter (Pi.evalMulHom G i) ha0.2 hb0.2 hi hu⟩

Goal state after:
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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (g ∘ₗ f).ker.FG

Tactic:
LinearMap.ker_comp

Goal state after:
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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (comap f g.ker).FG
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝¹² : Monoid R
inst✝¹¹ : Monoid S
inst✝¹⁰ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁹ : NonUnitalNonAssocSemiring A
inst✝⁸ : DistribMulAction R A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : DistribMulAction S B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝³ : NonUnitalNonAssocSemiring B₁
inst✝² : DistribMulAction R B₁
inst✝¹ : DistribMulAction R B
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ Function.prod (⇑f) (⇑g) 0 = 0

Tactic:
by simp only [Function.prod_apply, Prod.mk_zero_zero, map_zero]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
newHead : α
rel : (newHead, p.head) ∈ r
⊢ (p.cons newHead rel).last = p.last

Tactic:
by
  delta cons
  rw [last_append]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
p : RelSeries r
n : ℕ
heq : p.length = n
⊢ motive p

Tactic:
by
    induction n generalizing p with
    | zero =>
      convert! singleton p.head
      ext n
      · exact heq
      simp [show n = 0 by lia, apply_zero]
    | succ d hd =>
      have lq := p.tail_length (heq ▸ d.zero_ne_add_one.symm)
      nth_rw 3 [heq] at lq
      convert!
        cons (p.tail (heq ▸ d.zero_ne_add_one.symm)) p.head (p.3 ⟨0, heq ▸ d.zero_lt_succ⟩)
          (hd _ lq)
      exact (p.cons_self_tail (heq ▸ d.zero_ne_add_one.symm)).symm

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map₂ f p q = map₂ f p (span R ↑q)

Tactic:
span_eq

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map₂ f p q = map₂ f p q
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map₂ f.flip q p = map₂ f p q

Tactic:
map₂_eq_span_image2,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun m n ↦ (f.flip m) n) ↑q ↑p) = map₂ f p q
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun m n ↦ (f.flip m) n) ↑q ↑p) = map₂ f p q

Tactic:
map₂_eq_span_image2,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun m n ↦ (f.flip m) n) ↑q ↑p) = span R (image2 (fun m n ↦ (f m) n) ↑p ↑q)
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range ≤ g.ker
hg : Function.Surjective ⇑g
x₂ : N
⊢ ∃ a, (f.range.liftQ g h) a = g x₂

Tactic:
exact ⟨Submodule.Quotient.mk x₂, rfl⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
apply height_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries α), RelSeries.last p = x → ↑p.length ≤ ⨆ y, ⨆ (_ : y < x), height y + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ ∃ x < RelSeries.last p, ↑n ≤ height x

Tactic:
use p.eraseLast.last, p.eraseLast_last_rel_last (by lia)

Goal state after:
case right
α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ ↑n ≤ height (RelSeries.eraseLast p).last
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
motive : M ⊗[R] N → Prop
z : M ⊗[R] N
zero : motive 0
tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)
add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)
x : FreeAddMonoid (M × N)
x✝ : M × N
y : FreeAddMonoid (M × N)
ih : motive ↑y
m : M
n : N
⊢ motive ↑(FreeAddMonoid.of (m, n) + y)

Tactic:
by
      rw [AddCon.coe_add]
      exact add _ _ (tmul ..) ih

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⊥ ↔ IsEmpty α

Tactic:
rw [eq_bot_iff, krullDim, iSup_le_iff]

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (i : LTSeries α), ↑i.length ≤ ⊥) ↔ IsEmpty α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ ∃ i, 1 < ↑i.length

Tactic:
exact ⟨⟨2, ![y, x, z], fun i ↦ by fin_cases i <;> simpa⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ krullDim α < ↑n ↔ ∀ (l : LTSeries α), l.length < n

Tactic:
by
  rw [krullDim, ← WithBot.coe_natCast]
  rcases n with - | n
  · rw [ENat.natCast_zero, ← bot_eq_zero, WithBot.lt_coe_bot]
    simp
  · simp [ENat.WithBot.lt_add_one_iff, WithBot.coe_natCast]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α = ↑(⨆ a, coheight a)

Tactic:
simpa using! krullDim_eq_iSup_height_of_nonempty (α := αᵒᵈ)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑⟨i, hi⟩

Tactic:
simp only at *

Goal state after:
p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, hj⟩ + i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℤ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑↑⟨i, hi⟩

Tactic:
simp only at *

Goal state after:
p : LTSeries ℤ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun ⟨j, hj⟩ + ↑i
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P₂
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R₂ P₂
g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H : (mk R M N).compr₂ₛₗ g = (mk R M N).compr₂ₛₗ h
⊢ g = h

Tactic:
← lift_mk_compr₂ₛₗ g,

Goal state after:
R : Type u_1
R₂ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P₂
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R₂ P₂
g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H : (mk R M N).compr₂ₛₗ g = (mk R M N).compr₂ₛₗ h
⊢ lift ((mk R M N).compr₂ₛₗ g) = h
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x + 1

Tactic:
apply height_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries (WithBot α)), RelSeries.last p = ↑x → ↑p.length ≤ height x + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x

Tactic:
apply height_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries (WithTop α)), RelSeries.last p = ↑x → ↑p.length ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i ↦ (p.toFun i).untop ⋯, step := ⋯ }
⊢ ↑p.length ≤ height x

Tactic:
have hlast' : p'.last = x := by
      simp only [p', RelSeries.last, WithTop.untop_eq_iff, ← hlast]

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i ↦ (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p.length ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ height ↑x

Tactic:
apply height_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries α), RelSeries.last p = x → ↑p.length ≤ height ↑x
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ y ∈ a, ∃ a, a • y = x) → x ∈ a

Tactic:
rintro ⟨y, hy, r, rfl⟩

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
y : M
hy : y ∈ a
r : R
⊢ r • y ∈ 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
r : R
h : IsUnit r
⊢ R ∙ (algebraMap R A) r = 1

Tactic:
by
  conv_rhs => rw [one_eq_span, ← span_singleton_smul_eq h, ← algebraMap_eq_smul_one]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
n : ℕ
⊢ M ^ n = span R ↑M ^ n

Tactic:
span_eq

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
n : ℕ
⊢ M ^ n = M ^ n
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * (s' - b✝ / a✝ * s) + b * (t' - b✝ / a✝ * t)

Tactic:
mul_sub,

Goal state after:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * s' - a * (b✝ / a✝ * s) + b * (t' - b✝ / a✝ * t)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * s' - a * (b✝ / a✝ * s) + b * (t' - b✝ / a✝ * t)

Tactic:
mul_sub,

Goal state after:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * s' - a * (b✝ / a✝ * s) + (b * t' - b * (b✝ / a✝ * t))
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
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x

Tactic:
constructor; swap
  · rintro ⟨a, ha, rfl⟩
    exact Submodule.sum_mem _ fun c _ => smul_mem_smul (ha c) <| subset_span <| Set.mem_range_self _
  refine fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)
  · rintro x ⟨y, hy, x, ⟨i, rfl⟩, rfl⟩
    refine ⟨Finsupp.single i y, fun j => ?_, ?_⟩
    · let := Classical.decEq ι
      rw [Finsupp.single_apply]
      split_ifs
      · assumption
      · exact I.zero_mem
    refine @Finsupp.sum_single_index ι R M _ _ i _ (fun i y => y • f i) ?_
    simp
  · exact ⟨0, fun _ => I.zero_mem, Finsupp.sum_zero_index⟩
  · rintro x y - - ⟨ax, hax, rfl⟩ ⟨ay, hay, rfl⟩
    refine ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩ <;>
      intros <;> simp only [zero_smul, add_smul]
  · rintro c x - ⟨a, ha, rfl⟩
    refine ⟨c • a, fun i => I.mul_mem_left c (ha i), ?_⟩
    rw [Finsupp.sum_smul_index, Finsupp.smul_sum] <;> intros <;> simp only [zero_smul, mul_smul]

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : ι →₀ M), r • m = 0
⊢ ∀ (m : M), r • m = 0

Tactic:
refine Nonempty.elim ‹_› fun i : ι ↦ ?_
    simpa using fun m ↦ congr($(h (Finsupp.single i m)) i)

Goal state after: