mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ p.toFun (m.succ.castPred ⋯) = p.toFun ⟨↑m + 1, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case refine_3
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
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ fst R M P ∘ₗ inl R M P = LinearMap.id

Tactic:
rfl

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

Goal state before:
pp: R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f : A →ₛₙₐ[φ] B
h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x
h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y
⊢ { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = f

Tactic:
rfl

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

Goal state before:
pp: R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f : A →ₛₙₐ[φ] B
h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x
h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y
⊢ ↑{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } =
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }

Tactic:
rfl

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

Goal state before:
pp: R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f : A →ₛₙₐ[φ] B
h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x
h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y
⊢ ↑{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = { toFun := ⇑f, map_mul' := h₄ }

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝⁶ : Monoid R
A : Type v
B : Type w
C : Type w₁
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R B
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝⁶ : Monoid R
A : Type v
B : Type w
C : Type w₁
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R B
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
rfl

Goal state after:
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
m : M
n : N
p : Submodule R M
q : Submodule R N
hm : m ∈ p
hn : n ∈ q
⊢ (f ↑⟨m, hm⟩) n = (f m) n

Tactic:
rfl

Goal state after:
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
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun a b ↦ (f.flip b) a) ↑p ↑q) = span R (image2 (fun m n ↦ (f m) n) ↑p ↑q)

Tactic:
rfl

Goal state after:
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
M₂ : Type u_5
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₂ →ₗ[R] N →ₗ[R] P
g : M →ₗ[R] M₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.flip.compl₂ g).flip p q = map₂ (f ∘ₗ g) p q

Tactic:
rfl

Goal state after:
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
M₂ : Type u_5
N₂ : Type u_6
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R M₂
inst✝ : Module R N₂
f : M₂ →ₗ[R] N₂ →ₗ[R] P
g : M →ₗ[R] M₂
h : N →ₗ[R] N₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.compl₂ h ∘ₗ g) p q = map₂ (f.compl₁₂ g h) p q

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : 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
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : x = f a
⊢ f a < p.head

Tactic:
grind

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last = (RelSeries.eraseLast p).last

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.RelSeries

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

Tactic:
simp [RelSeries.smash_castLE]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ 0 < krullDim α ↔ ∃ x y, x < y

Tactic:
contrapose!
  simp_rw [← isMax_iff_forall_not_lt, ← krullDim_nonpos_iff_forall_isMax]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℕ
i j : Fin (p.length + 1)
hij : i ≤ j
⊢ p.toFun i + ↑j ≤ p.toFun j + ↑i

Tactic:
have ⟨i, hi⟩ := i

Goal state after:
p : LTSeries ℕ
i✝ j : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
hij : ⟨i, hi⟩ ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun j + ↑⟨i, hi⟩
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℤ
i j : Fin (p.length + 1)
hij : i ≤ j
⊢ p.toFun i + ↑↑j ≤ p.toFun j + ↑↑i

Tactic:
have ⟨i, hi⟩ := i

Goal state after:
p : LTSeries ℤ
i✝ j : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
hij : ⟨i, hi⟩ ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑↑j ≤ p.toFun j + ↑↑⟨i, hi⟩
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case h
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ (injStrictMono (Fintype.card α)) ⟨⟨⟨l, bl⟩, f⟩, ⋯⟩ = { length := l, toFun := f, step := mf }

Tactic:
rfl

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₃
inst✝¹ : Module R P
inst✝ : Module R Q
f✝ : M →ₗ[R] N →ₗ[R] P
f' f g : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ₛₗ (lift (f + g))) x✝¹) x✝ = (((mk R M N).compr₂ₛₗ (lift f + lift g)) x✝¹) x✝

Tactic:
rfl

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₃
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N →ₗ[R] P
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
x✝³ : R₂
x✝² : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ₛₗ (lift (x✝³ • x✝²))) x✝¹) x✝ = (((mk R M N).compr₂ₛₗ ((RingHom.id R₂) x✝³ • lift x✝²)) x✝¹) x✝

Tactic:
rfl

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

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
x✝¹ : N
x✝ : M
⊢ (((mk R N M).compr₂ₛₗ ↑(TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N)) x✝¹) x✝ =
    (((mk R N M).compr₂ₛₗ ↑(LinearEquiv.refl R (N ⊗[R] M))) x✝¹) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
n : ℕ
x : M ⊗[R] N
⊢ -(↑n.succ • x) = -((↑n + 1) • x)

Tactic:
rfl

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

Goal state before:
pp: case le.refine_2.mp
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
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
h : sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ ∀ p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}, r • n ∈ p

