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

Goal state before:
pp: α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ∀ (i : α), height i + coheight i ≤ ⨆ p, ↑p.length

Tactic:
intro a

Goal state after:
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
⊢ height a + coheight a ≤ ⨆ p, ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
x : α
⊢ coheight x < ⊤

Tactic:
← WithBot.coe_lt_coe

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
x : α
⊢ ↑(coheight x) < ↑⊤
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: case zero
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
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : CommSemiring A
inst✝⁷ : Module A M
inst✝⁶ : Module A N
inst✝⁵ : SMulCommClass R A M
inst✝⁴ : CommSemiring S
inst✝³ : Module S M
inst✝² : SMulCommClass R S M
inst✝¹ : SMulCommClass A S M
inst✝ : CompatibleSMul R A M N
s : S
⊢ (lift
          {
            toFun := fun m ↦
              let __spread.0 := (mk R M N) m;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }).toFun
      (s • 0) =
    (RingHom.id S) s •
      (lift
            {
              toFun := fun m ↦
                let __spread.0 := (mk R M N) m;
                { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ }).toFun
        0

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ sR • N = map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

Tactic:
by
  apply set_smul_eq_of_le
  · intro r n hr hn
    exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩
  · intro x hx
    obtain ⟨c, hc, rfl⟩ := hx
    simp only [LinearMap.coe_comp, coe_subtype, Finsupp.coe_lsum, Finsupp.sum, Function.comp_apply]
    rw [AddSubmonoid.coe_finsetSum]
    refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩
    · rintro r hr
      rw [mem_set_smul_def, Submodule.mem_sInf]
      rintro p hp
      exact hp (hc hr) (c r).2
    · ext x : 1
      simp only [Set.mem_iInter, SetLike.mem_coe]
      fconstructor
      · refine fun h ↦ h fun r n hr hn ↦ ?_
        rw [mem_set_smul_def, mem_sInf]
        exact fun p hp ↦ hp hr hn
      · simp_all

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

Goal state before:
pp: case zero
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
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n
⊢ ∃ m n, 0 = m ⊗ₜ[R] n

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
⊢ map f g ^ 0 = map (f ^ 0) (g ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
⊢ congr f g ^ 0 = congr (f ^ 0) (g ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗

Tactic:
← mul_one a∗

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ * 1 ≤ 1 + a * a∗
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : ℤ
h : IsCoprime a b
⊢ IsCoprime ↑a ↑b

Tactic:
rcases h with ⟨u, v, H⟩
  use u, v
  rw_mod_cast [H]
  exact Int.cast_one

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z

Tactic:
rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]

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
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊥ ^ (n + 1) * ⊥ = ⊥

Tactic:
bot_pow n.succ_ne_zero,

Goal state after:
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊥ * ⊥ = ⊥
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case zero
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
h : 0 ≠ 0
⊢ (M ^ 0).toAddSubmonoid = M.toAddSubmonoid ^ 0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
x : A
hx : x ∈ M ^ 0
⊢ C 0 x hx

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
x : A
hx : x ∈ M ^ 0
⊢ C 0 x hx

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
⊢ ∀ (a : I) (s_1 : Finset I),
    a ∉ s_1 →
      ((↑s_1).Pairwise (IsRelPrime on s) → (∀ i ∈ s_1, s i ∣ z) → ∏ x ∈ s_1, s x ∣ z) →
        (↑(insert a s_1)).Pairwise (IsRelPrime on s) → (∀ i ∈ insert a s_1, s i ∣ z) → ∏ x ∈ insert a s_1, s x ∣ z

Tactic:
intro a

Goal state after:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
⊢ ∀ (s_1 : Finset I),
    a ∉ s_1 →
      ((↑s_1).Pairwise (IsRelPrime on s) → (∀ i ∈ s_1, s i ∣ z) → ∏ x ∈ s_1, s x ∣ z) →
        (↑(insert a s_1)).Pairwise (IsRelPrime on s) → (∀ i ∈ insert a s_1, s i ∣ z) → ∏ x ∈ insert a s_1, s x ∣ z
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case inl.e_J
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ span (⇑(RingHom.snd R S) '' s ×ˢ t) = span t

Tactic:
simp [Set.snd_image_prod hs]

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

Goal state before:
pp: case zero
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
⊢ 0 • n ∈ s • N

Tactic:
| zero =>

Goal state after:
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
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ map (LinearMap.toSpanSingleton R M x) ⊤ ≤ M'

Tactic:
← hs,

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ map (LinearMap.toSpanSingleton R M x) (Ideal.span s) ≤ M'
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ ∀ (x s t s' t' : R), (xgcdAux 0 s t x s' t').1 = gcd 0 x

Tactic:
intros
      rw [xgcd_zero_left, gcd_zero_left]

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

Goal state before:
pp: S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ ↑I
s : R
hsj : s ∈ ↑J
⊢ (fun x1 x2 ↦ x1 * x2) (f r) (f s) ∈ ↑(map f (I * J))

Tactic:
simp_rw [← map_mul]

Goal state after:
S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ ↑I
s : R
hsj : s ∈ ↑J
⊢ f (r * s) ∈ ↑(map f (I * J))
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ comap f K ^ 0 ≤ comap f (K ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
⊢ I ^ 0 ≤ J ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
⊢ span {s} ^ 0 = span {s ^ 0}

Tactic:
| zero =>

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

Goal state before:
pp: 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 ∣ y * z

Tactic:
use 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
⊢ y * z = t * (y * a)
Module: Mathlib.RingTheory.Ideal.Maps

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

Tactic:
intro a

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

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

Tactic:
intro a

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ 0 = ⊤

Tactic:
| zero =>

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ sInf (map f '' A) ≤ map f (sInf A)

Tactic:
· intro y hy
    obtain ⟨x, hx⟩ := hf y
    refine hx ▸ mem_map_of_mem f ?_
    have : ∀ I ∈ A, y ∈ map f I := by simpa using hy
    rw [Submodule.mem_sInf]
    intro J hJ
    rcases (mem_map_iff_of_surjective f hf).1 (this J hJ) with ⟨x', hx', rfl⟩
    have : x - x' ∈ J := by
      apply h J hJ
      rw [RingHom.mem_ker, map_sub, hx, sub_self]
    simpa only [sub_add_cancel] using J.add_mem this hx'

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
⊢ (∀ J ∈ A, RingHom.ker f ≤ J) → map f (sInf A) = sInf (map f '' A)

Tactic:
refine fun h => le_antisymm (le_sInf ?_) ?_
  · intro j hj y hy
    obtain ⟨x, hx⟩ := (mem_map_iff_of_surjective f hf).1 hy
    obtain ⟨J, hJ⟩ := (Set.mem_image _ _ _).mp hj
    rw [← hJ.right, ← hx.right]
    exact mem_map_of_mem f (sInf_le_of_le hJ.left (le_of_eq rfl) hx.left)
  · intro y hy
    obtain ⟨x, hx⟩ := hf y
    refine hx ▸ mem_map_of_mem f ?_
    have : ∀ I ∈ A, y ∈ map f I := by simpa using hy
    rw [Submodule.mem_sInf]
    intro J hJ
    rcases (mem_map_iff_of_surjective f hf).1 (this J hJ) with ⟨x', hx', rfl⟩
    have : x - x' ∈ J := by
      apply h J hJ
      rw [RingHom.mem_ker, map_sub, hx, sub_self]
    simpa only [sub_add_cancel] using J.add_mem this hx'

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ 0 = ⊤

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
hn : 0 ≠ 0
⊢ ↑0 = ⊤

Tactic:
| zero =>

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ ∀ (a : Ideal R) (s : Multiset (Ideal R)), s.prod ≤ s.inf → (a ::ₘ s).prod ≤ (a ::ₘ s).inf

Tactic:
intro a

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
a : Ideal R
⊢ ∀ (s : Multiset (Ideal R)), s.prod ≤ s.inf → (a ::ₘ s).prod ≤ (a ::ₘ s).inf
Module: Mathlib.Algebra.GCDMonoid.Finset

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

Tactic:
intro a

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

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
refine ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], ?_⟩

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ (s.gcd fun x ↦ 1) = 1
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : DivisionMonoid α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
ha : IsUnit a
⊢ (↑a)⁻¹ ∈ S

Tactic:
obtain ⟨u, rfl⟩ := ha

Goal state after:
α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : DivisionMonoid α
inst✝ : SubmonoidClass C α
S : C
u : (↥S)ˣ
⊢ (↑↑u)⁻¹ ∈ S
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg.zero
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a (b ^ 0) ∣ gcd a b ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
⊢ ∃ d, Associated (d ^ k) a

Tactic:
cases subsingleton_or_nontrivial α

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Subsingleton α
⊢ ∃ d, Associated (d ^ k) a

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
⊢ ∃ d, Associated (d ^ k) a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ Associated (gcd x y * gcd x' y') (gcd x y * 1)

Tactic:
convert (gcd_mul_left' (gcd x y) x' y').symm

Goal state after:
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ gcd x y * 1 = gcd (gcd x y * x') (gcd x y * y')
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
⊢ gcd x y = 1 ↔ ¬x ∣ y

Tactic:
← hx.isUnit_gcd_iff,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
⊢ gcd x y = 1 ↔ IsUnit (gcd x y)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
hn : s.card = 0
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
clear hp

Goal state after:
case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hn : s.card = 0
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
hn : s.card = 0
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
| zero =>

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

Goal state before:
pp: case neg
α : 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 : α
a0 : ¬a = 0
this : GCDMonoid α := gcdMonoidOfGCD gcd gcd_dvd_left gcd_dvd_right ⋯
⊢ normalize (Classical.choose ⋯) = 0

Tactic:
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
M : Type v
inst✝¹ : Ring R
inst✝ : IsBezout R
x y : R
⊢ IsPrincipal (Ideal.span {x, y})

Tactic:
by
  classical exact isPrincipal_of_FG (Ideal.span {x, y}) ⟨{x, y}, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
hI : R ∙ p < I
⊢ I = ⊤

Tactic:
rcases principal I with ⟨a, rfl⟩

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : R ∙ p < R ∙ a
⊢ R ∙ a = ⊤
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
hI : R ∙ p < I
⊢ I = ⊤

Tactic:
by
      rcases principal I with ⟨a, rfl⟩
      rw [Ideal.submodule_span_eq, Ideal.span_singleton_eq_top]
      rcases Ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩
      refine (of_irreducible_mul hp).resolve_right (mt (fun hb => ?_) (not_le_of_gt hI))
      rw [Ideal.submodule_span_eq, Ideal.submodule_span_eq,
        Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]

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

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
← Cardinal.lift_le,

Goal state after:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift.{?u.40, v} #↑(range ⇑v) ≤ lift.{?u.40, v} #↑J
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
⊢ diagonal (r • d) = r • diagonal d

Tactic:
by
  ext i j
  by_cases h : i = j <;> simp [h]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
⊢ #α ≤ #β

Tactic:
let b : Basis β R (β →₀ R) := ⟨1⟩
  apply linearIndependent_le_basis b (fun (i : α) ↦ f (Finsupp.single i 1))
  rw [LinearIndependent]
  have : (linearCombination R fun i ↦ f (Finsupp.single i 1)) = f := by ext a b; simp
  exact this.symm ▸ i

Goal state after: