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

Goal state before:
pp: case mp.succ.succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl : ∀ (i : Fin (n + 1 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
exact ⟨l 1, ⟨l 0, hl 0⟩, l 2, hl 1⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
simp [krullDim, WithBot.coe_iSup (OrderTop.bddAbove _), WithBot.coe_natCast]

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
krullDim_eq_iSup_coheight_of_nonempty,

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ ↑(⨆ a, coheight a) = ⨆ a, ↑(coheight a)
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

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

Tactic:
rw [ihx, ihy, add_add_add_comm]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : List ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
⊢ (List.map f₁ t).prod ⊆ (List.map f₂ t).prod

Tactic:
by
  induction t with
  | nil => rfl
  | cons h tl ih =>
    simp_rw [List.map_cons, List.prod_cons]
    exact mul_subset_mul (hf h List.mem_cons_self)
      (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)

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

Goal state before:
pp: case negSucc
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
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ Int.negSucc n = congr (f ^ Int.negSucc n) (g ^ Int.negSucc n)

Tactic:
| negSucc n =>

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

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
x : M ⊗[R] N
⊢ _root_.id x = x

Tactic:
_root_.id

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
x : M ⊗[R] N
⊢ x = x
Module: Mathlib.LinearAlgebra.TensorProduct.Map

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
x : N ⊗[R] M
⊢ _root_.id x = x

Tactic:
_root_.id

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
x : N ⊗[R] M
⊢ x = x
Module: Mathlib.LinearAlgebra.TensorProduct.Map

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
x : N ⊗[R] M
⊢ (rTensor M id) x = x

Tactic:
by
  rw [rTensor_id, id_coe, _root_.id]

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

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

Tactic:
add_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ a * x * z + b * y * z
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: case h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x)

pp: case h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (b * y)

Tactic:
· rw [mul_comm z, mul_assoc]
    exact (mul_dvd_mul_left _ H2).mul_left _

Goal state after:
case h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (b * y)
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:
rwa [mul_right_comm, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
this : IsCoprime m n
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
simpa [hn]

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
inst✝ : IsScalarTower R A A
M : Submodule R A
⊢ M ^ 1 = M

Tactic:
by
  rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul]

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
s : Set A
n : ℕ
⊢ span R s ^ n * span R s = span R (s ^ n * s)

Tactic:
span_pow s n,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
n : ℕ
⊢ span R (s ^ n) * span R s = span R (s ^ n * s)
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
⊢ x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
hxy

Goal state after:
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
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:
by
  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.Ideal.Maps

Goal state before:
pp: R : Type u
F : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : FunLike F R S
inst✝¹ : RingHomClass F R S
f : F
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
le : comap f I ≤ P
x✝ : S
⊢ x✝ ∈ ↑I → x✝ ∉ ↑(Submonoid.map f P.primeCompl)

Tactic:
rintro hI ⟨r, hp, rfl⟩

Goal state after:
R : Type u
F : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : FunLike F R S
inst✝¹ : RingHomClass F R S
f : F
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
le : comap f I ≤ P
r : R
hp : r ∈ ↑P.primeCompl
hI : f r ∈ ↑I
⊢ False
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
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
⊢ ⇑f '' ↑I ⊆ ↑(comap g I)

Tactic:
rintro x ⟨x, hx, rfl⟩

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
x : R
hx : x ∈ ↑I
⊢ f x ∈ ↑(comap g I)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u_1
inst✝ : EuclideanDomain R
a b : R
⊢ b * (a / b) + a % b - b * (a / b) = a - b * (a / b)

Tactic:
div_add_mod

Goal state after:
R : Type u_1
inst✝ : EuclideanDomain R
a b : R
⊢ a - b * (a / b) = a - b * (a / b)
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
N : Submodule R M
x : ↥N
⊢ map N.subtype (I • ⊤) = I • N

Tactic:
rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : c ∣ b
⊢ c ∣ b * ?m.21 + a % b ↔ c ∣ a

pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : c ∣ b
⊢ R

Tactic:
div_add_mod

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : c ∣ b
⊢ c ∣ a ↔ c ∣ a
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ ∀ (a_1 : M), a • a_1 = 0 • a_1

Tactic:
simp [Module.mem_annihilator.mp ha]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : gcd x y = 0
⊢ y = 0

Tactic:
rw [EuclideanDomain.gcd_eq_zero_iff] at hgxy

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : x = 0 ∧ y = 0
⊢ y = 0
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_comm y a

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 * (a * y)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
⊢ I ⊔ J ^ (n + 1) = ⊤

Tactic:
J.pow_succ,

Goal state after:
case succ
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
⊢ I ⊔ J ^ n * J = ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
⊢ I = ⊤ ∨ n = 0 → I ^ n = ⊤

Tactic:
rintro (h | h)

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : I = ⊤
⊢ I ^ n = ⊤

case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ I ^ n = ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ x * I + y * J

Tactic:
hxy

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ (p + c * x) * (f + d * y) ∈ m

Tactic:
add_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ p * (f + d * y) + c * x * (f + d * y) ∈ m
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * ↑(Classical.choose ⋯) = a * ↑(Classical.choose ⋯) * (b * ↑(Classical.choose ⋯))

Tactic:
rw [map_mk_unit_aux hinv a, map_mk_unit_aux hinv (a * b), map_mk_unit_aux hinv b, ←
      map_mul, Associates.mk_mul_mk]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a b : α
a0 : a = 0
⊢ Associated (gcd a b * 0) (a * b)

Tactic:
rw [mul_zero, a0, zero_mul]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
a0 : a = 0
⊢ Associated (gcd a b * 0) (a * b)

Tactic:
rw [mul_zero, a0, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : (x * f a + y * s.gcd f) * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a

Tactic:
add_mul,

Goal state after:
case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : x * f a * ↑u + y * s.gcd f * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
⊢ IsPrincipal S

Tactic:
exact
    ⟨if h : { x : R | x ∈ S ∧ x ≠ 0 }.Nonempty then
        have wf : WellFounded (EuclideanDomain.r : R → R → Prop) := EuclideanDomain.r_wellFounded
        have hmin : WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∈ S ∧
            WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ≠ 0 :=
          WellFounded.min_mem wf { x : R | x ∈ S ∧ x ≠ 0 } h
        ⟨WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h,
          Submodule.ext fun x => ⟨fun hx =>
            div_add_mod x (WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h) ▸
              (Ideal.mem_span_singleton.2 <| dvd_add (dvd_mul_right _ _) <| by
                have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∉
                    { x : R | x ∈ S ∧ x ≠ 0 } :=
                  fun h₁ => WellFounded.not_lt_min wf _ h₁ (mod_lt x hmin.2)
                have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h = 0 := by
                  simp only [not_and_or, Set.mem_ofPred_eq, not_ne_iff] at this
                  exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx
                simp [*]),
              fun hx =>
                let ⟨y, hy⟩ := Ideal.mem_span_singleton.1 hx
                hy.symm ▸ S.mul_mem_right _ hmin.1⟩⟩
      else ⟨0, Submodule.ext fun a => by
            rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]
            exact ⟨fun haS => by_contra fun ha0 => h ⟨a, ⟨haS, ha0⟩⟩,
              fun h₁ => h₁.symm ▸ S.zero_mem⟩⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
⊢ ∀ (a : Associates α), Quotient.map₂ lcm ⋯ 0 a = 0

Tactic:
by rintro ⟨a⟩; exact congr_arg Associates.mk <| lcm_zero_left _

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

Goal state before:
pp: case neg
ι : 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) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
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
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
rcases Set.not_subset.1 this with ⟨r, ⟨⟨⟨hrI, hra⟩, hrb⟩, hr⟩, hri⟩

Goal state after:
case neg
ι : 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) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
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
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ #ι

Tactic:
rintro ⟨s, li⟩

Goal state after:
case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
s : Set M
li : LinearIndepOn R id s
⊢ #↑↑⟨s, li⟩ ≤ #ι
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
i✝ : m
j✝ : l
⊢ (a • M * N) i✝ j✝ = (a • (M * N)) i✝ j✝

Tactic:
apply smul_dotProduct a

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
i✝ : m
j✝ : l
⊢ (M * a • N) i✝ j✝ = (a • (M * N)) i✝ j✝

Tactic:
apply dotProduct_smul

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
⊢ ∑ i, single i i (f i) = diagonal f

Tactic:
ext j k
  rw [sum_apply, diagonal_apply, Finset.sum_eq_single j] <;> simp +contextual [single]

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
i : m
j : n
⊢ single i j 1 = vecMulVec (Pi.single i 1) (Pi.single j 1)

Tactic:
simp [-mul_ite, single, vecMulVec, ite_and, Pi.single_apply, eq_comm]

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst✝¹¹ : DecidableEq m
inst✝¹⁰ : DecidableEq n
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : Module S β
inst✝ : SMulCommClass R S β
f : m → n → α →ₗ[R] β
M : Matrix m n α
⊢ ((liftLinear S) f) M = ∑ i, ∑ j, (f i j) (M i j)

Tactic:
simp [liftLinear, map_sum, LinearEquiv.congrLeft]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ (c * a + i) * b ∈ I ^ n

Tactic:
add_mul,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ c * a * b + i * b ∈ I ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n

Tactic:
by
  rw [Classical.or_iff_not_imp_left]
  intro ha
  obtain ⟨c, i, hi, hc⟩ := exists_inv_pow I ha n
  obtain hb := congr($hc * b)
  rw [one_mul] at hb
  rw [← hb, add_mul, mul_assoc]
  exact add_mem (mul_mem_left _ _ h) (mul_mem_right _ _ hi)

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
x : l → α
y : m → α
M : Matrix m n α
⊢ vecMulVec x y * M = vecMulVec x (y ᵥ* M)

Tactic:
by
  ext
  simp_rw [mul_apply, vecMulVec_apply, vecMul, dotProduct, Finset.mul_sum, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
m : ↑s → ℕ
a b : ↑s → R
ha : ∀ (z : ↑s), a z ∈ I
hb : ∀ (z : ↑s), b z ∈ J
heq : ∀ (z : ↑s), a z + b z = ↑z ^ m z
⊢ ∃ t, Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical

Tactic:
refine ⟨a, by rwa [Set.range_subset_iff], fun z hz ↦ ⟨m ⟨z, hz⟩, heq ⟨z, hz⟩ ▸ ?_⟩⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
m : ↑s → ℕ
a b : ↑s → R
ha : ∀ (z : ↑s), a z ∈ I
hb : ∀ (z : ↑s), b z ∈ J
heq : ∀ (z : ↑s), a z + b z = ↑z ^ m z
z : R
hz : z ∈ s
⊢ a ⟨z, hz⟩ + b ⟨z, hz⟩ ∈ span (Set.range a) ⊔ J
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
x : Matrix n n α
⊢ x ∈ Set.center (Matrix n n α) ↔ x ∈ ⇑(scalar n) '' Set.center α

Tactic:
simp_rw [Set.mem_image, Semigroup.mem_center_iff]

Goal state after:
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
x : Matrix n n α
⊢ (∀ (g : Matrix n n α), g * x = x * g) ↔ ∃ x_1, (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n) x_1 = x
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)

Tactic:
let b := Module.Free.chooseBasis F K
  let c := Module.Free.chooseBasis K A
  rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank,
    ← lift_umax.{w, v}, ← (b.smulTower c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift,
    lift_lift, lift_lift, lift_umax.{v, w}]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
⊢ ∃ f, Injective ⇑f

Tactic:
nontriviality M

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
a✝ : Nontrivial M
⊢ ∃ f, Injective ⇑f