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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ ∑ x ∈ f.coeff.support, (f.coeff x • (of S M) x) • v ∈ ↑W

Tactic:
smul_assoc

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ ∑ x ∈ f.coeff.support, f.coeff x • (of S M) x • v ∈ ↑W
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g = t.sup' ⋯ fun y ↦ s.sup' ⋯ fun x ↦ g (f x y)

Tactic:
simp only [image₂, sup'_image, sup'_product_right]; rfl

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
⊢ ∀ (x y : R[M]ᵐᵒᵖ),
    (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun (x * y) =
      (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun x *
        (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun y

Tactic:
simp [coeff_mul, MonoidAlgebra.ext_iff, Finsupp.ext_iff, ← MulOpposite.unop_inj,
      unop_finsuppSum, sum_mapRange_index, apply_ite unop, mapAddEquiv]
    simpa using fun _ _ _ ↦ Finsupp.sum_comm ..

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : One α
s : Finset α
a : α
inst✝³ : DecidableEq β
inst✝² : One β
inst✝¹ : FunLike F α β
inst✝ : OneHomClass F α β
f : F
⊢ image (⇑f) 1 = 1

Tactic:
by rw [image_one, map_one, singleton_one]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
⊢ ↑(s.preimage (fun x ↦ x⁻¹) ⋯) = ↑s⁻¹

Tactic:
by rw [coe_preimage, Set.inv_preimage, coe_inv]

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

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝⁴ : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : IsScalarTower S₁ S₂ R
x✝ : S₁
y✝ : S₂
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := (x✝ • y✝) • toFinsupp✝ } = { toFinsupp := x✝ • y✝ • toFinsupp✝ }

Tactic:
smul_assoc

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n) a)
n : ℕ
a : R
_h : motive (C a * X ^ n)
⊢ motive (C a * X ^ (n + 1))

Tactic:
by rw [C_mul_X_pow_eq_monomial]; exact monomial _ _

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

Goal state before:
pp: 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)
⊢ ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
let _ := isWellFounded_ssubset (α := ∀ i, G i)

Goal state after:
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
⊢ ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this : IsCompl (span R (⇑Finsupp.basisSingleOne '' Set.range u)) (span R (⇑Finsupp.basisSingleOne '' Set.range v))
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))

Tactic:
rwa [← Set.range_comp, ← Set.range_comp, Function.comp_def] at this

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

Goal state before:
pp: 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)
⊢ ∀ {B : Finset ((i : ι) → G i)},
    1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
let _ := isWellFounded_ssubset (α := ∀ i, G i)

Goal state after:
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
⊢ ∀ {B : Finset ((i : ι) → G i)},
    1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
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
h : IsCompl p q
⊢ (↥p × ↥q) ≃ₗ[R] E

Tactic:
by
  apply LinearEquiv.ofBijective (p.subtype.coprod q.subtype)
  constructor
  · rw [← ker_eq_bot, ker_coprod_of_disjoint_range, ker_subtype, ker_subtype, prod_bot]
    rw [range_subtype, range_subtype]
    exact h.1
  · rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top]

Goal state after:
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
p q : Submodule R E
hpq : IsCompl p q
⊢ (p.projection q hpq).ker = q

Tactic:
by
  simp [projection, ker_comp]

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

Goal state before:
pp: 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' (τ₂ (f x₁)) = 1
⊢ f' (τ₁ x₁) = τ₂ (f x₁)

Tactic:
by simp only [comm₁₂]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ
α : 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 i,
    t.toFun ∘ ⇑i = { length := n + 1, toFun := s, step := h }.toFun ∧
      i 0 = 0 ∧ i (Fin.last { length := n + 1, toFun := s, step := h }.length) = Fin.last t.length

Tactic:
obtain ⟨t₂, h₁, m, h₂, ht₂⟩ :=
      exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le (h (.last _)).le

Goal state after:
case succ
α : 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 i,
    t.toFun ∘ ⇑i = { length := n + 1, toFun := s, step := h }.toFun ∧
      i 0 = 0 ∧ i (Fin.last { length := n + 1, toFun := s, step := h }.length) = Fin.last t.length
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
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
⊢ (SMul.aux r) (FreeAddMonoid.of (m, 0)) = (SMul.aux r) 0

Tactic:
by simp_rw [map_zero, SMul.aux_of, tmul_zero]

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:
rw [top_le_iff, ENat.WithBot.eq_top_iff_forall_ge]
    intro n
    simpa using hm (LTSeries.withLength _ n)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length

Tactic:
obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh

Goal state after:
case coe.coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length
Module: Mathlib.Order.KrullDimension

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

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

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p ≤ x
q : LTSeries { x_1 // x_1 ∈ Set.Iic x } := LTSeries.mk p.length (fun i ↦ ⟨p.toFun i, ⋯⟩) ⋯
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length
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 : ∃ b, n + b = 0
m : M
b : N
eq : n + b = 0
⊢ m ⊗ₜ[R] n + m ⊗ₜ[R] b = 0

Tactic:
rw [← tmul_add, eq, tmul_zero]

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
R'₂ : Type u_22
inst✝⁴ : Monoid R'₂
inst✝³ : DistribMulAction R'₂ M
inst✝² : SMulCommClass R R'₂ M
inst✝¹ : SMul R'₂ R'
inst✝ : IsScalarTower R'₂ R' M
s : R'₂
r : R'
x : M ⊗[R] N
m : M
n : N
⊢ ((s • r) • m) ⊗ₜ[R] n = (s • r • m) ⊗ₜ[R] n

Tactic:
smul_assoc

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
R'₂ : Type u_22
inst✝⁴ : Monoid R'₂
inst✝³ : DistribMulAction R'₂ M
inst✝² : SMulCommClass R R'₂ M
inst✝¹ : SMul R'₂ R'
inst✝ : IsScalarTower R'₂ R' M
s : R'₂
r : R'
x : M ⊗[R] N
m : M
n : N
⊢ (s • r • m) ⊗ₜ[R] n = (s • r • m) ⊗ₜ[R] n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length ≤ (↑m + 1) * ↑n' + (↑m + 1) + ↑m
⊢ False

Tactic:
← mul_add_one

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length ≤ (↑m + 1) * (↑n' + 1) + ↑m
⊢ False
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mp
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∃ g_1, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g_1 i_1 ∈ f i_1), g_1 i * ∏ i ∈ is, g_1 i = x * ∏ i ∈ is, g i

Tactic:
refine ⟨Function.update g i x, ?_, ?_⟩

Goal state after:
case insert.mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i is → update g i x i_1 ∈ f i_1

case insert.mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ update g i x i * ∏ i_1 ∈ is, update g i x i_1 = x * ∏ i ∈ is, g i
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
⊢ b * x + 0 * x = 1

Tactic:
rwa [zero_mul, add_zero]

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

Goal state before:
pp: case h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x)

Tactic:
mul_comm z,

Goal state after:
case h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ a * x * z
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp.refine_2.refine_1
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 ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
⊢ (μ a * ∏ i ∈ t \ {b}, s i) * s b + (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) * s a = 1

Tactic:
rw [mul_assoc, ← prod_eq_prod_sdiff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]

Goal state after:
case cons.mp.refine_2.refine_1
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 ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
⊢ ∀ x ∈ t, (μ x * ∏ j ∈ t \ {x}, s j) * s a = μ x * ∏ j ∈ insert a t \ {x}, s j
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
| Set.up {a} • M

Tactic:
rw [← span_eq M]

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
| Set.up {a} • span R ↑M
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case inl
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 (s ×ˢ t) = (span s).prod (span t)

Tactic:
conv_lhs => rw [Ideal.ideal_prod_eq (Ideal.span (s ×ˢ t))]

Goal state after:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ (map (RingHom.fst R S) (span (s ×ˢ t))).prod (map (RingHom.snd R S) (span (s ×ˢ t))) = (span s).prod (span t)
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
intro x y hxy
    have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤ := by
      rw [Prod.mk_mul_mk, mul_one, mem_prod]
      exact ⟨hxy, trivial⟩
    simpa using h.mem_or_mem this

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

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

Tactic:
· exact isPrime_ideal_prod_top'

Goal state after:
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
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
m : M
hm : m ∈ T
r : R
hr : r ∈ Ideal.span S
x✝² x✝¹ : R
x✝ : x✝¹ ∈ span R S
h : x✝¹ • m ∈ span R (S • T)
⊢ (x✝² • x✝¹) • m ∈ span R (S • T)

Tactic:
smul_assoc

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
m : M
hm : m ∈ T
r : R
hr : r ∈ Ideal.span S
x✝² x✝¹ : R
x✝ : x✝¹ ∈ span R S
h : x✝¹ • m ∈ span R (S • T)
⊢ x✝² • x✝¹ • m ∈ span R (S • T)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
⊢ I * K ⊔ J = K ⊔ J

Tactic:
rw [sup_comm] at h

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : J ⊔ I = ⊤
⊢ I * K ⊔ J = K ⊔ J
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : K ⊔ J = ⊤
⊢ I * K ⊔ J = I ⊔ J

Tactic:
rw [sup_comm] at h

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : J ⊔ K = ⊤
⊢ I * K ⊔ J = I ⊔ J
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
⊢ y ∈ map f (sInf A)

Tactic:
obtain ⟨x, hx⟩ := hf y

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
⊢ y ∈ map f (sInf A)
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ normalize z = -z

Tactic:
· rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]

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

Goal state before:
pp: β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f

Tactic:
exact gcd_mul_left

Goal state after: