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

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ ↑(Fin.cast ⋯ (Fin.last (p.tail len_pos).length)) + 1 = p.length

Tactic:
exact Nat.succ_pred_eq_of_pos (by simpa [Nat.pos_iff_ne_zero] using len_pos)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ ((p.tail hp).cons p.head ⋯).toList = p.toList

Tactic:
simp [← head_toList]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc a ⋯
⊢ ↑p'.length ≤ n

Tactic:
apply h

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries {(a, b) | a < b} := ⋯
⊢ p'.last = a
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hab
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ (RelSeries.eraseLast p).last < ?b

Tactic:
apply p.step ⟨p.length - 1, by lia⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin (↑lg + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lg) g ⋯
leq : lf = lg
⊢ ⟨⟨lf, f⟩, mf⟩ = ⟨⟨lg, g⟩, mg⟩

Tactic:
subst leq

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
⊢ ⟨⟨lf, f⟩, mf⟩ = ⟨⟨lf, g⟩, mg⟩
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ.refine_2.refine_1
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
⊢ ((t₁.smash t₃ H).toFun ∘ ⇑{ toFun := Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length), inj' := ⋯ })
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    { length := n + 1, toFun := s, step := h }.toFun (Fin.last { length := n + 1, toFun := s, step := h }.length)

Tactic:
convert! h₂

Goal state after:
case e'_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
⊢ ((t₁.smash t₃ H).toFun ∘ ⇑{ toFun := Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length), inj' := ⋯ })
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    t₂ m
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
s : LTSeries α
⊢ s ∈ Finset.map (injStrictMono (Fintype.card α)) Finset.univ

Tactic:
have bl := s.length_lt_card
    obtain ⟨l, f, mf⟩ := s
    simp_rw [Finset.mem_map, Finset.mem_univ, true_and, Subtype.exists]
    use ⟨⟨l, bl⟩, f⟩, Fin.strictMono_iff_lt_succ.mpr mf; rfl

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

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
n : N
hn : IsAddUnit n
m : M
⊢ IsAddUnit (m ⊗ₜ[R] n)

Tactic:
rw [isAddUnit_iff_exists_neg] at hn ⊢
  have ⟨b, eq⟩ := hn
  exact ⟨m ⊗ₜ[R] b, by rw [← tmul_add, eq, tmul_zero]⟩

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

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ s * t → n ∈ x → r • n ∈ s • t • x

Tactic:
by rintro _ _ ⟨_, _, _, _, rfl⟩ _; rw [mul_smul]; aesop

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

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

Tactic:
apply h

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
l : Finset ι
S : ι → Set α
⊢ (fun f ↦ ∏ i ∈ l, f i) '' (↑l).pi S = ∏ i ∈ l, S i

Tactic:
ext
  simp_rw [mem_finsetProd, mem_image, mem_pi, exists_prop, Finset.mem_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b : α
hbc : a ≤ b
c : α
⊢ a + c ≤ b + c

Tactic:
add_eq_sup

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b : α
hbc : a ≤ b
c : α
⊢ a ⊔ c ≤ b ⊔ c
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : c * a ≤ c
⊢ b * a∗ ≤ c

Tactic:
by grw [hb, mul_kstar_le_self ha]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹¹ : IdemSemiring α
inst✝¹⁰ : LE β
inst✝⁹ : LT β
inst✝⁸ : Zero β
inst✝⁷ : One β
inst✝⁶ : Add β
inst✝⁵ : Mul β
inst✝⁴ : Pow β ℕ
inst✝³ : SMul ℕ β
inst✝² : NatCast β
inst✝¹ : Max β
inst✝ : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
⊢ f a + f b = f a ⊔ f b

Tactic:
add_eq_sup

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹¹ : IdemSemiring α
inst✝¹⁰ : LE β
inst✝⁹ : LT β
inst✝⁸ : Zero β
inst✝⁷ : One β
inst✝⁶ : Add β
inst✝⁵ : Mul β
inst✝⁴ : Pow β ℕ
inst✝³ : SMul ℕ β
inst✝² : NatCast β
inst✝¹ : Max β
inst✝ : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
⊢ f a ⊔ f b = f a ⊔ f b
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R S
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
g' : S →ₗ[R] N
⊢ map f g ∘ₗ lTensor M g' = map f (g ∘ₗ g')

Tactic:
simp only [lTensor, ← map_comp, comp_id]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
⊢ -x * y = -(x * y)

Tactic:
refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_) <;>
        simp only [AddSubmonoid.mem_neg, ← neg_mul] at *

Goal state after:
case refine_1
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m n : R
hn : n ∈ y
hm : -m ∈ x
⊢ -m * n ∈ x * y

case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ -m * n ∈ -x * y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
obtain ⟨z, rfl⟩ := h

Goal state after:
R : Type u
inst✝ : CommRing R
y z : R
⊢ IsCoprime (y * z + 1) y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: case refine_1
m n : ℕ
x✝ : IsCoprime m n
a b : ℕ
H : a * m + b * n = 1
⊢ m = 1 ∨ n = 1

Tactic:
simp_rw [Nat.add_eq_one_iff, mul_eq_one, mul_eq_zero] at H

Goal state after:
case refine_1
m n : ℕ
x✝ : IsCoprime m n
a b : ℕ
H : (a = 0 ∨ m = 0) ∧ b = 1 ∧ n = 1 ∨ (a = 1 ∧ m = 1) ∧ (b = 0 ∨ n = 0)
⊢ m = 1 ∨ n = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (x + 1) y

Tactic:
obtain ⟨z, rfl⟩ := h

Goal state after:
R : Type u_1
inst✝ : CommRing R
y z : R
⊢ IsRelPrime (y * z + 1) y
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
M✝¹ : Type u_1
inst✝⁵ : AddCommMonoid M✝¹
inst✝⁴ : Module R M✝¹
inst✝³ : Module A M✝¹
inst✝² : IsScalarTower R A M✝¹
inst✝¹ : IsScalarTower R A A
S T : Set A
M✝ N P Q : Submodule R A
m n : A
ι : Sort uι
inst✝ : IsReduced A
M : Submodule R A
hM : IsNilpotent M
⊢ ∀ x ∈ M, x = 0

Tactic:
rintro m hm

Goal state after:
R : Type u
inst✝⁸ : Semiring R
A : Type v
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
M✝¹ : Type u_1
inst✝⁵ : AddCommMonoid M✝¹
inst✝⁴ : Module R M✝¹
inst✝³ : Module A M✝¹
inst✝² : IsScalarTower R A M✝¹
inst✝¹ : IsScalarTower R A A
S T : Set A
M✝ N P Q : Submodule R A
m✝ n : A
ι : Sort uι
inst✝ : IsReduced A
M : Submodule R A
hM : IsNilpotent M
m : A
hm : m ∈ M
⊢ m = 0
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
P : Submodule R A
x y : A
⊢ (∃ y_1 ∈ P, ((LinearMap.mul R A) y) y_1 = x) ↔ ∃ z ∈ P, y * z = x

Tactic:
LinearMap.mul_apply_apply

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
P : Submodule R A
x y : A
⊢ (∃ y_1 ∈ P, ((LinearMap.mul R A) y_1) y = x) ↔ ∃ z ∈ P, z * y = x

Tactic:
LinearMap.mul_apply_apply

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
s t : SetSemiring A
P : Submodule R A
⊢ span R (SetSemiring.down s) * P ⊔ span R (SetSemiring.down t) * P =
    span R (SetSemiring.down s) * P + span R (SetSemiring.down t) * P

Tactic:
add_eq_sup

Goal state after:
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
I J : Ideal (R × S)
⊢ { toFun := fun I ↦ (map (RingHom.fst R S) I, map (RingHom.snd R S) I), invFun := fun I ↦ I.1.prod I.2, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun I ↦ (map (RingHom.fst R S) I, map (RingHom.snd R S) I), invFun := fun I ↦ I.1.prod I.2,
          left_inv := ⋯, right_inv := ⋯ }
        J ↔
    I ≤ J

Tactic:
by
    simp only [Equiv.coe_fn_mk, Prod.mk_le_mk]
    refine ⟨fun h ↦ ?_, fun h ↦ ⟨map_mono h, map_mono h⟩⟩
    rw [ideal_prod_eq I, ideal_prod_eq J]
    exact inf_le_inf (comap_mono h.1) (comap_mono h.2)

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

Goal state before:
pp: case inl.e_I
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.fst R S) '' s ×ˢ t) = span s