Tactic:
exact fun p hp ↦ hp hr hn

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

Goal state before:
pp: case nil
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
hf : ∀ i ∈ [], f₁ i ⊆ f₂ i
⊢ (List.map f₁ []).prod ⊆ (List.map f₂ []).prod

Tactic:
rfl

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

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

Tactic:
isRegular_iff,

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ ((∀ (s : ↥S), IsLeftRegular ↑s) ∧ ∀ (s : ↥S), IsRightRegular ↑s) ↔ ∀ (s : ↥S), IsLeftRegular ↑s ∧ IsRightRegular ↑s
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
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.map₂ ((mk R M N).compr₂ (map f g)) ⊤ ⊤ = Submodule.map₂ ((mk R P Q).compl₁₂ f g) ⊤ ⊤

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
P : Type u_9
Q : Type u_10
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R M
inst✝¹ : Module R P
inst✝ : Module R Q
f : P →ₗ[R] Q →ₗ[R] M
p : Submodule R P
q : Submodule R Q
⊢ Submodule.map₂ f p q = Submodule.map₂ ((mk R P Q).compr₂ (lift f)) p q

Tactic:
rfl

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N : AddSubmonoid A
m : R
n : A
hm : m ∈ M
hn : n ∈ N
⊢ (DistribSMul.toAddMonoidHom A ↑⟨m, hm⟩) n = m • n

Tactic:
rfl

Goal state after:
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 : M ⊗[R] N
⊢ (⇑(lTensor M g) ∘ ⇑(lTensor M f)) x = (lTensor M g) ((lTensor M f) x)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗

Tactic:
nth_rw 1 [← mul_one a∗]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ * 1 ≤ 1 + a * a∗
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) ∘ ⇑(rTensor M f)) x = (rTensor M g) ((rTensor M f) x)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Semifield R
m n : R
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
obtain rfl | hn := eq_or_ne n 0
  · simp [isCoprime_zero_right]
  suffices IsCoprime m n by simpa [hn]
  refine ⟨0, n⁻¹, ?_⟩
  simp [inv_mul_cancel₀ hn]

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hi.choose ≤ ↑hj.choose
⊢ hi.choose < hj.choose

Tactic:
apply lt_of_le_of_ne h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := ⋯
sli : List α := ⋯
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hi.choose ≤ ↑hj.choose
⊢ ↑hi.choose ≠ ↑hj.choose
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case refine_2
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ ↑⟨j, hj⟩ ∈ t \ {i}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
n : ℕ
H : IsRelPrime x y
⊢ IsRelPrime x (y ^ n)

Tactic:
by
  rw [← Finset.card_range n, ← Finset.prod_const]
  exact IsRelPrime.prod_right fun _ _ ↦ H

Goal state after:
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 = map (LinearMap.mulLeft R a) M

Tactic:
conv_lhs => rw [← span_eq M]
  rw [setSemiring_smul_def, SetSemiring.down_up, span_mul_span, singleton_mul]
  exact (map (LinearMap.mulLeft R a) M).span_eq

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
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ f y ∈ I • ⊤

Tactic:
rw [← mul_one y, ← smul_eq_mul, f.map_smul]

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
⊢ y • f 1 ∈ I • ⊤
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case inr
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
j : ι
ne : j ≠ i
⊢ 1 j = (update 0 i r * x + update 1 i y) j

Tactic:
simp [update_of_ne ne]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : ¬a = 0
⊢ (have x := ⋯;
    gcd (b % a) a) =
    gcd (b % a) a

Tactic:
rfl

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

Goal state before:
pp: case H0
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b n s t s' t' : R
p : P a b (0, s, t)
p' : P a b (n, s', t')
⊢ P a b (xgcdAux 0 s t n s' t')

Tactic:
simpa only [xgcd_zero_left]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (a : M) (b : a ∈ N), ↑(r • ⟨a, b⟩) = ↑0) ↔ ∀ n ∈ N, r • n = 0

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0

Tactic:
by
  simp_rw [annihilator, Module.mem_annihilator, Subtype.forall, Subtype.ext_iff]; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ (∀ ⦃x : R⦄, x ∈ I → ∀ n ∈ N, x • n = 0) ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ ⊥

Tactic:
rfl

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

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

Tactic:
Ideal.map,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
I : Ideal S
N : Submodule R M
this : restrictScalars S (⇑(algebraMap S R) '' ↑I • N) = I • restrictScalars S N
⊢ restrictScalars S (Ideal.span (⇑(algebraMap S R) '' ↑I) • N) = I • restrictScalars S N