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

Goal state before:
pp: case top
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
hh : height a = ⊤
⊢ ⊤ + coheight a ≤ ⨆ p, ↑p.length

Tactic:
| top =>

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.top
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
hch : coheight a = ⊤
⊢ ↑n + ⊤ ≤ ⨆ p, ↑p.length

Tactic:
| top =>

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℤ
i j : Fin (p.length + 1)
hij : i ≤ j
⊢ p.toFun i + ↑↑j ≤ p.toFun j + ↑↑i

Tactic:
by
  -- The proof is identical to `LTSeries.apply_add_index_le_apply_add_index_nat`, but seemed easier
  -- to copy rather than to abstract
  have ⟨i, hi⟩ := i
  have ⟨j, hj⟩ := j
  simp only [Fin.mk_le_mk] at hij
  simp only at *
  induction j, hij using Nat.le_induction with
  | base => simp
  | succ j _hij ih =>
    specialize ih (Nat.lt_of_succ_lt hj)
    have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩ := p.step ⟨j, by lia⟩
    lia

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

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✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N →ₗ[R] P
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
m : M
n : N
⊢ ((LinearMap.toAddMonoidHom'.comp f'.toAddMonoidHom) (r • m)) n =
    ((LinearMap.toAddMonoidHom'.comp f'.toAddMonoidHom) m) (r • n)

Tactic:
by dsimp; rw [LinearMap.map_smulₛₗ₂, map_smulₛₗ]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
⊢ coheight a = ⊤

Tactic:
apply coheight_eq_top_iff.mpr

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
⊢ ∀ (n : ℕ), ∃ p, RelSeries.head p = a ∧ p.length = n
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
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
r s : R'
x : M ⊗[R] N
m : M
n : N
⊢ (r * s) • m ⊗ₜ[R] n = r • s • m ⊗ₜ[R] n

Tactic:
simp_rw [this, mul_smul]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
⊢ height ⊤ = ⊤

Tactic:
| top =>

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
| top =>

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

Goal state before:
pp: case insert.mp.refine_1
ι : 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
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i is → update g i x i_1 ∈ f i_1

pp: case insert.mp.refine_2
ι : 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
⊢ update g i x i * ∏ i_1 ∈ is, update g i x i_1 = x * ∏ i ∈ is, g i

Tactic:
· intro j hj
        obtain rfl | hj := Finset.mem_insert.mp hj
        · rwa [Function.update_self]
        · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
          exact hg hj

Goal state after:
case insert.mp.refine_2
ι : 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
⊢ update g i x i * ∏ i_1 ∈ is, update g i x i_1 = x * ∏ i ∈ is, g i
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
⊢ (fun n ↦ r ^ n) n = (fun n ↦ r ^ n) m → n = m

Tactic:
hnm

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : (fun n ↦ r ^ n) n = (fun n ↦ r ^ n) m
⊢ n = m
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 : AddSubmonoid A
C : A → Prop
a : A
ha : a ∈ M • N
hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)
hadd : ∀ (x y : A), C x → C y → C (x + y)
⊢ 0 ∈ { carrier := ofPred C, add_mem' := ⋯ }.carrier

Tactic:
simpa only [smul_zero] using! hm _ (zero_mem _) _ (zero_mem _)

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
f : N →ₗ[R] N
n : ℕ
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
by
  have h := TensorProduct.map_pow (id : M →ₗ[R] M) f n
  rwa [Module.End.id_pow] at h

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ↑(p ^ (n + 1) * p) = ↑p ^ (n + 1) * ↑p

Tactic:
coe_mul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ↑(p ^ (n + 1)) * ↑p = ↑p ^ (n + 1) * ↑p
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
s : Set R
n : ℕ
⊢ closure s ^ n * closure s = closure (s ^ n * s)

Tactic:
closure_pow s n,

Goal state after:
R : Type u_2
inst✝ : Semiring R
s : Set R
n : ℕ
⊢ closure (s ^ n) * closure s = closure (s ^ n * s)
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ False

Tactic:
obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
ha : a ^ 2 = 0
hb : b ^ 2 = 0
⊢ False
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ comap (↑(opLinearEquiv R).symm) (M * N) = comap (↑(opLinearEquiv R).symm) N * comap (↑(opLinearEquiv R).symm) M

Tactic:
simp_rw [← map_equiv_eq_comap_symm, map_op_mul]

Goal state after:
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
hK : K.IsPrime
x y : R
⊢ x * y ∈ Ideal.comap f K → x ∈ Ideal.comap f K ∨ y ∈ Ideal.comap f K

Tactic:
simp only [mem_comap, map_mul]; apply hK.2

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
⊢ x * g * s * p = x * s * p * g

Tactic:
simp only [mul_right_comm]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (s.erase a)) =
    GCDMonoid.lcm (GCDMonoid.lcm a a) (fold GCDMonoid.lcm 1 (s.erase a))

Tactic:
lcm_same

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (s.erase a)) = GCDMonoid.lcm (normalize a) (fold GCDMonoid.lcm 1 (s.erase a))
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case refine_2
n : ℕ
⊢ (↑n).natAbs = n

Tactic:
Int.natAbs_natCast

Goal state after:
case refine_2
n : ℕ
⊢ n = n
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : f x' = x
y : A
hy : y ∈ RingHom.ker f
z : A
hz : z ∈ J
hyz : y + z = x'
⊢ ∃ y ∈ J, f y = x

Tactic:
use z, hz

Goal state after:
case right
A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : f x' = x
y : A
hy : y ∈ RingHom.ker f
z : A
hz : z ∈ J
hyz : y + z = x'
⊢ f z = x
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
⊢ normUnit (a * ↑(normUnit a)) = 1

Tactic:
obtain rfl | h := eq_or_ne a 0

Goal state after:
case inl
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a✝ : Nontrivial α
⊢ normUnit (0 * ↑(normUnit 0)) = 1

case inr
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
h : a ≠ 0
⊢ normUnit (a * ↑(normUnit a)) = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ (s.inf f).radical = (f i).radical

Tactic:
← radicalInfTopHom_apply,

Goal state after:
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ radicalInfTopHom (s.inf f) = (f i).radical
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (I * J).radical = I.radical ⊓ J.radical

Tactic:
refine le_antisymm ?_ fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ =>
    ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩
  have := radical_mono <| mul_le_inf (I := I) (J := J)
  simp_rw [radical_inf I J] at this
  assumption

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

Goal state before:
pp: case succ
ι : 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
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
hn : ∃ i t, i ∉ t ∧ insert i t = s ∧ t.card = n
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
rcases hn with ⟨i, t, hit, rfl, hn⟩

Goal state after:
case succ
ι : 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
hp : ∀ i_1 ∈ insert i t, (f i_1).IsPrime
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : 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 : α
⊢ (if a = 0 then 0 else normalize (Classical.choose ⋯)) = 0

Tactic:
by
      split_ifs with a0
      · rfl
      let := gcdMonoidOfGCD gcd gcd_dvd_left gcd_dvd_right dvd_gcd
      simpa [gcd_ne_zero_of_left a0] using show GCDMonoid.gcd .. * _ = _
        from (Classical.choose_spec ((gcd_dvd_left a 0).trans (.intro 0 rfl))).symm

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ Ideal.span {x, y}

Tactic:
by rw [← span_gcd]; apply Ideal.subset_span; simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : ¬a = 0
h_1 : b = 0
⊢ Associated (a * lcm a b) (a * b)

Tactic:
rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _)]

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

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

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

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

Goal state before:
pp: 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
⊢ ?m.29 ≤ ⨆ ι, #↑↑ι

Tactic:
apply le_ciSup Cardinal.bddAbove_of_small

Goal state after:
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 // LinearIndepOn R id s }
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ v ⬝ᵥ Pi.single i 1 = v i

Tactic:
dotProduct_single,

Goal state after:
n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ v i * 1 = v i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
A : Matrix o n α := M.submatrix (⇑e₂.symm) id
⊢ submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id

Tactic:
have : M = A.submatrix e₂ id := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]

Goal state after:
case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
val✝ : Fintype o
A : Matrix o n α := M.submatrix (⇑e₂.symm) id
this : M = A.submatrix (⇑e₂) id
⊢ submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = count x (s.card • {a})

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.card ≠ 0 ∧ s = s.card • {a}
⊢ s.toFinset = {a}

Tactic:
· rw [count_nsmul, count_singleton]
    by_cases hx : x = a
    · simp_rw [hx, ite_true, mul_one, count_eq_card]
      intro y hy
      rw [← mem_toFinset, H, Finset.mem_singleton] at hy
      exact hy.symm
    have hx' : x ∉ s := fun h' ↦ hx <| by rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
    simp_rw [count_eq_zero_of_notMem hx', hx, ite_false, Nat.mul_zero]

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.card ≠ 0 ∧ s = s.card • {a}
⊢ s.toFinset = {a}
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) ≤ max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
calc
      #(α →₀ β) ≤ #(Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
      _ = #(α × β) := mk_finset_of_infinite _
      _ = max (lift.{v} #α) (lift.{u} #β) := by
        rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
have : ℵ₀ ≤ (#β).lift := aleph0_le_lift.2 (aleph0_le_mk β)

Goal state after:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{?u.31, v} #β
⊢ lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Set.range ⇑(algebraMap R A) ∪ (↑S ∪ ↑T) = ↑S ∪ ↑T

Tactic:
Set.union_eq_right

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Set.range ⇑(algebraMap R A) ⊆ ↑S ∪ ↑T
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ Set.range ⇑(algebraMap R A) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)

Tactic:
Set.union_eq_right

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ Set.range ⇑(algebraMap R A) ⊆ ⋃₀ (SetLike.coe '' S)
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
i : ι
x : ↥(A i)
⊢ ((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) i = x

Tactic:
rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_same]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case mul
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : f y ∈ adjoin R (⇑f '' (s ∪ {1}))
hz : f z ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f (y * z) ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
| mul y z _ _ hy hz =>

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case mul
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : Commute a y
hz : Commute a z
⊢ Commute a (y * z)

Tactic:
| mul y z _ _ hy hz =>

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

Goal state before:
pp: case pos
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
i j : ι₁
n : M₁ j
hj : j = i
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n

Tactic:
subst hj

Goal state after:
case pos
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
j : ι₁
n : M₁ j
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') j ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ j) M₂').flip n✝ ∘ₗ component S ι₁ M₁ j) ∘ₗ lof S ι₁ M₁ j) n