Tactic:
simp [Set.fst_image_prod _ ht]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
α✝ β✝ : Type u_6
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R N
inst✝ : ∀ (i : β✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ x, M✝ (e x))

Tactic:
apply h

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

Goal state before:
pp: R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (map (algebraMap R S) I • N) = I • Submodule.restrictScalars R N

Tactic:
simp_rw [map, Submodule.span_smul_eq, ← Submodule.coe_set_smul,
    Submodule.set_smul_eq_iSup, ← element_smul_restrictScalars, iSup_image]

Goal state after:
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (⨆ b ∈ ↑I, (algebraMap R S) b • N) =
    ⨆ a ∈ ↑I, Submodule.restrictScalars R ((algebraMap R S) a • N)
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]

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'
this : (LinearMap.toSpanSingleton R M x).range ≤ M'
⊢ (LinearMap.toSpanSingleton R M x) 1 ∈ M'
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'
⊢ x ∈ M'

Tactic:
by
  suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by
    rw [← LinearMap.toSpanSingleton_apply_one R M x]
    exact this (LinearMap.mem_range_self _ 1)
  rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le]
  exact fun r hr ↦ H ⟨r, hr⟩

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

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

Tactic:
by
  rw [gcd]
  split_ifs with h <;> simp only [h, zero_mod, gcd_zero_left]

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

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

Tactic:
simpa [h] using gcd_dvd a b

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective ⇑f ↔ ∀ (x : R), x ∈ ⇑f ⁻¹' {0} ↔ x ∈ ↑⊥

Tactic:
exact injective_iff_map_eq_zero' f

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
| Ideal.span {r} • N

Tactic:
rw [← span_eq N, span_smul_span]

Goal state after:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
| span R ({r} • ↑N)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
a : R
ha : x = y * a
⊢ x / y = z ↔ x = y * z

Tactic:
rw [ha, mul_div_cancel_left₀ _ h1]

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
a : R
ha : x = y * a
⊢ a = z ↔ y * a = y * z
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case pos
z : ℤ
hz : normalize z = z
h : 0 ≤ z
⊢ 0 ≤ z

Tactic:
exact h

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

Goal state before:
pp: case neg
α : 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:
· 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.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, IsCoprime I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE

Tactic:
← isCoprime_iff_add,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, IsCoprime I J, IsCoprime I J, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: 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

Tactic:
obtain ⟨h0₂, ⟨b', hb'⟩⟩ := pow_dvd_of_mul_eq_pow hb hab h hc hd₂

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'
h0₂ : d₂ ^ k ≠ 0
b' : α
hb' : b = d₂ ^ k * b'
⊢ Associated (d₁ ^ k) a
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
exact 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
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
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑u, ↑(f x))
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑u, ↑(f x))

Tactic:
exact 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 : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ x ∈ ↑t, ↑(f x)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : f a ≤ f i
⊢ ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)

Tactic:
exact h

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ IsPrincipal I

Tactic:
rw [← map_comap_of_surjective f hf I]

Goal state after:
R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ IsPrincipal (map f (comap f I))
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 : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)

Tactic:
exact h

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

Goal state before:
pp: R : Type u_7
m n : ℕ
A : Matrix (Fin m) (Fin n) R
i : Fin m
j : Fin n
⊢ A ⟨↑(i.mkDivMod j), ⋯⟩.divNat ⟨↑(i.mkDivMod j), ⋯⟩.modNat = A i j

Tactic:
Fin.divNat_mkDivMod,

Goal state after:
R : Type u_7
m n : ℕ
A : Matrix (Fin m) (Fin n) R
i : Fin m
j : Fin n
⊢ A i ⟨↑(i.mkDivMod j), ⋯⟩.modNat = A i j
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
refine ⟨fun ⟨n, le⟩ ↦ ⟨n + 1, n.succ_pos, ?_⟩, fun ⟨n, pos, eq⟩ ↦ ⟨n, ?_⟩⟩

Goal state after:
case refine_1
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
le : ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ Module.rank R (Fin (n + 1) → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin (n + 1) → R)

case refine_2
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq : Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)
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✝ : Zero α
i i' : m
hi : i ≠ i'
j j' : n
a : α
⊢ single i j a i' j' = 0

Tactic:
by simp [hi]

Goal state after: