mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ (Finsupp.linearCombination R v).range = ⊤

Tactic:
Finsupp.range_linearCombination

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ span R (range v) = ⊤
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h✝ : (f.sum fun _i xi ↦ xi) ≠ 0
j : ι
hj : j ∈ insert i f.support
h : j = i
⊢ (-f.sum fun x x_1 ↦ x_1) ∈ p j

Tactic:
exact (p j).neg_mem (h ▸ hx)

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

Goal state before:
pp: X : Type u_1
⊢ support 0 = ∅

Tactic:
by
  simp only [support, Finsupp.support_zero, map_zero]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ.mulShift u = 1 ↔ ψ = 1

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · ext1 y
    rw [show y = u * (hu.unit⁻¹ * y) by rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]]
    simpa only [mulShift_apply] using! DFunLike.ext_iff.mp h (hu.unit⁻¹ * y)
  · solve_by_elim

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case pos
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∈ s
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s)

Tactic:
simp [insert_eq_of_mem has, has]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
⊢ (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2

Tactic:
let F (p : M × M) : R := if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0

Goal state after:
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (∑ x ∈ f.coeff.support ×ˢ g.coeff.support, if x.1 * x.2 = a0 * b0 then f.coeff x.1 * g.coeff x.2 else 0) =
    f.coeff a0 * g.coeff b0

Tactic:
refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl) <;> simp_rw [Finset.mem_product]

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ∀ (b : A × A),
    b.1 ∈ f.coeff.support ∧ b.2 ∈ g.coeff.support →
      b ≠ (a0, b0) → (if b.1 * b.2 = a0 * b0 then f.coeff b.1 * g.coeff b.2 else 0) = 0

case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support) → (if True then f.coeff a0 * g.coeff b0 else 0) = 0
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
⊢ a • 0 = 0

Tactic:
smul_def,

Goal state after:
R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
⊢ ↑a * 0 = 0
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ a • (x + y) = a • x + a • y

Tactic:
smul_def,

Goal state after:
R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ ↑a * (x + y) = a • x + a • y
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ ↑a * (x + y) = a • x + a • y

Tactic:
smul_def,

Goal state after:
R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ ↑a * (x + y) = ↑a * x + a • y
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ ↑a * (x + y) = ↑a * x + a • y

Tactic:
smul_def,

Goal state after:
R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ ↑a * (x + y) = ↑a * x + ↑a * y
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
⊢ a • 0 = 0

Tactic:
smul_def,

Goal state after:
R : Type u_1
inst✝ : DivisionRing R
a : ℚ
⊢ ↑a * 0 = 0
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ a • (x + y) = a • x + a • y

Tactic:
smul_def,

Goal state after:
R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ ↑a * (x + y) = a • x + a • y
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ ↑a * (x + y) = a • x + a • y

Tactic:
smul_def,

Goal state after:
R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ ↑a * (x + y) = ↑a * x + a • y
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ ↑a * (x + y) = ↑a * x + a • y

Tactic:
smul_def,

Goal state after:
R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ ↑a * (x + y) = ↑a * x + ↑a * y
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty

Tactic:
exact hs.pow.mul hs

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
apply subset_inter <;> gcongr

Goal state after:
case hab
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ s

case hab
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ t
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ X.coeff n = 0

Tactic:
by
  rw [coeff_X, if_neg hn.symm]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n i : ℕ
toFinsupp✝ : R[ℕ]
⊢ (AddMonoidAlgebra.erase n toFinsupp✝).coeff i = if i = n then 0 else toFinsupp✝.coeff i

Tactic:
exact ite_congr rfl (fun _ ↦ rfl) (fun _ ↦ rfl)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
n : ℕ
⊢ (p - q).coeff n = p.coeff n - q.coeff n

Tactic:
by
  simp [coeff, sub_eq_add_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
⊢ (Pi.basis s).repr (single j ((s j) i)) = Finsupp.single ⟨j, i⟩ 1

Tactic:
classical
  ext ⟨j', i'⟩
  by_cases hj : j = j'
  · subst hj
    simp only [Pi.basis, LinearEquiv.trans_apply,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk]
    symm
    simp [Finsupp.single_apply]
  simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
    LinearEquiv.piCongrRight]
  dsimp
  rw [Pi.single_eq_of_ne (Ne.symm hj), map_zero, Finsupp.zero_apply,
    Finsupp.single_eq_of_ne]
  rintro ⟨⟩
  contradiction

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
y : P
hy : y ∈ t1
⊢ ∃ x ∈ s, f x = y

Tactic:
have : y ∈ s.map f := by
      rw [← ht1]
      exact subset_span hy

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
y : P
hy : y ∈ t1
this : y ∈ map f s
⊢ ∃ x ∈ s, f x = y
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
this : f x ∈ span R ↑t1
⊢ x ∈ span R (g '' ↑t1) ⊔ span R ↑t2

Tactic:
← Set.image_id (t1 : Set P),

Goal state after:
case a
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
this : f x ∈ span R (id '' ↑t1)
⊢ x ∈ span R (g '' ↑t1) ⊔ span R ↑t2
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
y : P
hy : y ∈ l.support
⊢ l y • id y = f (l y • id (g y))

Tactic:
unfold id

Goal state after:
case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
y : P
hy : y ∈ l.support
⊢ l y • y = f (l y • g y)
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
iSup_add,

Goal state after:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, f i + iSup g ≤ a
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R.inv

Tactic:
R.inv_eq_self

Goal state after:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
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
s : Submodule R M
n : N
⊢ map₂ f s (R ∙ n) = map (f.flip n) s

Tactic:
by rw [← map₂_span_singleton_eq_map, map₂_flip]

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:
Subsingleton.elim y 0,

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Preorder α
⊢ (∃ x, (∃ b, b < x) ∧ ∃ b, x < b) → ∃ i, 1 < ↑i.length

Tactic:
rintro ⟨x, ⟨y, hxy⟩, z, hzx⟩

Goal state after:
case mpr
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ ∃ i, 1 < ↑i.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg.mp
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

pp: case neg.mpr
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α

Tactic:
· exact (fun h1 ↦ False.elim (h (LTSeries.nonempty_of_finiteDimensionalOrder α)))

Goal state after:
case neg.mpr
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ⇑f '' (a :: as).prod = (List.map (fun s ↦ ⇑f '' s) (a :: as)).prod

Tactic:
by rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]

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

Goal state before:
pp: case insert.mp.refine_1.inr
ι : 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
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ update g i x j ∈ f j

Tactic:
rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]

Goal state after:
case insert.mp.refine_1.inr
ι : 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
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ g j ∈ f j
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case mpr
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
hc1 : ↑c.support ⊆ sR
p : Submodule R M
hp : p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
⊢ ∑ i ∈ c.support, ↑(i • c i) ∈ p

Tactic:
exact Submodule.sum_mem _ fun r hr ↦ hp (hc1 hr) (c _).2

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
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
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 M₃
inst✝¹ : Module R N₂
inst✝ : Module R N₃
a : M →ₗ[R] M₂
b : M₃ →ₗ[R] M₂
c : N →ₗ[R] N₂
d : N₃ →ₗ[R] N₂
hab : a.range ≤ b.range
hcd : c.range ≤ d.range
⊢ (map a c).range ≤ (map b d).range

Tactic:
simp_rw [range_map]

Goal state after:
R : Type u_1
inst✝¹² : CommSemiring R
M : Type u_7
N : Type u_8
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
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 M₃
inst✝¹ : Module R N₂
inst✝ : Module R N₃
a : M →ₗ[R] M₂
b : M₃ →ₗ[R] M₂
c : N →ₗ[R] N₂
d : N₃ →ₗ[R] N₂
hab : a.range ≤ b.range
hcd : c.range ≤ d.range
⊢ Submodule.map₂ (mk R M₂ N₂) a.range c.range ≤ Submodule.map₂ (mk R M₂ N₂) b.range d.range
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
S : Type u_11
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R S
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
f' : S →ₗ[R] M
⊢ map f g ∘ₗ rTensor N f' = map (f ∘ₗ f') g

Tactic:
by
  simp only [rTensor, ← map_comp, comp_id]

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

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

Tactic:
use ⟨f y, mem_map.mpr ⟨y.1, y.2, rfl⟩⟩
        refine Eq.trans ?_ hy
        ext
        simp

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
J : Ideal S
x : S
⊢ x ∈ map (RingHom.snd R S) (I.prod J) ↔ x ∈ J

Tactic:
rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1 ∈ I.prod J, (RingHom.snd R S) x_1 = x) ↔ x ∈ J
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ map (RingHom.snd R S) (I.prod J) = J

Tactic:
ext x
  rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
  exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.2, fun h => ⟨⟨0, x⟩, ⟨⟨Ideal.zero_mem _, h⟩, rfl⟩⟩⟩

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

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : β) → R i)

Tactic:
exact fun e h ↦ isNoetherianRing_of_ringEquiv _ (.piCongrLeft _ e)

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
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
⊢ comap f ⊥ ≤ I

Tactic:
by
  refine le_trans (fun x hx => ?_) bot_le
  rw [mem_comap, Submodule.mem_bot, ← map_zero f] at hx
  exact Eq.symm (hf hx) ▸ Submodule.zero_mem ⊥

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i) →
        (∀ i ∈ insert a s, x i ∈ I i) → ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i

Tactic:
grind [mul_mem_mul]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
m✝ : Multiset R
a : R
m : Multiset R
ih : (Multiset.map (fun x ↦ span {x}) m).prod = span {m.prod}
⊢ (Multiset.map (fun x ↦ span {x}) (a ::ₘ m)).prod = span {(a ::ₘ m).prod}

Tactic:
simp only [Multiset.map_cons, Multiset.prod_cons, ih, ← Ideal.span_singleton_mul_span_singleton]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ ∃ d, Associated (d ^ k) a

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
⊢ ∃ d, Associated (d ^ k) a

Tactic:
· use 1
    rw [one_pow]
    apply (associated_one_iff_isUnit.mpr hab).symm.trans
    rw [hb]
    exact gcd_zero_right' a

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
⊢ ∃ d, Associated (d ^ k) a
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i.hf
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ (Finsupp.linearCombination R Subtype.val).range = ⊤

Tactic:
Finsupp.range_linearCombination

Goal state after:
case i.hf
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ span R (range Subtype.val) = ⊤