mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ (Fin.append p.toFun q.toFun x, Fin.append p.toFun q.toFun y) ∈ r

Tactic:
hx,

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 : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ (Fin.append p.toFun q.toFun (Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩), Fin.append p.toFun q.toFun y) ∈ r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case length_eq
α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last, q.head) ∈ r
hqw : (q.last, w.head) ∈ r
⊢ ((p.append q hpq).append w ⋯).length = (p.append (q.append w hqw) ⋯).length

pp: case toFun_eq
α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last, q.head) ∈ r
hqw : (q.last, w.head) ∈ r
x✝ : Fin (((p.append q hpq).append w ⋯).length + 1)
⊢ ((p.append q hpq).append w ⋯).toFun x✝ = ((p.append (q.append w hqw) ⋯).toFun ∘ Fin.cast ⋯) x✝

Tactic:
· simp only [append_length, Nat.add_left_inj]
    lia

Goal state after:
case toFun_eq
α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last, q.head) ∈ r
hqw : (q.last, w.head) ∈ r
x✝ : Fin (((p.append q hpq).append w ⋯).length + 1)
⊢ ((p.append q hpq).append w ⋯).toFun x✝ = ((p.append (q.append w hqw) ⋯).toFun ∘ Fin.cast ⋯) x✝
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
p : RelSeries r
⊢ motive p

Tactic:
by
  let {n : ℕ} (heq : p.length = n) : motive p := by
    induction n generalizing p with
    | zero =>
      convert! singleton p.head
      ext n
      · exact heq
      simp [show n = 0 by lia, apply_zero]
    | succ d hd =>
      have lq := p.tail_length (heq ▸ d.zero_ne_add_one.symm)
      nth_rw 3 [heq] at lq
      convert!
        cons (p.tail (heq ▸ d.zero_ne_add_one.symm)) p.head (p.3 ⟨0, heq ▸ d.zero_lt_succ⟩)
          (hd _ lq)
      exact (p.cons_self_tail (heq ▸ d.zero_ne_add_one.symm)).symm
  exact this rfl

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : WithBot ℕ∞
hm : ∀ (i : LTSeries α), ↑i.length ≤ m
⊢ m = ⊤

Tactic:
ENat.WithBot.eq_top_iff_forall_ge

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : WithBot ℕ∞
hm : ∀ (i : LTSeries α), ↑i.length ≤ m
⊢ ∀ (m_1 : ℕ), ↑m_1 ≤ m
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 * 1) ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

Tactic:
← smul_eq_mul,

Goal state after:
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 • 1) ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x = height x + 1

Tactic:
apply le_antisymm
  · apply height_le
    intro p hlast
    wlog hlenpos : p.length ≠ 0
    · simp_all
    -- essentially p' := (p.drop 1).map unbot
    let p' : LTSeries α := {
      length := p.length - 1
      toFun := fun ⟨i, hi⟩ => (p ⟨i+1, by lia⟩).unbot (by
        apply ne_bot_of_gt (b := p.head)
        apply p.strictMono
        exact compare_gt_iff_gt.mp rfl)
      step := fun i => by simpa [WithBot.unbot_lt_iff] using! p.step ⟨i + 1, by lia⟩ }
    have hlast' : p'.last = x := by
      simp only [p', RelSeries.last, WithBot.unbot_eq_iff, ← hlast, Fin.last]
      congr
      lia
    suffices p'.length ≤ height p'.last by
      simpa [p', hlast'] using! this
    apply length_le_height_last
  · rw [height_add_const]
    apply iSup₂_le
    intro p hlast
    let p' := (p.map _ WithBot.coe_strictMono).cons ⊥ (by simp)
    apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x = height x

Tactic:
apply le_antisymm
  · apply height_le
    intro p hlast
    -- essentially p' := p.map untop
    let p' : LTSeries α := {
      length := p.length
      toFun := fun i => (p i).untop (by
        apply WithTop.lt_top_iff_ne_top.mp
        apply lt_of_le_of_lt
        · exact p.monotone (Fin.le_last _)
        · rw [RelSeries.last] at hlast
          simp [hlast])
      step := fun i => by simpa [WithTop.untop_lt_iff, WithTop.coe_untop] using p.step i }
    have hlast' : p'.last = x := by
      simp only [p', RelSeries.last, WithTop.untop_eq_iff, ← hlast]
    suffices p'.length ≤ height p'.last by
      rw [hlast'] at this
      simpa [p'] using this
    apply length_le_height_last
  · apply height_le
    intro p hlast
    let p' := p.map _ WithTop.coe_strictMono
    apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : SMulCommClass R R' M
inst✝² : SMulCommClass R R'' M
inst✝¹ : Module R''ᵐᵒᵖ M
inst✝ : IsCentralScalar R'' M
r : R''
x✝ x y : M ⊗[R] N
hx : MulOpposite.op r • x = r • x
hy : MulOpposite.op r • y = r • y
⊢ MulOpposite.op r • x + MulOpposite.op r • y = r • x + r • y

Tactic:
hx,

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : SMulCommClass R R' M
inst✝² : SMulCommClass R R'' M
inst✝¹ : Module R''ᵐᵒᵖ M
inst✝ : IsCentralScalar R'' M
r : R''
x✝ x y : M ⊗[R] N
hx : MulOpposite.op r • x = r • x
hy : MulOpposite.op r • y = r • y
⊢ r • x + MulOpposite.op r • y = r • x + r • y
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
⊢ -x + x + (-y + y) = 0

Tactic:
hx,

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
⊢ 0 + (-y + y) = 0
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
x : A ⊗[R] A
⊢ ∀ (x y : A ⊗[R] A),
    (mul' R A).toFun (a • x) = (RingHom.id A) a • (mul' R A).toFun x →
      (mul' R A).toFun (a • y) = (RingHom.id A) a • (mul' R A).toFun y →
        (mul' R A).toFun (a • (x + y)) = (RingHom.id A) a • (mul' R A).toFun (x + y)

Tactic:
simp +contextual [mul_add]

Goal state after:
Module: Mathlib.Algebra.Ring.NonZeroDivisors

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

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

Goal state after:
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r x y : R
hr : r ∈ R⁰
⊢ r * x ∣ r * y ↔ x ∣ y

Tactic:
dvd_cancel_left_mem_nonZeroDivisors hr

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : IdemSemiring α
n x : ℕ
hmn✝ : 1 ≤ x
hx : ↑x = 1
⊢ ↑x + ↑1 = 1

Tactic:
hx,

Goal state after:
case succ
α : Type u_1
inst✝ : IdemSemiring α
n x : ℕ
hmn✝ : 1 ≤ x
hx : ↑x = 1
⊢ 1 + ↑1 = 1
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : N ≃ₗ[R] N
n : ℕ
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
simpa only [one_pow] using! TensorProduct.congr_pow (1 : M ≃ₗ[R] M) f n

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

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

Tactic:
exact mul_mem_mul hm hn

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

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

Tactic:
exact mul_mem_mul hm hn

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ ↑p ^ 0 ⊆ ↑(p ^ 0)

Tactic:
rw [pow_zero, pow_zero]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ 1 ⊆ ↑1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
H : IsUnit x
b : R
hb : b * x = 1
⊢ 1 * 0 + b * x = 1

Tactic:
by rwa [one_mul, zero_add]

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

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

Tactic:
exact h.of_add_mul_left_right

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

Goal state before:
pp: case cons.mp
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) →
    Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
rintro ⟨μ, hμ⟩

Goal state after:
case cons.mp
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1
⊢ Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ insert a t \ {a}, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
⊢ Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
sdiff_singleton_eq_erase,

Goal state after:
case cons.mp
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ (insert a t).erase a, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
⊢ Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case pos
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : x = Exists.choose h
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j

Tactic:
hx,

Goal state after:
case pos
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : x = Exists.choose h
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) (Exists.choose h) =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) (Exists.choose h) * ∏ j ∈ t \ {Exists.choose h}, s j
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
⊢ (fun i ↦ if i = a then u else v * μ i) a * ∏ j ∈ insert a t \ {a}, s j +
      ∑ x ∈ t, (fun i ↦ if i = a then u else v * μ i) x * ∏ j ∈ insert a t \ {x}, s j =
    1

Tactic:
sdiff_singleton_eq_erase,

Goal state after:
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
⊢ (fun i ↦ if i = a then u else v * μ i) a * ∏ j ∈ (insert a t).erase a, s j +
      ∑ x ∈ t, (fun i ↦ if i = a then u else v * μ i) x * ∏ j ∈ insert a t \ {x}, s j =
    1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: 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
⊢ restrictScalars S (⇑(algebraMap S R) '' s • N) = s • restrictScalars S N

Tactic:
refine le_antisymm (fun x x_in ↦ ?_) (set_smul_le _ _ _ fun r x r_in x_in ↦ ?_)
  · rw [restrictScalars_mem] at x_in
    refine set_smul_inductionOn x x_in ?_ ?_ (fun _ _ _ _ h h' ↦ add_mem h h') (zero_mem _)
    · rintro _ x ⟨r, r_in, rfl⟩ x_in
      rw [algebraMap_smul]
      exact mem_set_smul_of_mem_mem r_in x_in
    · intro r y h h'
      obtain ⟨c, c_supp, hc⟩ := (mem_set_smul ..).mp <| smul_mem _ r h
      simp only [hc, Finsupp.sum, AddSubmonoidClass.coe_finsetSum, SetLike.val_smul]
      refine sum_mem fun u u_in ↦ ?_
      obtain ⟨u, u_in', rfl⟩ := c_supp (Finset.mem_coe.mpr u_in)
      rw [algebraMap_smul]
      exact mem_set_smul_of_mem_mem u_in' (coe_mem (c ((algebraMap S R) u)))
  · rw [restrictScalars_mem, ← algebraMap_smul R r]
    exact mem_set_smul_of_mem_mem (Set.mem_image_of_mem _ r_in) x_in

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
M₁ M₂ : Submodule R N
inst✝¹ : IsNoetherian R ↥M₁
inst✝ : IsNoetherian R ↥M₂
this : IsNoetherian R ↥(M₁.subtype.coprod M₂.subtype).range
⊢ IsNoetherian R ↥(M₁ ⊔ M₂)

Tactic:
LinearMap.range_coprod,

Goal state after:
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
M₁ M₂ : Submodule R N
inst✝¹ : IsNoetherian R ↥M₁
inst✝ : IsNoetherian R ↥M₂
this : IsNoetherian R ↥(M₁.subtype.range ⊔ M₂.subtype.range)
⊢ IsNoetherian R ↥(M₁ ⊔ 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
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ f (y * 1) ∈ I • ⊤

Tactic:
← smul_eq_mul,

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ f (y • 1) ∈ 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:
by
    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: R : Type u
S : Type v
F : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : FunLike F R S
f✝ : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R
inst✝² : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst✝¹ : RingHomSurjective f
I : Ideal R
inst✝ : I.IsTwoSided
a✝ b : S
ha : a✝ ∈ map f I
⊢ a✝ * b ∈ map f I

Tactic:
by
    rw [map_eq_submodule_map] at ha ⊢
    obtain ⟨a, ha, rfl⟩ := ha
    obtain ⟨b, rfl⟩ := f.surjective b
    rw [RingHom.coe_toSemilinearMap, ← map_mul]
    exact ⟨_, I.mul_mem_right _ ha, rfl⟩

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map ((↑f.symm).comp ↑f) I = I

Tactic:
RingEquiv.symm_comp,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map (RingHom.id R) I = I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap ((↑f.symm).comp ↑f) I = I

Tactic:
RingEquiv.symm_comp,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap (RingHom.id R) I = I
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
I : Ideal R
r : R
h : f r ∈ map f I
s : R
hsi : s ∈ ↑I
hfsr : f s = f r
⊢ f (r - s) = 0

Tactic:
rw [map_sub, hfsr, sub_self]

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:
rw [Submodule.pow_zero, Submodule.pow_zero]

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✝ * I ≤ J ^ (n✝ + 1)

Tactic:
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.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case mpr.inl
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hx : x = 0
⊢ lcm x y = 0

Tactic:
hx,

Goal state after:
case mpr.inl
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hx : x = 0
⊢ lcm 0 y = 0
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 x✝¹ : ℕ
x✝ : (I ^ x✝¹).IsTwoSided
⊢ (I ^ x✝¹.succ).IsTwoSided

Tactic:
Submodule.pow_succ

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n x✝¹ : ℕ
x✝ : (I ^ x✝¹).IsTwoSided
⊢ IsTwoSided (I ^ x✝¹ * I)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
i : ι
m : M i
⊢ r • m = 0

Tactic:
simpa using congr_fun (h (Pi.single i m)) i

Goal state after: