mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
this : rd * rb * ↑s₁ = ↑sd * ↑sc * ↑s₃
⊢ add'' r₃ s₃ r₁ s₁ = add'' r₃ s₃ r₂ s₂

Tactic:
add''_char _ _ _ _ rc sc hc (sc * s₃).2

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
this : rd * rb * ↑s₁ = ↑sd * ↑sc * ↑s₃
⊢ add'' r₃ s₃ r₁ s₁ = (↑sc • r₃ + rc • r₂) /ₒ ⟨↑sc * ↑s₃, ⋯⟩
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
q : (sa • r₁ + ra • r₂) /ₒ (sa * s₁) + r₃ /ₒ s₃ = (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁))
⊢ (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁)) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)

Tactic:
clear q

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁)) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ (M *ᵥ ⇑(v₁.repr (v₁ i))) j • v₂ j = M j i • v₂ j

Tactic:
rw [Basis.repr_self, Matrix.mulVec, dotProduct, Finset.sum_eq_single i, Finsupp.single_eq_same,
    mul_one]

Goal state after:
case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ ∀ b ∈ Finset.univ, b ≠ i → M j b * (Finsupp.single i 1) b = 0

case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ i ∉ Finset.univ → M j i * (Finsupp.single i 1) i = 0
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : IsCancelMulZero M
⊢ ∀ {a : N}, a ≠ 0 → IsRightRegular a

Tactic:
intro n

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : IsCancelMulZero M
n : N
⊢ n ≠ 0 → IsRightRegular n
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Tactic:
clear q

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
q : (sa • r₂ /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Tactic:
clear q

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
⊢ (fun f i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ })
      ((fun m ↦ { toFun := fun x i ↦ ∑ j, (m i j) (x j), map_add' := ⋯, map_smul' := ⋯ }) m) =
    m

Tactic:
ext; simp [Pi.single_apply, apply_ite]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr ↑(snf.bN a)) (snf.f i) = (snf.a i • c) i

Tactic:
Finsupp.smul_apply,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr ↑(snf.bN a)) (snf.f i) = snf.a i • c i
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
x₁ x₂ : Localization (Submonoid.comap (Pi.evalRingHom R i) S)
eq : (mapPiEvalRingHom S) x₁ = (mapPiEvalRingHom S) x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨r₁, s₁, rfl⟩ := exists_mk'_eq T x₁
    obtain ⟨r₂, s₂, rfl⟩ := exists_mk'_eq T x₂
    simp_rw [map_mk'] at eq
    rw [IsLocalization.eq] at eq ⊢
    obtain ⟨s, hs⟩ := eq
    refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩
    obtain rfl | ne := eq_or_ne j i
    · simpa using hs
    · simp [update_of_ne ne]

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

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module R N₂
inst✝³ : Module S N₁
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ f (r • s') = r • f s'

Tactic:
map_smul

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

Goal state before:
pp: case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
⊢ ∀ n ≥ l.support.sup n₁, (r ^ n • l.sum fun i c ↦ c • ↑i) ∈ B'

Tactic:
intro n

Goal state after:
case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
⊢ n ≥ l.support.sup n₁ → (r ^ n • l.sum fun i c ↦ c • ↑i) ∈ B'
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case e'_3
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₁ T) ((algebraMap R S₁) m) * (algebraMap S₂ T) ((algebraMap R S₂) ↑(z, ⟨n, hn⟩).2) *
      (algebraMap S₁ T) ↑hunit.unit⁻¹ =
    a * (algebraMap S₂ T) ((algebraMap R S₂) n) * (algebraMap S₁ T) ((algebraMap R S₁) m * ↑hunit.unit⁻¹)

Tactic:
rw [map_mul]
      ring

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_4
inst✝⁴ : CommSemiring S
K : Type u_5
inst✝³ : CommSemiring K
inst✝² : Algebra R K
e : R ≃+* S
inst✝¹ : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h : ∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)
inst✝ : IsLocalization M₁ K
⊢ ∀ (r : S), (algebraMap S K) r = (algebraMap S K) r

Tactic:
by simp [RingHom.algebraMap_toAlgebra, h]

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
⊢ IsFractionRing R S ↔ IsFractionRing P S

Tactic:
delta IsFractionRing
  convert! isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h
  exact (MulEquivClass.map_nonZeroDivisors h).symm

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective ⇑(algebraMap R S)

Tactic:
refine Function.Injective.of_comp (f := algebraMap S L) ?_

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case tmul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
i : N
m : M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, i ⊗ₜ[R] m = (rTensor M J.subtype) y

Tactic:
| tmul i m =>

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
⊢ s⋆ = s

Tactic:
rw [← star_preimage]

Goal state after:
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
⊢ star ⁻¹' s = s
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ x ∈ σ (- -↑ₐ r + a) ↔ x ∈ σ (↑ₐ r + a)

Tactic:
neg_neg

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ x ∈ σ (↑ₐ r + a) ↔ x ∈ σ (↑ₐ r + a)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Module A M
inst✝⁴ : Module B M
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R B M
r t : A
⊢ (r + t) • (Algebra.lsmul R R M).toLinearMap =
    r • (Algebra.lsmul R R M).toLinearMap + t • (Algebra.lsmul R R M).toLinearMap

Tactic:
ext
        simp only [add_smul, LinearMap.add_apply]

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

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y : B) (x_1 : A) (y_1 : B), (x_1 ⊗ₜ[R] y_1 * x ⊗ₜ[R] y) • m = x_1 ⊗ₜ[R] y_1 • x ⊗ₜ[R] y • m

Tactic:
intro a₁ b₁ a₂ b₂

Goal state after:
case refine_2.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a₁ : A
b₁ : B
a₂ : A
b₂ : B
⊢ (a₂ ⊗ₜ[R] b₂ * a₁ ⊗ₜ[R] b₁) • m = a₂ ⊗ₜ[R] b₂ • a₁ ⊗ₜ[R] b₁ • m
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
x : M
h₁ : x ∈ span R (range fun x ↦ ↑(f x))
h₂ : x ∈ span R (range g)
this : x ∈ M'
⊢ x = 0

Tactic:
obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a ↦ a • g i) ∈ span R (range fun x ↦ ↑(f x))
h₂ : (c.sum fun i a ↦ a • g i) ∈ span R (range g)
this : (c.sum fun i a ↦ a • g i) ∈ M'
⊢ (c.sum fun i a ↦ a • g i) = 0
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
ι : Type w
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)

Tactic:
by
  obtain ⟨⟨_, bs⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
    Cardinal.sum_const]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f)) ∘ₗ f) (hB b) = id (hB b)

Tactic:
have fb_eq : f b = hC ⟨f b, BC b.2⟩ := by
    change f b = Basis.extend this _
    simp_rw [Basis.extend_apply_self]

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f)) ∘ₗ f) (hB b) = id (hB b)
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : StrongRankCondition K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Finite K
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ #V < ℵ₀

Tactic:
rw [← lift_lt_aleph0.{v, u}, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V]

Goal state after:
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : StrongRankCondition K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Finite K
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ lift.{v, u} #K ^ lift.{u, v} (Module.rank K V) < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ comap (f ^ m) (LinearMap.ker (f ^ (k + 1))) ≤ comap (f ^ m) (LinearMap.ker (f ^ k.succ))

Tactic:
Nat.add_one

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ comap (f ^ m) (LinearMap.ker (f ^ k.succ)) ≤ comap (f ^ m) (LinearMap.ker (f ^ k.succ))
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
⊢ eval₂ f x p * eval₂ f x (C a) = eval₂ f x p * f a

pp: case hf
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
⊢ ∀ (k : ℕ), Commute (f ((C a).coeff k)) x

Tactic:
eval₂_C

Goal state after:
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
⊢ eval₂ f x p * f a = eval₂ f x p * f a

case hf
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
⊢ ∀ (k : ℕ), Commute (f ((C a).coeff k)) x
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ comp 0 p = 0

Tactic:
by rw [← C_0, C_comp]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q : R[X]
⊢ eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
  | monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n1 : n = 1
⊢ 0 < n.minFac

pp: case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac

Tactic:
· simp [n1]

Goal state after:
case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Monoid M
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f : M →* A
x : R[M]
⊢ ((lift S A M) f) ((mapRingHom M (algebraMap R S)) x) = ((lift R A M) f) x

Tactic:
induction x using induction with

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ x * (X ^ k).coeff k + y * (X ^ m).coeff k ≠ 0 ∧ x * (X ^ k).coeff m + y * (X ^ m).coeff m ≠ 0

Tactic:
coeff_X_pow_self,

Goal state after:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ x * 1 + y * (X ^ m).coeff k ≠ 0 ∧ x * (X ^ k).coeff m + y * 1 ≠ 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ x * (X ^ k).coeff k + y * (X ^ m).coeff k + z * (X ^ n).coeff k ≠ 0 ∧
    x * (X ^ k).coeff m + y * (X ^ m).coeff m + z * (X ^ n).coeff m ≠ 0 ∧
      x * (X ^ k).coeff n + y * (X ^ m).coeff n + z * (X ^ n).coeff n ≠ 0

Tactic:
coeff_X_pow_self,

Goal state after:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ x * 1 + y * (X ^ m).coeff k + z * (X ^ n).coeff k ≠ 0 ∧
    x * (X ^ k).coeff m + y * 1 + z * (X ^ n).coeff m ≠ 0 ∧ x * (X ^ k).coeff n + y * (X ^ m).coeff n + z * 1 ≠ 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ #{k, m} = 2

Tactic:
card_insert_of_notMem (mt mem_singleton.mp h),

Goal state after:
R : Type u
inst✝ : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ #{m} + 1 = 2
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddMonoid M
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f : Multiplicative M →* A
x : R[M]
⊢ ((lift S A M) f) ((mapRingHom M (algebraMap R S)) x) = ((lift R A M) f) x

Tactic:
induction x using induction with

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

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
m : Multiset R[A]
⊢ m.prod.coeff.support.sup degb ≤ (Multiset.map (fun f ↦ f.coeff.support.sup degb) m).sum

Tactic:
induction m using Quot.inductionOn
  rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sum_coe, Multiset.prod_coe]
  exact sup_support_list_prod_le degb0 degbm _

Goal state after: