mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ x - (linearCombination R id) ((lmapDomain R R g) l) ∈ f.ker

Tactic:
rw [LinearMap.mem_ker, f.map_sub, ← hl2]

Goal state after:
case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (linearCombination R id) l - f ((linearCombination R id) ((lmapDomain R R g) l)) = 0
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a c : ℕ∞
⊢ a - ⨅ i, f i ≤ c ↔ ⨆ i, a - f i ≤ c

Tactic:
rw [tsub_le_iff_right, add_comm, iInf_add]

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a c : ℕ∞
⊢ a ≤ ⨅ i, f i + c ↔ ⨆ i, a - f i ≤ c
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ R.preimage s = R.image s

Tactic:
rw [← preimage_inv, inv_eq_self]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : ?m.784 := ?m.785
⊢ ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc, (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ) ∈ r

Tactic:
set y := _

Goal state after:
case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : ?m.784 := ?m.785
y : ?m.790 := ?m.791
⊢ ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc, (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ) ∈ r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : ?m.38 := ?m.39
⊢ (i.succ.castSucc.insertNth a p.toFun m.castSucc, i.succ.castSucc.insertNth a p.toFun m.succ) ∈ r

Tactic:
set y := _

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : ?m.38 := ?m.39
y : ?m.44 := ?m.45
⊢ (i.succ.castSucc.insertNth a p.toFun m.castSucc, i.succ.castSucc.insertNth a p.toFun m.succ) ∈ r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ (p.tail len_pos).last = p.last

Tactic:
change p _ = p _

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ p.toFun (Fin.cast ⋯ (Fin.last (p.tail len_pos).length)).succ = p.toFun (Fin.last p.length)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
⊢ ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n

Tactic:
intro p hlast

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
⊢ ↑p.length ≤ n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hbc
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.toFun ⟨p.length - 1, ⋯⟩.succ ≤ x

Tactic:
· convert! hlast
        simp only [Fin.succ_mk, RelSeries.last, Fin.last]
        congr; lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.drop i).head = p.toFun i

Tactic:
simp [drop, head]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height y

Tactic:
intro p hlast

Goal state after:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length + 1 ≤ height y
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
⊢ (RelSeries.last p, y) ∈ {(a, b) | a < b}

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length

Tactic:
intro p hlast

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ↑(RelSeries.eraseLast p).length + 1

Tactic:
by simp [hlen]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
this : ∃ x < a, ↑n ≤ height x
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a

Tactic:
by
      simp_all [minimal_iff_forall_lt]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : 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
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
p₂ : LTSeries α
hhead : RelSeries.head p₂ = a
hlen₂ : p₂.length = m
⊢ RelSeries.last p₁ = RelSeries.head p₂

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : 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
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
p₂ : LTSeries α
hhead : RelSeries.head p₂ = a
hlen₂ : p₂.length = m
⊢ ↑n + ↑m ≤ ↑(RelSeries.smash p₁ p₂ ⋯).length

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
by
  rw [← height_top_eq_krullDim, height, height, WithBot.coe_inj]
  apply le_antisymm
  · apply iSup_le; intro p; apply iSup_le; intro hp
    let q := LTSeries.mk p.length (fun i ↦ (⟨p.toFun i, le_trans (p.monotone (Fin.le_last _)) hp⟩
     : Set.Iic x)) (fun _ _ h ↦ p.strictMono h)
    simp only [le_top, iSup_pos, ge_iff_le]
    exact le_iSup (fun p ↦ (p.length : ℕ∞)) q
  · apply iSup_le; intro p; apply iSup_le; intro _
    have mono : StrictMono (fun (y : Set.Iic x) ↦ y.1) := fun _ _ h ↦ h
    rw [← LTSeries.map_length p (fun x ↦ x.1) mono, ]
    refine le_iSup₂ (f := fun p hp ↦ (p.length : ℕ∞)) (p.map (fun x ↦ x.1) mono) ?_
    exact (p.toFun (Fin.last p.length)).2

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
intro p hlast

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height ↑x

Tactic:
intro p hlast

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

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

Tactic:
intro p hlast

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries α), RelSeries.last p = x → ↑p.length ≤ height ↑x

Tactic:
intro p hlast

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ height ↑x
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = -x + x + (-y + y)

Tactic:
unfold Neg.neg neg

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ { neg := ⇑(Neg.aux R) }.1 (x + y) + (x + y) = { neg := ⇑(Neg.aux R) }.1 x + x + ({ neg := ⇑(Neg.aux R) }.1 y + y)
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
⊢ (TensorProduct.comm R A B) 0 =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      0

Tactic:
simp [*]

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

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x✝ : A
y✝ : B
⊢ (TensorProduct.comm R A B) (x✝ ⊗ₜ[R] y✝) =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      (x✝ ⊗ₜ[R] y✝)

Tactic:
simp [*]

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

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x✝ y✝ : A ⊗[R] B
a✝¹ :
  (TensorProduct.comm R A B) x✝ =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      x✝
a✝ :
  (TensorProduct.comm R A B) y✝ =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      y✝
⊢ (TensorProduct.comm R A B) (x✝ + y✝) =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      (x✝ + y✝)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Fintype.Lattice

Goal state before:
pp: case empty
ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : ι → Finset α
a : α
⊢ a ∈ ∅.inf f ↔ ∀ i ∈ ∅, a ∈ f i

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Fintype.Lattice

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : a ∈ s✝.inf f ↔ ∀ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).inf f ↔ ∀ i ∈ cons a✝¹ s✝ h✝, a ∈ f i

Tactic:
simp [*]

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

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

Tactic:
by
  rw [mul_comm]
  exact h.add_mul_left_left z

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

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : a✝ ∉ s✝
ih : ∏ i ∈ s✝, span R (M i) = span R (∏ i ∈ s✝, M i)
⊢ ∏ i ∈ insert a✝ s✝, span R (M i) = span R (∏ i ∈ insert a✝ s✝, M i)

Tactic:
Finset.prod_insert H,

Goal state after:
case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : a✝ ∉ s✝
ih : ∏ i ∈ s✝, span R (M i) = span R (∏ i ∈ s✝, M i)
⊢ span R (M a✝) * ∏ x ∈ s✝, span R (M x) = span R (∏ i ∈ insert a✝ s✝, M i)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : a✝ ∉ s✝
ih : ∏ i ∈ s✝, span R (M i) = span R (∏ i ∈ s✝, M i)
⊢ span R (M a✝) * ∏ x ∈ s✝, span R (M x) = span R (∏ i ∈ insert a✝ s✝, M i)

Tactic:
Finset.prod_insert H,

Goal state after:
case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : a✝ ∉ s✝
ih : ∏ i ∈ s✝, span R (M i) = span R (∏ i ∈ s✝, M i)
⊢ span R (M a✝) * ∏ x ∈ s✝, span R (M x) = span R (M a✝ * ∏ x ∈ s✝, M x)
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ x ∈ map (RingHom.fst R S) (I.prod J) ↔ x ∈ I

Tactic:
mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1 ∈ I.prod J, (RingHom.fst R S) x_1 = x) ↔ x ∈ I
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x✝ : M
x_in✝ : x✝ ∈ ⇑(algebraMap S R) '' s • N
x : M
r : S
r_in : r ∈ s
x_in : x ∈ N
⊢ (algebraMap S R) r • x ∈ s • restrictScalars S N

Tactic:
rw [algebraMap_smul]

Goal state after:
case refine_1.refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x✝ : M
x_in✝ : x✝ ∈ ⇑(algebraMap S R) '' s • N
x : M
r : S
r_in : r ∈ s
x_in : x ∈ N
⊢ r • x ∈ s • restrictScalars S N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
c : R →₀ ↥N
c_supp : ↑c.support ⊆ ⇑(algebraMap S R) '' s
hc : r • y = ↑(c.sum fun r m ↦ r • m)
u : S
u_in' : u ∈ s
u_in : (algebraMap S R) u ∈ c.support
⊢ (algebraMap S R) u • ↑(c ((algebraMap S R) u)) ∈ s • restrictScalars S N

Tactic:
rw [algebraMap_smul]

