mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: ι : Sort uι
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
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (span R (⋃ i, ↑(s i))) (span R ↑t) = span R (⋃ i, image2 (fun m n ↦ (f m) n) ↑(s i) ↑t)

Tactic:
map₂_span_span,

Goal state after:
ι : Sort uι
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
s : ι → Submodule R M
t : Submodule R N
⊢ span R (image2 (fun m n ↦ (f m) n) (⋃ i, ↑(s i)) ↑t) = span R (⋃ i, image2 (fun m n ↦ (f m) n) ↑(s i) ↑t)
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: ι : Sort uι
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
s : Submodule R M
t : ι → Submodule R N
⊢ map₂ f (span R ↑s) (⨆ i, span R ↑(t i)) = ⨆ i, map₂ f (span R ↑s) (span R ↑(t i))

Tactic:
map₂_span_span,

Goal state after:
ι : Sort uι
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
s : Submodule R M
t : ι → Submodule R N
⊢ map₂ f (span R ↑s) (⨆ i, span R ↑(t i)) = ⨆ i, span R (image2 (fun m n ↦ (f m) n) ↑s ↑(t i))
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: ι : Sort uι
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
s : Submodule R M
t : ι → Submodule R N
⊢ map₂ f (span R ↑s) (span R (⋃ i, ↑(t i))) = span R (⋃ i, image2 (fun m n ↦ (f m) n) ↑s ↑(t i))

Tactic:
map₂_span_span,

Goal state after:
ι : Sort uι
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
s : Submodule R M
t : ι → Submodule R N
⊢ span R (image2 (fun m n ↦ (f m) n) (↑s) (⋃ i, ↑(t i))) = span R (⋃ i, image2 (fun m n ↦ (f m) n) ↑s ↑(t i))
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
m : M
s : Submodule R N
⊢ map₂ f (R ∙ m) (span R ↑s) = map (f m) (span R ↑s)

Tactic:
map₂_span_span,

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
m : M
s : Submodule R N
⊢ span R (image2 (fun m n ↦ (f m) n) {m} ↑s) = map (f m) (span R ↑s)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < x

Tactic:
rw [← hp]
      apply LTSeries.strictMono
      simp [Fin.last]; lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ (∀ (i : LTSeries α), ↑i.length ≤ 0) ↔ ∀ (x b : α), ¬x < b

Tactic:
refine ⟨fun H x y h ↦ (H ⟨1, ![x, y],
    fun i ↦ by obtain rfl := Subsingleton.elim i 0; simpa⟩).not_gt (by simp), ?_⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x b : α), ¬x < b) → ∀ (i : LTSeries α), ↑i.length ≤ 0
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α), RelSeries.head s = ⊥ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₁ : ¬RelSeries.head s = ⊥
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

Tactic:
· obtain ⟨t, i, hi, ht⟩ := this (s.cons ⊥ (bot_lt_iff_ne_bot.mpr h₁)) rfl
    exact ⟨t, ⟨fun j ↦ i (j.succ.cast (by simp)), fun _ _ ↦ by simp⟩,
      funext fun j ↦ (congr_fun hi _).trans (RelSeries.cons_cast_succ _ _ _ _), ht⟩

Goal state after:
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
ih : ∀ (hj : j < p.length + 1), p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, hj⟩ + i
hj : j + 1 < p.length + 1
⊢ p.toFun ⟨i, hi⟩ + (j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + i

Tactic:
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.Order.RelSeries

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

Tactic:
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.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ ↑(height x) = krullDim ↑(Set.Iic x)

Tactic:
← height_top_eq_krullDim,

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ↑(height x) = ↑(height ⊤)
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_7
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_22
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
s : S
m : M
⊢ s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

Tactic:
by
  nth_rw 1 [← mul_one s, ← smul_eq_mul, smul_tmul']

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim (WithTop α) = krullDim α + 1

Tactic:
← height_top_eq_krullDim,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(height ⊤) = krullDim α + 1
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ S ≤ nonZeroDivisorsLeft R ↔ ∀ (s : ↥S), IsLeftRegular ↑s

Tactic:
by
  simp_rw [SetLike.le_def, isLeftRegular_iff_mem_nonZeroDivisorsLeft, Subtype.forall]

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

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

Tactic:
rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x (x * z - y) ↔ IsRelPrime x y

Tactic:
rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h✝ : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
T T' : Finset A
hS : ↑T ⊆ S
hS' : ↑T' ⊆ S'
h : U ⊆ T * T'
⊢ ∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (↑T * ↑T')

Tactic:
use T, T', hS, hS'

Goal state after:
case right
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h✝ : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
T T' : Finset A
hS : ↑T ⊆ S
hS' : ↑T' ⊆ S'
h : U ⊆ T * T'
⊢ x ∈ span R (↑T * ↑T')
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
⊢ (s + t) • P = s • P + t • P

Tactic:
by
    simp_rw [HSMul.hSMul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]

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

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
r : R
x : A
hx : x ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ r • x * y ∈ I

Tactic:
Algebra.smul_mul_assoc

Goal state after:
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
r : R
x : A
hx : x ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ r • (x * y) ∈ I
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'
this : (LinearMap.toSpanSingleton R M x).range ≤ M'
⊢ x ∈ M'

Tactic:
rw [← LinearMap.toSpanSingleton_apply_one R M x]
    exact this (LinearMap.mem_range_self _ 1)

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

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
j : ι
⊢ 1 j = (update 0 i r * x + update 1 i y) j

Tactic:
obtain rfl | ne := eq_or_ne j i

Goal state after:
case inl
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
hxJ : x ∈ J
j : ι
I : Ideal (R j)
h : I.IsMaximal
le : comap (Pi.evalRingHom R j) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R j) I
r y : R j
hy : y ∈ I
eq : r * (Pi.evalRingHom R j) x + y = 1
⊢ 1 j = (update 0 j r * x + update 1 j y) j

case inr
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
j : ι
ne : j ≠ i
⊢ 1 j = (update 0 i r * x + update 1 i y) j
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
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
r' : R
m : M
hm : m ∈ span R T
mem : ∀ r ∈ Ideal.span S, r • m ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ r • r' • m ∈ span R (S • T)

Tactic:
rw [← mul_smul]

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
r' : R
m : M
hm : m ∈ span R T
mem : ∀ r ∈ Ideal.span S, r • m ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ (r * r') • m ∈ span R (S • T)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
⊢ (comap f K).IsMaximal

Tactic:
refine ⟨⟨comap_ne_top _ H.1.1, fun J hJ => ?_⟩⟩
  suffices map f J = ⊤ by
    have := congr_arg (comap f) this
    rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this
    rw [eq_top_iff]
    exact le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))
  refine
    H.1.2 (map f J)
      (lt_of_le_of_ne (le_map_of_comap_le_of_surjective _ hf (le_of_lt hJ)) fun h =>
        ne_of_lt hJ (_root_.trans (congr_arg (comap f) h) ?_))
  rw [comap_map_of_surjective _ hf, sup_eq_left]
  exact le_trans (comap_mono bot_le) (le_of_lt hJ)

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I ^ (n✝ + 1) ≤ J ^ (n✝ + 1)

Tactic:
rw [Submodule.pow_succ, Submodule.pow_succ]

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I ^ n✝ * I ≤ J ^ n✝ * J
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ (I ^ Nat.zero).IsTwoSided

Tactic:
by rw [Submodule.pow_zero, one_eq_top]; infer_instance

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

Goal state before:
pp: case refine_1
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
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ y ∈ j

Tactic:
← hJ.right,

Goal state after:
case refine_1
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
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ y ∈ map f J
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = map (fun x ↦ s.gcd * x) (replicate s.card 1) ∧ (replicate s.card 1).gcd = 1

Tactic:
map_replicate,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ s = replicate s.card (s.gcd * 1) ∧ (replicate s.card 1).gcd = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m : ℕ
⊢ (I + J) ^ (n + m) ≤ I ^ n + J ^ m

Tactic:
add_pow,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m : ℕ
⊢ ∑ m_1 ∈ Finset.range (n + m + 1), I ^ m_1 * J ^ (n + m - m_1) * ↑((n + m).choose m_1) ≤ I ^ n + J ^ m
Module: Mathlib.Algebra.GCDMonoid.Finset

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

Tactic:
classical
    by_cases! h : ∀ x ∈ s, f x = (0 : α)
    · refine ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], ?_⟩
      rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]
    · choose g' hg using @gcd_dvd _ _ _ _ s f
      refine ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ ?_,
          extract_gcd' f _ h fun b hb ↦ ?_⟩
      · simp only [hb, hg, dite_true]
      rw [dif_pos hb, hg hb]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd (m * k) n

