mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case mp.mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₂ : M₂
y₁ : N₁
hy₁ : f' y₁ = τ₂ x₂
⊢ g' (τ₂ x₂) = 1

Tactic:
obtain ⟨x₁, rfl⟩ := h₁ y₁

Goal state after:
case mp.mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₂ : M₂
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ g' (τ₂ x₂) = 1
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
rw [mul_iInf]

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
mul_iInf' h₀

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

Goal state before:
pp: case mpr.mp
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
hx₂ : g x₂ = 1
y₁ : N₁
hy₁ : f' y₁ = τ₂ x₂
⊢ x₂ ∈ Set.range ⇑f

Tactic:
obtain ⟨x₁, rfl⟩ := h₁ y₁

Goal state after:
case mpr.mp
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
hx₂ : g x₂ = 1
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ x₂ ∈ Set.range ⇑f
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
f : α → β
inst✝ : R.IsSymm
⊢ ∀ (a b : β), (a, b) ∈ Prod.map f f '' R → (b, a) ∈ Prod.map f f '' R

Tactic:
simp only [Set.mem_image, Prod.exists, Prod.map_apply, Prod.mk.injEq, forall_exists_index,
      and_imp]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
f : α → β
inst✝ : R.IsSymm
⊢ ∀ (a b : β) (x x_1 : α), (x, x_1) ∈ R → f x = a → f x_1 = b → ∃ a_4 b_1, (a_4, b_1) ∈ R ∧ f a_4 = b ∧ f b_1 = a
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1.inr
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
h1 : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
⊢ 1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
    ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
      ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
        p1_1 ≠ p2 ∧
          UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
            UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2

Tactic:
by_cases hA : {a ∈ A | a i = p1.1} = A
      · rw [hA]
        exact ihB _ (hc.2 _)
      · exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)

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

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
⊢ g (x - y) = 0

Tactic:
simpa [sub_eq_zero] using e.2

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inl
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
hl : b < b0
⊢ a = a0 ∧ b = b0

Tactic:
exact ((he0 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| le_max' _ _ <| mul_mem_mul ha hb0).elim

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (p.append q connect).toList = p.toList ++ q.toList

Tactic:
by
  apply List.ext_getElem
  · simp; grind
  · simp [List.getElem_append, Fin.append, Fin.addCases]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : 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 : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m < ↑i
⊢ y = p.toFun ⟨↑m, ⋯⟩.succ

Tactic:
change Fin.insertNth _ _ _ _ = _
        rw [Fin.insertNth_apply_below]
        pick_goal 2
        · change m.1 + 1 < i.1 + 1; rwa [add_lt_add_iff_right]
        simp; rfl

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

Goal state before:
pp: case a.mem
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 : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ n ∈ span R t, (f a) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
apply @span_induction R N _ _ _ t

Goal state after:
case a.mem.mem
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 : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ x ∈ t, (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.mem.zero
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 : Set M
t : Set N
a : M
ha : a ∈ s
⊢ (f a) 0 ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.mem.add
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 : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x y : N),
    x ∈ span R t →
      y ∈ span R t →
        (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) →
          (f a) y ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (x + y) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.mem.smul
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 : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R),
    ∀ x ∈ span R t,
      (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (a_1 • x) ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
a : α
h : (a, s.head) ∈ r
i : Fin (s.length + 1)
⊢ (s.cons a h).toFun (Fin.cast ⋯ i.succ) = s.toFun i

Tactic:
simp [cons, Fin.append, Fin.addCases, Fin.subNat]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Tactic:
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

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ height x + 1

Tactic:
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⟩ }

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x ↦
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ ↑p.length ≤ height x + 1
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: case tmul
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴⁹ : CommSemiring R
inst✝⁴⁸ : CommSemiring R₂
inst✝⁴⁷ : CommSemiring R₃
inst✝⁴⁶ : Monoid R'
inst✝⁴⁵ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A✝ : Type u_6
M✝ : Type u_7
N✝ : Type u_8
P : Type u_9
Q : Type u_10
S✝ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁴ : AddCommMonoid M✝
inst✝⁴³ : AddCommMonoid N✝
inst✝⁴² : AddCommMonoid P
inst✝⁴¹ : AddCommMonoid Q
inst✝⁴⁰ : AddCommMonoid S✝
inst✝³⁹ : AddCommMonoid P'
inst✝³⁸ : AddCommMonoid Q'
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N₂
inst✝³⁵ : AddCommMonoid P₂
inst✝³⁴ : AddCommMonoid Q₂
inst✝³³ : AddCommMonoid M₃
inst✝³² : AddCommMonoid N₃
inst✝³¹ : AddCommMonoid P₃
inst✝³⁰ : AddCommMonoid Q₃
inst✝²⁹ : DistribMulAction R' M✝
inst✝²⁸ : Module R'' M✝
inst✝²⁷ : Module R M✝
inst✝²⁶ : Module R N✝
inst✝²⁵ : Module R S✝
inst✝²⁴ : Module R P'
inst✝²³ : Module R Q'
inst✝²² : Module R₂ M₂
inst✝²¹ : Module R₂ N₂
inst✝²⁰ : Module R₂ P₂
inst✝¹⁹ : Module R₂ Q₂
inst✝¹⁸ : Module R₃ M₃
inst✝¹⁷ : Module R₃ N₃
inst✝¹⁶ : Module R₃ P₃
inst✝¹⁵ : Module R₃ Q₃
inst✝¹⁴ : Module R P
inst✝¹³ : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : CommSemiring A
inst✝⁷ : Module A M
inst✝⁶ : Module A N
inst✝⁵ : SMulCommClass R A M
inst✝⁴ : CommSemiring S
inst✝³ : Module S M
inst✝² : SMulCommClass R S M
inst✝¹ : SMulCommClass A S M
inst✝ : CompatibleSMul R A M N
s : S
x : M
y : N
⊢ (lift
          {
            toFun := fun m ↦
              let __spread.0 := (mk R M N) m;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }).toFun
      (s • x ⊗ₜ[A] y) =
    (RingHom.id S) s •
      (lift
            {
              toFun := fun m ↦
                let __spread.0 := (mk R M N) m;
                { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ }).toFun
        (x ⊗ₜ[A] y)

Tactic:
| tmul x y =>

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

Goal state before:
pp: case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ : A
⊢ ∀ (y : A),
    x✝ ∈ closure (↑N ∪ ↑P) →
      y ∈ closure (↑N ∪ ↑P) → m • x✝ ∈ M • N ⊔ M • P → m • y ∈ M • N ⊔ M • P → m • (x✝ + y) ∈ M • N ⊔ M • P

Tactic:
_

Goal state after:
case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
⊢ x✝ ∈ closure (↑N ∪ ↑P) →
    y✝ ∈ closure (↑N ∪ ↑P) → m • x✝ ∈ M • N ⊔ M • P → m • y✝ ∈ M • N ⊔ M • P → m • (x✝ + y✝) ∈ M • N ⊔ M • P
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
⊢ x✝ ∈ closure (↑N ∪ ↑P) →
    y✝ ∈ closure (↑N ∪ ↑P) → m • x✝ ∈ M • N ⊔ M • P → m • y✝ ∈ M • N ⊔ M • P → m • (x✝ + y✝) ∈ M • N ⊔ M • P

Tactic:
_

Goal state after:
case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
⊢ y✝ ∈ closure (↑N ∪ ↑P) → m • x✝ ∈ M • N ⊔ M • P → m • y✝ ∈ M • N ⊔ M • P → m • (x✝ + y✝) ∈ M • N ⊔ M • P
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
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : N ⊗[R] M
⊢ (rTensor M (g ∘ₗ f)) x = (rTensor M g) ((rTensor M f) x)

Tactic:
rw [rTensor_comp, coe_comp]; rfl

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

Goal state before:
pp: case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
⊢ y✝ ∈ closure (↑N ∪ ↑P) → m • x✝ ∈ M • N ⊔ M • P → m • y✝ ∈ M • N ⊔ M • P → m • (x✝ + y✝) ∈ M • N ⊔ M • P

Tactic:
_

Goal state after:
case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
⊢ m • x✝ ∈ M • N ⊔ M • P → m • y✝ ∈ M • N ⊔ M • P → m • (x✝ + y✝) ∈ M • N ⊔ M • P
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ (a * x + b * z) * (c * y + d * z) = 1

Tactic:
by rw [h1, h2, mul_one]

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

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
⊢ S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

Tactic:
use ⟨f y, mem_map.mpr ⟨y.1, y.2, rfl⟩⟩

Goal state after:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
⊢ (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) ⟨f ↑y, ⋯⟩ = S
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
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
x : A
hx : x ∈ M ^ n
⊢ C n x hx

Tactic:
by
  induction n generalizing x with
  | zero =>
    rw [pow_zero] at hx
    obtain ⟨r, rfl⟩ := mem_one.mp hx
    exact algebraMap r
  | succ n n_ih =>
    revert hx
    simp_rw [pow_succ]
    exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

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
M : Submodule R A
n : ℕ
⊢ comap (↑(opLinearEquiv R).symm) (M ^ n) = comap (↑(opLinearEquiv R).symm) M ^ n

Tactic:
comap_unop_pow

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
n : ℕ
⊢ comap (↑(opLinearEquiv R).symm) M ^ n = comap (↑(opLinearEquiv R).symm) M ^ n
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 ι),
    a✝ ∉ s →
      ∏ 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:
_

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 ι
⊢ a✝ ∉ s✝ →
    ∏ 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)
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s' : S
h₁ : (r, s') ∈ I
r' : R
s : S
h₂ : (r', s) ∈ I
⊢ ((RingHom.fst R S) (r, s'), (RingHom.snd R S) (r', s)) ∈ I

Tactic:
simpa using I.add_mem (I.mul_mem_left (1, 0) h₁) (I.mul_mem_left (0, 1) h₂)

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

Goal state before:
pp: case mpr.inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : Ideal R
h : p.IsPrime
⊢ (p.prod ⊤).IsPrime

Tactic:
exact isPrime_ideal_prod_top

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

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ ((∃ p, p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ p, p.IsPrime ∧ I = ⊤.prod p) → I.IsPrime

Tactic:
· rintro (⟨p, ⟨h, rfl⟩⟩ | ⟨p, ⟨h, rfl⟩⟩)
    · exact isPrime_ideal_prod_top
    · exact isPrime_ideal_prod_top'

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
⊢ ∀ {β : Type u_6} (a : α✝ ≃ β),
    (∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : β → Submodule R N} [∀ (i : β), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
_

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
ι : Type u_6
inst✝ : Finite ι
α✝ β✝ : Type u_6
⊢ ∀ (a : α✝ ≃ β✝),
    (∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : β✝ → Submodule R N} [∀ (i : β✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
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} [∀ (i : β✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
_

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
ι : 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
⊢ ∀ [∀ (i : β✝), IsNoetherian R ↥(M✝ i)], IsNoetherian R ↥(⨆ i, M✝ i)