mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
h : Basis ι R M
⊢ finrank R M = toNat #ι

Tactic:
← toNat_lift.{v},

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
h : Basis ι R M
⊢ finrank R M = toNat (Cardinal.lift.{v, w} #ι)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
· have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
k : ℕ
⊢ ∀ (i j : n), 0 ≤ (A ^ k) i j

Tactic:
by
  induction k with
  | zero => aesop (add simp one_apply)
  | succ m ih =>
    intro i j; rw [pow_succ, mul_apply]
    exact Finset.sum_nonneg fun l _ => mul_nonneg (ih i l) (hA l j)

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * B * C) i j = A i ⬝ᵥ B *ᵥ Cᵀ j

Tactic:
rw [Matrix.mul_assoc]
  simp [mul_apply, dotProduct, mulVec]

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Nonempty n
A : Matrix l m α
ha : Function.Injective fun B ↦ A * B
v w : m → α
hvw : A *ᵥ v = A *ᵥ w
inhabited_h : Inhabited n
⊢ v = w

Tactic:
suffices (of fun i j => v i) = (of fun i j => w i) from
    funext fun i => congrFun₂ this i (default : n)

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Nonempty n
A : Matrix l m α
ha : Function.Injective fun B ↦ A * B
v w : m → α
hvw : A *ᵥ v = A *ᵥ w
inhabited_h : Inhabited n
⊢ (of fun i j ↦ v i) = of fun i j ↦ w i
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
⊢ ↑(((of (fun i ↦ ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Tactic:
obtain rfl | h := Decidable.eq_or_ne j i
  · rw [DirectSum.of_eq_same, if_pos rfl]
  · rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
⊢ (e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun ((algebraMap R ↥S) r) = (algebraMap R ↥(Subalgebra.map (↑e) S)) r

Tactic:
by ext; exact e.commutes r

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³ * x✝², ⋯⟩

Tactic:
convert! congr_arg₂ (· * ·) h₁ h₂

Goal state after:
case e'_2
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₁ ⟨x✝³, x✝¹⟩ * φ₁ ⟨x✝², x✝⟩

case e'_3
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³, x✝¹⟩ * φ₂ ⟨x✝², x✝⟩
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
m : M
p : ι →₀ N
i : ι
⊢ ((finsuppRight R S M N ι) (m ⊗ₜ[R] p)) i = m ⊗ₜ[R] p i

Tactic:
rw [finsuppRight_apply_tmul, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
P : Type v
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective ⇑p
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
g : P →ₗ[R] P →₀ Shrink.{v, u} R
hg : (p ∘ₗ ↑e) ∘ₗ g = LinearMap.id
⊢ ∃ h, p ∘ₗ h = LinearMap.id

Tactic:
exact ⟨e.toLinearMap ∘ₗ g, hg⟩

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
P : Type v
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective ⇑p
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
g : P →ₗ[R] P →₀ Shrink.{v, u} R
hg : (p ∘ₗ ↑e) ∘ₗ g = LinearMap.id
⊢ ∃ h, p ∘ₗ h = LinearMap.id

Tactic:
exact ⟨e.toLinearMap ∘ₗ g, hg⟩

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι'
⊢ b'.repr ((b.prod b') (Sum.inr i)).2 = b'.repr (b' i)

Tactic:
ext i
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b'.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Finsupp.snd_sumFinsuppLEquivProdFinsupp]
    apply Finsupp.single_apply_left Sum.inr_injective

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : o → Matrix m n α
⊢ (blockDiagonal M)ᴴ = blockDiagonal fun k ↦ (M k)ᴴ

Tactic:
simp only [conjTranspose, blockDiagonal_transpose]
  rw [blockDiagonal_map _ star (star_zero α)]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f g : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ of (fun i j ↦ (f + g) (Pi.single j 1) i) i j =
    ((of fun i j ↦ f (Pi.single j 1) i) + of fun i j ↦ g (Pi.single j 1) i) i j

Tactic:
simp only [Pi.add_apply, LinearMap.add_apply, of_apply, Matrix.add_apply]

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
s : Subfield L
h : s ≤ f.fieldRange
⊢ map f (comap f s) = s

Tactic:
by
  simpa only [inf_of_le_left h] using map_comap_eq f s

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : t * ↑s ∈ R⁰
hr : ¬r = 0
ht : ¬t = 0
⊢ (if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = if hr : t • r = 0 then 0 else ↑⟨t * ↑s, hst⟩ /ₒ ⟨t • r, ⋯⟩

Tactic:
simp only [hr, ht, dif_neg, not_false_iff, or_self_iff, mul_eq_zero, smul_eq_mul]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : t * ↑s ∈ R⁰
hr : ¬r = 0
ht : ¬t = 0
⊢ ↑s /ₒ ⟨r, ⋯⟩ = t * ↑s /ₒ ⟨t * r, ⋯⟩
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
v : M₁
⊢ v₁.equivFun.symm ((toLinAlgEquiv' M) ⇑(v₁.repr v)) = ∑ j, (M *ᵥ ⇑(v₁.repr v)) j • v₁ j

Tactic:
rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]

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

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
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ Submonoid.map h.symm.toMonoidHom T = M

Tactic:
rw [← M.map_id, ← H, Submonoid.map_map]
    congr
    ext
    apply h.symm_apply_apply

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 : ℕ
hn : n ≥ l.support.sup n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ (n - n₁ a) • (algebraMap R A) (l a) • r ^ n₁ a • ↑a ∈ Subalgebra.toSubmodule B'

Tactic:
smul_def,

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 : ℕ
hn : n ≥ l.support.sup n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ (algebraMap A B) (r ^ (n - n₁ a)) * (algebraMap R A) (l a) • r ^ n₁ a • ↑a ∈ Subalgebra.toSubmodule B'
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: F : Type u_4
inst✝² : CommSemiring F
E : Type u_5
inst✝¹ : CommSemiring E
inst✝ : Algebra F E
K : Subalgebra F E
S : Set E
| Subalgebra.restrictScalars F (adjoin (↥(adjoin F ↑K)) S)

Tactic:
← Algebra.adjoin_union_eq_adjoin_adjoin

Goal state after:
F : Type u_4
inst✝² : CommSemiring F
E : Type u_5
inst✝¹ : CommSemiring E
inst✝ : Algebra F E
K : Subalgebra F E
S : Set E
| adjoin F (↑K ∪ S)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
x : R
y : ↥M
⊢ mk x y = mk' (Localization M) x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply, mk', toLocalizationMap_eq_monoidOf]

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

Goal state after:
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
⊢ IsLocalization R⁰ S ↔ IsLocalization P⁰ S
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
⊢ Fin.val ⁻¹' Set.Iio x = Set.univ

Tactic:
ext y

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
y : Fin n
⊢ y ∈ Fin.val ⁻¹' Set.Iio x ↔ y ∈ Set.univ
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ f a ⊗ₜ[R] (1 / f b) = (b • (f a / f b)) ⊗ₜ[R] (1 / f b)

Tactic:
smul_def,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ f a ⊗ₜ[R] (1 / f b) = ((algebraMap R A) b * (f a / f b)) ⊗ₜ[R] (1 / f b)
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ (f a / f b) ⊗ₜ[R] (b • (1 / f b)) = (f a / f b) ⊗ₜ[R] 1

Tactic:
smul_def,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ (f a / f b) ⊗ₜ[R] ((algebraMap R A) b * (1 / f b)) = (f a / f b) ⊗ₜ[R] 1
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
x y s : A
hs : 1 ⊗ₜ[R] s = x ⊗ₜ[R] y
this : R'.mkQ 1 = 0
⊢ R'.mkQ x ⊗ₜ[R] R'.mkQ y = 0

Tactic:
rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
⊢ (Algebra.TensorProduct.map f g).Finite

Tactic:
by
  convert!
    RingHom.Finite.tensorProductMap_id (T := T') Hf |>.comp <|
      (Algebra.TensorProduct.comm _ _ _).toRingEquiv.finite |>.comp <|
        RingHom.Finite.tensorProductMap_id (T := S) Hg |>.comp <|
          (Algebra.TensorProduct.comm _ _ _).toRingEquiv.finite
  simp only [AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, ← AlgEquiv.toAlgHom_toRingHom, ← AlgHom.comp_toRingHom]
  congr
  ext <;> simp

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
C : Type u_3
inst✝ : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp includeRight.toRingHom = g.comp includeRight.toRingHom
⊢ f = g

Tactic:
by
  ext x
  induction x with
  | zero => simp
  | add x y _ _ => simp_all
  | tmul x y => simpa [← map_mul] using congr($h₁ x * $h₂ y)

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
⊢ ∀ (x_1 : IsUnit x), IsQuasiregular (-(⋯.unit⁻¹ • a)) → ∃ (h : IsUnit x), IsQuasiregular (-(⋯.unit⁻¹ • φ a))

Tactic:
refine fun hx this ↦ ⟨hx, ?_⟩

Goal state after:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
hx : IsUnit x
this : IsQuasiregular (-(⋯.unit⁻¹ • a))
⊢ IsQuasiregular (-(⋯.unit⁻¹ • φ a))
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: case inl_add_inr.inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
r✝¹ : R
a✝¹ : A
r✝ : R
a✝ : A
⊢ (algebraMap R C) (inl r✝¹ + ↑a✝¹ + (inl r✝ + ↑a✝)).toProd.1 + φ (inl r✝¹ + ↑a✝¹ + (inl r✝ + ↑a✝)).toProd.2 =
    (algebraMap R C) (inl r✝¹ + ↑a✝¹).toProd.1 + φ (inl r✝¹ + ↑a✝¹).toProd.2 +
      ((algebraMap R C) (inl r✝ + ↑a✝).toProd.1 + φ (inl r✝ + ↑a✝).toProd.2)

Tactic:
simp only [fst_add, fst_inl, fst_inr, add_zero, map_add, snd_add, snd_inl, snd_inr,
          zero_add, φ.map_add]
        rw [add_add_add_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
⊢ star x ≤ y ↔ x ≤ star y

Tactic:
rw [← star_le_star_iff, star_star]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht : LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t
⊢ LinearIndepOn R f (s ∪ t)

Tactic:
apply hs.union ht.of_comp

Goal state after:
R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht : LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t
⊢ Disjoint (span R (f '' s)) (span R (f '' t))
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
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ Set.finrank R (range b) ≤ Fintype.card ι

Tactic:
by
  classical
  refine (finrank_span_le_card _).trans ?_
  rw [Set.toFinset_range]
  exact Finset.card_image_le

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{w, v} (Module.rank R M) = lift.{w, v} ↑(finrank R M)

Tactic:
rw [finrank_eq_rank]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e • e = 0

Tactic:
sum_map,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (shift x) • shift x = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e • e = 0