Tactic:
by
  grw [← dvd_mul_right]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd m (n * k)

Tactic:
by
  grw [← dvd_mul_right]

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : b * a = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
⊢ Associated (d₁ ^ k) a

Tactic:
rw [(gcd_comm' a b).isUnit_iff] at hab

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h : b * a = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
⊢ Associated (d₁ ^ k) a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : ¬n = 0
⊢ I ≤ P

Tactic:
exact (pow_le_iff hn).mp h

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

Goal state before:
pp: ι : 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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ k ∈ ↑(insert i u), ↑(f k)

Tactic:
rw [Finset.coe_insert] at h ⊢

Goal state after:
ι : 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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ insert i ↑(insert j u), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ k ∈ insert i ↑u, ↑(f k)
Module: Mathlib.LinearAlgebra.Dimension.Subsingleton

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ ⨆ ι, Cardinal.mk ↑↑ι = ⊥

Tactic:
eq_bot_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ ⨆ ι, Cardinal.mk ↑↑ι ≤ ⊥
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 : f a * x * ↑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

Tactic:
mul_comm y

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 : f a * x * ↑u + s.gcd f * y * ↑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: case pos
R : Type u
inst✝ : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
x✝ : IsPrincipal (sSup c)
x : R
hx : sSup c = R ∙ x
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
⊢ False

Tactic:
exact hs hJc ⟨hsSupJ ▸ ⟨x, hx⟩⟩

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
⊢ dite P A B i j = if x : P then A x i j else B x i j

Tactic:
by_cases h : P

Goal state after:
case pos
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : P
⊢ dite P A B i j = if x : P then A x i j else B x i j

case neg
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : ¬P
⊢ dite P A B i j = if x : P then A x i j else B x i j
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
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ #κ ≤ #ι

Tactic:
rw [Cardinal.mk_fintype ι] -- When `ι` is finite, we have `linearIndependent_le_span`,
    have : Nontrivial R := nontrivial_of_invariantBasisNumber R
    rw [Fintype.card_congr (Equiv.ofInjective b b.injective)]
    exact linearIndependent_le_span v i (range b) b.span_eq

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

Goal state before:
pp: case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ ∀ x ∈ Finset.univ ×ˢ Finset.univ, P (single x.1 x.2 (M x.1 x.2))

Tactic:
intros
    apply h_std_basis

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✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
inhabited_h✝ : Inhabited m
inhabited_h : Inhabited n
⊢ P 0

Tactic:
simpa using h_std_basis default default 0

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

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).row i = 0
h' : k ≤ l
⊢ (M ^ l).row i = 0

Tactic:
replace h' : l = k + (l - k) := by lia

Goal state after:
n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).row i = 0
h' : l = k + (l - k)
⊢ (M ^ l).row i = 0
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ (toMultiset (single a n) + toMultiset f).prod = (single a n + f).prod fun a n ↦ a ^ n

Tactic:
Multiset.prod_add,

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ (toMultiset (single a n)).prod * (toMultiset f).prod = (single a n + f).prod fun a n ↦ a ^ n