Goal state after:
case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
c : R →₀ ↥N
c_supp : ↑c.support ⊆ ⇑(algebraMap S R) '' s
hc : r • y = ↑(c.sum fun r m ↦ r • m)
u : S
u_in' : u ∈ s
u_in : (algebraMap S R) u ∈ c.support
⊢ u • ↑(c ((algebraMap S R) u)) ∈ s • restrictScalars S N
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p

pp: case neg
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p / q ∣ p

Tactic:
· rw [hq, zero_dvd_iff] at hpq
    rw [hpq]
    exact dvd_zero _

Goal state after:
case neg
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p / q ∣ p
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ gcd 0 b ∣ 0 ∧ gcd 0 b ∣ b

Tactic:
rw [gcd_zero_left]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ b ∣ 0 ∧ b ∣ b
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b r r' s t s' t' : R
p : P a b (r, s, t)
p' : P a b (r', s', t')
⊢ P a b (xgcdAux r s t r' s' t')

Tactic:
by
  induction r, r' using GCD.induction generalizing s t s' t' with
  | H0 n => simpa only [xgcd_zero_left]
  | H1 _ _ h IH =>
    rw [xgcdAux_rec h]
    refine IH ?_ p
    unfold P at p p' ⊢
    dsimp
    rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]

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

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝ : EuclideanDomain R
c : R
⊢ (0 * c / 0) ^ 0 = (0 * c) ^ 0 / 0 ^ 0

Tactic:
simp [*]

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

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝ : EuclideanDomain R
n : ℕ
c : R
hn : n ≠ 0
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / 0 ^ n

Tactic:
simp [*]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0

Tactic:
annihilator,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ r ∈ Module.annihilator R ↥N ↔ ∀ n ∈ N, r • n = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.annihilator = ⊤ ↔ N = ⊥

Tactic:
annihilator,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ Module.annihilator R ↥N = ⊤ ↔ N = ⊥
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ (image g ∅).lcm f = ∅.lcm (f ∘ g)

Tactic:
simp [*]

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

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
a✝² : γ
s✝ : Finset γ
a✝¹ : a✝² ∉ s✝
a✝ : (image g s✝).lcm f = s✝.lcm (f ∘ g)
⊢ (image g (insert a✝² s✝)).lcm f = (insert a✝² s✝).lcm (f ∘ g)

Tactic:
simp [*]

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

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ (image g ∅).gcd f = ∅.gcd (f ∘ g)

Tactic:
simp [*]

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

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
a✝² : γ
s✝ : Finset γ
a✝¹ : a✝² ∉ s✝
a✝ : (image g s✝).gcd f = s✝.gcd (f ∘ g)
⊢ (image g (insert a✝² s✝)).gcd f = (insert a✝² s✝).gcd (f ∘ g)

Tactic:
simp [*]

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ (if a * ↑u = 0 then 1 else Exists.choose ⋯) = u⁻¹ * if a = 0 then 1 else Exists.choose ⋯

Tactic:
by
      simp_rw [Units.mul_left_eq_zero, if_neg ha, eq_inv_mul_iff_mul_eq, ← Units.val_inj]
      rw [Units.val_mul, ← (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero ha).eq_iff,
        (assoc a).choose_spec, ← mul_assoc, (assoc _).choose_spec,
        Associates.mk_eq_mk_iff_associated.mpr (associated_mul_unit_right a u u.isUnit)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ gcd 0 0

Tactic:
apply dvd_gcd <;> rfl

Goal state after:
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
this : a * b * ↑(Classical.choose ⋯) = a * ↑(Classical.choose ⋯) * (b * ↑(Classical.choose ⋯))
⊢ ↑(Classical.choose ⋯) = ↑(Classical.choose ⋯) * ↑(Classical.choose ⋯)

Tactic:
apply mul_left_cancel₀ (mul_ne_zero ha hb) _
      simpa only [mul_assoc, mul_comm, mul_left_comm] using this

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

Goal state before:
pp: case neg
α : 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 * Classical.choose ⋯) (a * b)

Tactic:
· rw [← Classical.choose_spec ((gcd_dvd_left a b).trans (Dvd.intro b rfl))]

Goal state after: