mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
⊢ ∃ p, RelSeries.head p = a ∧ p.length = n

Tactic:
obtain ⟨p, hp, hl⟩ := exists_series_of_le_height (α := αᵒᵈ) a h

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
p : LTSeries αᵒᵈ
hp : RelSeries.last p = a
hl : p.length = n
⊢ ∃ p, RelSeries.head p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2.mp
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.head p = x ∧ p.length = n) → ∃ p, RelSeries.last p = x ∧ p.length = n

pp: case e'_2.mpr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.last p = x ∧ p.length = n) → ∃ p, RelSeries.head p = x ∧ p.length = n

Tactic:
<;>

Goal state after:
case e'_2.mp
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.head p = x ∧ p.length = n) → ∃ p, RelSeries.last p = x ∧ p.length = n

case e'_2.mpr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.last p = x ∧ p.length = n) → ∃ p, RelSeries.head p = x ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ (RelSeries.reverse p).last = x

pp: case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ (RelSeries.reverse p).length = n

Tactic:
<;>

Goal state after:
case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ (RelSeries.reverse p).last = x

case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ (RelSeries.reverse p).length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).head = x

pp: case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).length = n

Tactic:
<;>

Goal state after:
case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).head = x

case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x = 0 ↔ IsMin x

Tactic:
by
  simpa [isMin_iff_forall_not_lt] using height_le_coe_iff (x := x) (n := 0)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2.top
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝ : y < x
⊢ ⊤ ≤ ↑n ↔ ⊤ < ↑n + 1

pp: case e'_2.coe
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ ≤ ↑n ↔ ↑a✝ < ↑n + 1

Tactic:
<;>

Goal state after:
case e'_2.top
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝ : y < x
⊢ ⊤ ≤ ↑n ↔ ⊤ < ↑n + 1

case e'_2.coe
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ ≤ ↑n ↔ ↑a✝ < ↑n + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = 2
⊢ 0 < 1

pp: case refine_1.refine_2
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = 2
⊢ 1 < Fin.last p.length

Tactic:
<;>

Goal state after:
case refine_1.refine_1
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = 2
⊢ 0 < 1

case refine_1.refine_2
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = 2
⊢ 1 < Fin.last p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMin x

Tactic:
simp only [krullDim_nonpos_iff_forall_isMax, IsMax, IsMin]

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x : α) ⦃b : α⦄, x ≤ b → b ≤ x) ↔ ∀ (x : α) ⦃b : α⦄, b ≤ x → x ≤ b
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case «0»
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ (![y, x, z] ((fun i ↦ i) ⟨0, ⋯⟩).castSucc, ![y, x, z] ((fun i ↦ i) ⟨0, ⋯⟩).succ) ∈ {(a, b) | a < b}

pp: case «1»
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ (![y, x, z] ((fun i ↦ i) ⟨1, ⋯⟩).castSucc, ![y, x, z] ((fun i ↦ i) ⟨1, ⋯⟩).succ) ∈ {(a, b) | a < b}

Tactic:
<;>

Goal state after:
case «0»
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ (![y, x, z] ((fun i ↦ i) ⟨0, ⋯⟩).castSucc, ![y, x, z] ((fun i ↦ i) ⟨0, ⋯⟩).succ) ∈ {(a, b) | a < b}

case «1»
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ (![y, x, z] ((fun i ↦ i) ⟨1, ⋯⟩).castSucc, ![y, x, z] ((fun i ↦ i) ⟨1, ⋯⟩).succ) ∈ {(a, b) | a < b}
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₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
x p q : M ⊗[R] N
ih1 : (liftAux f') (r • p) = σ₁₂ r • (liftAux f') p
ih2 : (liftAux f') (r • q) = σ₁₂ r • (liftAux f') q
⊢ (liftAux f') (r • (p + q)) = σ₁₂ r • (liftAux f') (p + q)

Tactic:
simp_rw [smul_add, (liftAux f').map_add, ih1, ih2, smul_add]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
x : α
⊢ ↑(coheight x) = krullDim ↑(Set.Ici x)

Tactic:
by
  rw [coheight, ← krullDim_orderDual, Order.krullDim_eq_of_orderIso (OrderIso.refl _)]
  exact height_eq_krullDim_Iic _

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}

Tactic:
by_cases hzero : i = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : i = 0
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}
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_9
Q : Type u_10
P₂ : Type u_17
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid P₂
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R₂ P₂
inst✝¹ : Module R P
inst✝ : Module R Q
g h : M ⊗[R] N ⊗[R] P ⊗[R] Q →ₛₗ[σ₁₂] P₂
H : ∀ (w : M) (x : N) (y : P) (z : Q), g (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) = h (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)
⊢ g = h

Tactic:
ext w x y z

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_9
Q : Type u_10
P₂ : Type u_17
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid P₂
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R₂ P₂
inst✝¹ : Module R P
inst✝ : Module R Q
g h : M ⊗[R] N ⊗[R] P ⊗[R] Q →ₛₗ[σ₁₂] P₂
H : ∀ (w : M) (x : N) (y : P) (z : Q), g (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) = h (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)
w : M
x : N
y : P
z : Q
⊢ (((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ ((mk R (M ⊗[R] N ⊗[R] P) Q).compr₂ₛₗ g))) w) x) y) z =
    (((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ ((mk R (M ⊗[R] N ⊗[R] P) Q).compr₂ₛₗ h))) w) x) y) z
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n : ℕ
⊢ mulLeft R a ^ 0 = mulLeft R (a ^ 0)

Tactic:
rw [pow_zero, pow_zero, mulLeft_one, Module.End.one_eq_id]

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

Goal state before:
pp: case pos
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₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : P
⊢ x₁ ⊗ₜ[R] x₂ = x₁ ⊗ₜ[R] x₂

pp: case neg
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₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : ¬P
⊢ 0 ⊗ₜ[R] x₂ = 0

Tactic:
<;>

Goal state after:
case pos
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₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : P
⊢ x₁ ⊗ₜ[R] x₂ = x₁ ⊗ₜ[R] x₂

case neg
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₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : ¬P
⊢ 0 ⊗ₜ[R] x₂ = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case pos
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₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : P
⊢ x₁ ⊗ₜ[R] x₂ = x₁ ⊗ₜ[R] x₂

pp: case neg
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₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : ¬P
⊢ x₁ ⊗ₜ[R] 0 = 0

Tactic:
<;>

Goal state after:
case pos
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₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : P
⊢ x₁ ⊗ₜ[R] x₂ = x₁ ⊗ₜ[R] x₂

case neg
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₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : ¬P
⊢ x₁ ⊗ₜ[R] 0 = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : i = j
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j

pp: case neg
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : ¬i = j
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : i = j
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j

case neg
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : ¬i = j
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : i = j
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j

pp: case neg
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : ¬i = j
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : i = j
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j

case neg
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : ¬i = j
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j
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
⊢ (map f g).range = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Tactic:
simp only [← Submodule.map_top, ← span_tmul_eq_top, Submodule.map_span]

Goal state after:
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.span R (⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t}) = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: case zero
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
⊢ congr f g ^ 0 = congr (f ^ 0) (g ^ 0)

Tactic:
exact congr_refl_refl.symm

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

Goal state before:
pp: case refine_1
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ -x
n : R
hn : n ∈ y
⊢ m * n ∈ -(x * y)

pp: case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * n ∈ -(-x * y)

Tactic:
<;>

Goal state after:
case refine_1
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ -x
n : R
hn : n ∈ y
⊢ m * n ∈ -(x * y)

case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * n ∈ -(-x * y)
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case refine_1
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ -y
⊢ m * n ∈ -(x * y)

pp: case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * n ∈ -(x * -y)

Tactic:
<;>

Goal state after:
case refine_1
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ -y
⊢ m * n ∈ -(x * y)

case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * n ∈ -(x * -y)
Module: Mathlib.Data.Fintype.Lattice

Goal state before:
pp: case empty
ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : ι → Finset α
a : α
⊢ a ∈ ∅.inf f ↔ ∀ i ∈ ∅, a ∈ f i

pp: case cons
ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : a ∈ s✝.inf f ↔ ∀ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).inf f ↔ ∀ i ∈ cons a✝¹ s✝ h✝, a ∈ f i

Tactic:
<;>

Goal state after:
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : ι → Finset α
a : α
⊢ a ∈ ∅.inf f ↔ ∀ i ∈ ∅, a ∈ f i

case cons
ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : a ∈ s✝.inf f ↔ ∀ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).inf f ↔ ∀ i ∈ cons a✝¹ s✝ h✝, a ∈ f i
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
use -a, b

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_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
⊢ a ^ 2 + b ^ 2 ≠ 0

Tactic:
by
  intro h'
  obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'
  obtain rfl := eq_zero_of_pow_eq_zero ha
  obtain rfl := eq_zero_of_pow_eq_zero hb
  exact not_isCoprime_zero_zero h

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'
⊢ (S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) →
    S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

pp: case mpr
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'
⊢ (S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) →
    S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)

Tactic:
<;>

Goal state after:
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'
⊢ (S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) →
    S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

case mpr
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'
⊢ (S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) →
    S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case succ
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) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
hx : x ∈ M ^ (n + 1)
⊢ C (n + 1) x hx

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (y ^ n)

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

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

Goal state before:
pp: case succ
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 : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
hx : x ∈ M ^ (n + 1)
⊢ C (n + 1) x hx

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x

Tactic:
exact H.1.mul_left (ih H.2)

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

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

Tactic:
rw [ideal_prod_eq I]

Goal state after:
case mp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ ((map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)).IsPrime →
    (∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) = p.prod ⊤) ∨
      ∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) = ⊤.prod p
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
a b : K
h : b = 0
⊢ b * (a / b) + (a - a * b / b) = a

pp: case neg
K : Type u_1
inst✝ : Field K
a b : K
h : ¬b = 0
⊢ b * (a / b) + (a - a * b / b) = a

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
a b : K
h : b = 0
⊢ b * (a / b) + (a - a * b / b) = a

case neg
K : Type u_1
inst✝ : Field K
a b : K
h : ¬b = 0
⊢ b * (a / b) + (a - a * b / b) = a
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
a b : K
h✝ : a = 0
⊢ b = b

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
a b : K
h✝ : ¬a = 0
⊢ (have x := ⋯;
    EuclideanDomain.gcd (b % a) a) =
    a

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
a b : K
h✝ : a = 0
⊢ b = b

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
a b : K
h✝ : ¬a = 0
⊢ (have x := ⋯;
    EuclideanDomain.gcd (b % a) a) =
    a
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
h : a = 0
⊢ 0 = a

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

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
h : a = 0
⊢ 0 = a

case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
h : ¬a = 0
⊢ (have x := ⋯;
    gcd (0 % a) a) =
    a
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ (∃ x ∈ I, e x = y) → y ∈ map e I

Tactic:
· rintro ⟨x, hx, rfl⟩
    exact mem_map_of_mem e hx

Goal state after: