mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
⊢ k ∣ m * gcd k n

Tactic:
by
  rw [mul_comm] at H ⊢
  exact dvd_gcd_mul_of_dvd_mul H

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ IsUnit (gcd x' y')

Tactic:
rw [← associated_one_iff_isUnit]
  refine Associated.of_mul_left ?_ (Associated.refl <| gcd x y) h
  convert (gcd_mul_left' (gcd x y) x' y').symm
  rw [← ex, ← ey, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
⊢ gcd x y = 1 ↔ ¬x ∣ y

Tactic:
rw [← hx.isUnit_gcd_iff, ← normalize_eq_one, NormalizedGCDMonoid.normalize_gcd]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
s : { s // LinearIndepOn R id s }
⊢ Cardinal.mk ↑↑s ≤ ⊥

Tactic:
simp [(linearIndependent_subsingleton_iff _).mp s.2]

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

Goal state before:
pp: R : Type u
S : Type u_1
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι✝ : Type w
ι' : Type w'
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R R
this : #ι = ↑(finrank R R)
⊢ Unique ι

Tactic:
have : Subsingleton ι ∧ Nonempty ι := by simpa [Cardinal.eq_one_iff_unique]

Goal state after:
R : Type u
S : Type u_1
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι✝ : Type w
ι' : Type w'
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R R
this✝ : #ι = ↑(finrank R R)
this : Subsingleton ι ∧ Nonempty ι
⊢ Unique ι
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : AddCommMonoid α
inst✝ : CommMagma α
v w : m → α
⊢ v ⬝ᵥ w = w ⬝ᵥ v

Tactic:
by
  simp_rw [dotProduct, mul_comm]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : MulZeroClass α
inst✝ : NoZeroDivisors α
a b : n → α
⊢ vecMulVec a b = 0 ↔ a = 0 ∨ b = 0

Tactic:
by
  simp only [← ext_iff, vecMulVec_apply, zero_apply, mul_eq_zero, funext_iff, Pi.zero_apply,
    forall_or_left, forall_or_right]

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
⊢ (single i i c).diag = Pi.single i c

Tactic:
ext j
  by_cases hij : i = j <;> (try rw [hij]) <;> simp [hij]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ map (Algebra.linearMap R A) (R ∙ 1) = 1

Tactic:
map_span,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ span R (⇑(Algebra.linearMap R A) '' {1}) = 1
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ (b.repr (b (i, j).1 • if (i, j).2 = (i', j').2 then 1 else 0)) (i', j').1 = (single (i, j) 1) (i', j')

Tactic:
dsimp only

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ (b.repr (b i • if j = j' then 1 else 0)) i' = (single (i, j) 1) (i', j')
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ f : C →ₐ[A] D
⊢ (fun fg ↦
        let x := fg.fst.toAlgebra;
        AlgHom.restrictScalars A fg.snd)
      ((fun f ↦ ⟨AlgHom.domRestrict B f, AlgHom.extendScalars B f⟩) f) =
    f

Tactic:
dsimp only

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ f : C →ₐ[A] D
⊢ AlgHom.restrictScalars A (AlgHom.extendScalars B f) = f
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n α
x : n → α
y : m → α
⊢ x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x

Tactic:
by
  rw [dotProduct_mulVec, dotProduct_comm, vecMul_transpose]

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
x✝ : Nonempty n
i : n
x : α
hx : ∀ (g : Matrix n n α), g * (scalar n) x = (scalar n) x * g
⊢ (∀ (g : α), g * x = x * g) ∧ (scalar n) x = (scalar n) x

Tactic:
by simpa using fun r ↦ congr($(hx (single i i r)) i i)

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ f a * Multiset.count a {a} = f a

Tactic:
by rw [Multiset.count_singleton_self, mul_one]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
rw [le_def, le_def]; constructor <;> intro h _ _ h' <;> exact h h'

Goal state after:
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
rw [le_def, le_def]; constructor <;> intro h _ _ h' <;> exact h h'

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ¬Module.rank R M < ℵ₀

Tactic:
Module.rank_lt_aleph0_iff

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ¬Module.Finite R M
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
H : ¬Module.Finite S M
⊢ ¬Module.rank S M < ℵ₀

Tactic:
Module.rank_lt_aleph0_iff

Goal state after:
R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
H : ¬Module.Finite S M
⊢ ¬Module.Finite S M
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
H : ¬Module.Finite R S
⊢ ¬Module.rank R S < ℵ₀

Tactic:
Module.rank_lt_aleph0_iff

Goal state after:
R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
H : ¬Module.Finite R S
⊢ ¬Module.Finite R S
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
r : R
⊢ ∀ (i : ι) (x : ↑↑(K i)), (f i) (r • x) = r • (f i) x

Tactic:
all_goals simp

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

Goal state before:
pp: case hopi
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), Set.inclusion ⋯ (x + y) = Set.inclusion ⋯ x + Set.inclusion ⋯ y

pp: case h
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), (f i) (x + y) = (f i) x + (f i) y

Tactic:
all_goals simp

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

Goal state before:
pp: case hopi
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), Set.inclusion ⋯ (x * y) = Set.inclusion ⋯ x * Set.inclusion ⋯ y

pp: case h
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), (f i) (x * y) = (f i) x * (f i) y

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
n : N
⊢ (finsuppScalarLeft R N ι).symm (Finsupp.single i n) = Finsupp.single i 1 ⊗ₜ[R] n

Tactic:
by
  simp [finsuppScalarLeft, finsuppLeft_symm_apply_single]

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

Goal state before:
pp: case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ star y * star x = x * y

Tactic:
hx.star_eq,

Goal state after:
case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ star y * x = x * y
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ⅟2 • (x + star x) = x

Tactic:
hx.star_eq,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ⅟2 • (x + x) = x
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ⅟2 • (x - star x) = ↑0

Tactic:
hx.star_eq,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ⅟2 • (x - x) = ↑0
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarMul A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
r : R
⊢ (algebraMap R A) (star r) = star ((algebraMap R A) r)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, star_smul, star_one]

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

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ blockDiagonal' (fun k ↦ M k * N k) ⟨k, i⟩ ⟨k', j⟩ = (blockDiagonal' M * blockDiagonal' N) ⟨k, i⟩ ⟨k', j⟩

Tactic:
simp only [blockDiagonal'_apply, mul_apply, ← Finset.univ_sigma_univ, Finset.sum_sigma]

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x, ∑ x_1, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ baseChange A ⊤ = ⊤

Tactic:
rw [eq_top_iff, ← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..)]

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span A {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ baseChange A ⊤
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span A ↑(map ((TensorProduct.mk R A M) 1) (span R s)) = span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
map_span,

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span A ↑(span R (⇑((TensorProduct.mk R A M) 1) '' s)) = span A (⇑((TensorProduct.mk R A M) 1) '' s)
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
n : N
hn : n ≠ 0
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
h : ms.1 = 0
⊢ n = 0

Tactic:
rwa [h, map_zero, (f.map_units _).mul_left_eq_zero] at eq

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

Goal state before:
pp: R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ 0⁻¹ = 0

Tactic:
rw [OreLocalization.zero_def, OreLocalization.inv_def]
  simp

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

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✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ (toMatrix b b) ((lmul R S) x) i j = (b.repr (x * b j)) i

Tactic:
toMatrix_lmul' b x i j

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ (b.repr (x * b j)) i = (b.repr (x * b j)) i
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r : R
⊢ (universalHom f fS hf) (numeratorHom r) = f r

Tactic:
by
  simp [numeratorHom_apply, universalHom_apply]

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

Goal state before:
pp: case inr
ι : Type u_5
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
R : Type u_8
M : Type u_9
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis ι R M
a : ι → R
s : End R M
hs : ∀ (k : ι), s (b k) = a k • b k
i j k : ι
hjk : j ≠ k
⊢ s (if j = k then b i else 0) - (b.end (i, j)) (s (b k)) =
    (if j = k then a i • b i else 0) - if j = k then a j • b i else 0

Tactic:
simp [hs, Basis.end_apply_apply, hjk]

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
⊢ (fun a b ↦ r ^ n • b • ↑a) a (l a) ∈ Subalgebra.toSubmodule B'

Tactic:
dsimp only

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
⊢ r ^ n • l a • ↑a ∈ Subalgebra.toSubmodule B'
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: 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
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
obtain ⟨⟨-, c, hmc, rfl⟩, hc⟩ := exists_of_eq (M := Algebra.algebraMapSubmonoid S₂ M₁) hxy

Goal state after:
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
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : ↑⟨(algebraMap R S₂) c, ⋯⟩ * (algebraMap R S₂) r = ↑⟨(algebraMap R S₂) c, ⋯⟩ * (algebraMap R S₂) s
⊢ ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: case inr
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Subsingleton R
right✝ : Nontrivial S
⊢ False

Tactic:
· apply (h.map_units S 1).ne_zero
    rw [Subsingleton.eq_zero ((1 : nonZeroDivisors R) : R), map_zero]

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 L)

Tactic:
IsScalarTower.algebraMap_eq R K 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 K L).comp (algebraMap R K))