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

Goal state before:
pp: case pos
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 : ι), UniqueProds (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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : A' = A
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0

pp: case neg
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 : ι), UniqueProds (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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : ¬A' = A
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0

Tactic:
· rw [hA']
        exact ihB B' (hc.2 bi) hB

Goal state after:
case neg
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 : ι), UniqueProds (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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : ¬A' = A
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
⊢ ∀ (x y : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)), ofIsCompl h (x + y).1 (x + y).2 = ofIsCompl h x.1 x.2 + ofIsCompl h y.1 y.2

Tactic:
intro φ ψ; rw [Prod.snd_add, Prod.fst_add, ofIsCompl_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range

Tactic:
simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff,
    SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length = 0
⊢ {x | x ∈ s}.Subsingleton

Tactic:
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩
  congr!
  exact finCongr (by rw [hs, zero_add]) |>.injective <| Subsingleton.elim (α := Fin 1) _ _

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
hi : ↑i + 1 ≤ p.length
⊢ ↑i.castSucc.rev = ↑⟨p.length - (↑i + 1), ⋯⟩.succ

Tactic:
simp only [Fin.val_rev, Fin.val_castSucc, Fin.val_succ]

Goal state after:
case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ p.length + 1 - (↑i + 1) = p.length - (↑i + 1) + 1
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
q : Submodule R N
m : M
hm : m ∈ ⊥
n : N
x✝ : n ∈ q
⊢ (f m) n ∈ ⊥

Tactic:
by
      rw [Submodule.mem_bot] at hm ⊢
      rw [hm, LinearMap.map_zero₂]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case singleton
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
x : β
a : α
hp : (RelSeries.singleton {(a, b) | a < b} x).head = f a
⊢ ↑(RelSeries.singleton {(a, b) | a < b} x).length ≤ coheight a

Tactic:
| singleton x =>

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 : ℕ
f g : { f // StrictMono f.snd }
e : (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) f = (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) g
⊢ f = g

Tactic:
obtain ⟨⟨lf, f⟩, mf⟩ := f
    obtain ⟨⟨lg, g⟩, mg⟩ := g
    dsimp only at mf mg e
    have leq := congr($(e).length)
    rw [mk_length lf f mf, mk_length lg g mg, Fin.val_eq_val] at leq
    subst leq
    simp_rw [Subtype.mk_eq_mk, Sigma.mk.inj_iff, heq_eq_eq, true_and]
    have feq := fun i ↦ congr($(e).toFun i)
    simp_rw [mk_toFun lf f mf, mk_toFun lf g mg, mk_length lf f mf] at feq
    rwa [funext_iff]

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✝ : Subsingleton N
z : M ⊗[R] N
x : M
y : N
⊢ x ⊗ₜ[R] y = 0

Tactic:
rw [Subsingleton.elim y 0, tmul_zero]

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

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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
n₁ n₂ : N
⊢ (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m, n₁) + FreeAddMonoid.of (m, n₂)) =
    (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m, n₁ + n₂))

Tactic:
simp_rw [map_add, FreeAddMonoid.lift_eval_of, map_add]

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

Goal state before:
pp: R : Type u_1
R' : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : Monoid R'
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : DistribMulAction R' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
m : M
n : N
⊢ 1 • m ⊗ₜ[R] n = m ⊗ₜ[R] n

Tactic:
rw [this, one_smul]

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

Goal state before:
pp: R : Type u_1
R' : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : Monoid R'
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : DistribMulAction R' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R' M
x✝ : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : 1 • x = x
ihy : 1 • y = y
⊢ x + 1 • y = x + y

Tactic:
ihy

Goal state after:
R : Type u_1
R' : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : Monoid R'
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : DistribMulAction R' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R' M
x✝ : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : 1 • x = x
ihy : 1 • y = y
⊢ x + y = x + y
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P₂
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R₂ P₂
g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)
z x y : M ⊗[R] N
ihx : g x = h x
ihy : g y = h y
⊢ h x + g y = h x + h y

Tactic:
ihy

Goal state after:
R : Type u_1
R₂ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P₂
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R₂ P₂
g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)
z x y : M ⊗[R] N
ihx : g x = h x
ihy : g y = h y
⊢ h x + h y = h x + h y
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
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
r s : R'
x✝ x y : M ⊗[R] N
ihx : (r * s) • x = r • s • x
ihy : (r * s) • y = r • s • y
⊢ r • s • x + (r * s) • y = r • s • x + r • s • y

Tactic:
ihy

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
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
r s : R'
x✝ x y : M ⊗[R] N
ihx : (r * s) • x = r • s • x
ihy : (r * s) • y = r • s • y
⊢ r • s • x + r • s • y = r • s • x + r • s • y
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case closed_under_smul
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄,
    r ∈ sR →
      n ∈ N → r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

Tactic:
intro r n hr hn
    exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R₂ M₂
inst✝ : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
g₁ g₂ : N →ₛₗ[σ₁₂] N₂
⊢ map f (g₁ + g₂) = map f g₁ + map f g₂

Tactic:
by
  ext
  simp only [tmul_add, compr₂ₛₗ_apply, mk_apply, map_tmul, add_apply]

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

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✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f✝ : N →ₗ[R] P
r : R
f : N →ₗ[R] P
⊢ rTensor M (r • f) = (RingHom.id R) r • rTensor M f

Tactic:
by
    dsimp
    ext x y
    simp only [compr₂ₛₗ_apply, mk_apply, smul_tmul, tmul_smul, smul_apply, rTensor_tmul]

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

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a ≤ 1
⊢ 1 * a ≤ 1

Tactic:
rwa [one_mul]

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
s : AddSubmonoid R
n : ℕ
⊢ s ^ n = closure (↑s ^ n)

Tactic:
by
  rw [← closure_pow, closure_eq]

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ -a * -x + b * y = 1

Tactic:
neg_mul_neg

Goal state after:
case h
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ a * x + b * y = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
⊢ IsCoprime x |y| ↔ IsCoprime x y

Tactic:
by
  rw [isCoprime_comm, IsCoprime.abs_left_iff, isCoprime_comm]

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

Goal state before:
pp: case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ m * n ∈ comap (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M)

Tactic:
mem_comap,

Goal state after:
case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ ↑(opLinearEquiv R) (m * n) ∈ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ (∀ (y : B), (∃ y_1 ∈ J, h y_1 = y) → ∃ y_1 ∈ I, h y_1 = x * y) → ∃ y, (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ h y = x

Tactic:
rintro hx
    refine ⟨h.symm x, fun z hz => ?_, h.apply_symm_apply x⟩
    obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩
    convert! xz_mem
    apply h.injective
    rw [map_mul, h.apply_symm_apply, hxz]

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
h : I.IsPrime
x y : R × S
⊢ x * y ∈ I.prod ⊤ → x ∈ I.prod ⊤ ∨ y ∈ I.prod ⊤

Tactic:
by simpa using h.mem_or_mem

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 ↥(⨆ i, M✝ i)

Tactic:
← e.iSup_comp

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
inst✝ : ∀ (i : β✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ x, M✝ (e x))
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
inst✝ : RingHomClass F R S
I : Ideal S
x y : R
hx : x ∈ ⇑f ⁻¹' ↑I
hy : y ∈ ⇑f ⁻¹' ↑I
⊢ x + y ∈ ⇑f ⁻¹' ↑I

Tactic:
simp only [Set.mem_preimage, SetLike.mem_coe, map_add f] at hx hy ⊢

Goal state after:
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
inst✝ : RingHomClass F R S
I : Ideal S
x y : R
hx : f x ∈ I
hy : f y ∈ I
⊢ f x + f y ∈ I
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsNoetherian R M
P : Type u_5
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj✝ : Injective ⇑f
p : P
x✝ : ¬p = 0
g : (ℕ →₀ P) →ₗ[R] M
inj : Injective ⇑g
i : ℕ
⊢ g ((Finsupp.lsingle i) p) ≠ 0

Tactic:
by simpa [inj]

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
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ comap f K

Tactic:
mem_comap,

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ f 1 ∉ K
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
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
x : R
hx : x ∈ ↑I
⊢ f x ∈ comap g I

Tactic:
mem_comap,

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
x : R
hx : x ∈ ↑I
⊢ g (f x) ∈ I
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
inst✝ : K.IsTwoSided
a✝ b : R
ha : a✝ ∈ comap f K
⊢ a✝ * b ∈ comap f K

Tactic:
mem_comap,

Goal state after:
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
inst✝ : K.IsTwoSided
a✝ b : R
ha : a✝ ∈ comap f K
⊢ f (a✝ * b) ∈ K
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
⊢ p / q ∣ p

Tactic:
by_cases hq : q = 0
  · rw [hq, zero_dvd_iff] at hpq
    rw [hpq]
    exact dvd_zero _
  use q
  rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]

Goal state after: