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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
x y : OreLocalization S X
⊢ x + y = y + x

Tactic:
by
  induction x with | _ r s
  induction y with | _ r' s'
  rcases oreDivAddChar' r r' s s' with ⟨ra, sa, ha, ha'⟩
  rw [ha', oreDiv_add_char' s' s _ _ ha.symm (ha ▸ (sa * s).2), add_comm]
  congr; ext; exact ha

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Divisibility

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
h : IsUnit (f m)
s✝ : N
hxs : 1 = f m * s✝
r : M
s : ↥S
hrs : f ↑(r, s).2 = f (m * (r, s).1)
s' : ↥S
eq : ↑s' * ↑(r, s).2 = ↑s' * (m * (r, s).1)
⊢ ∃ s ∈ S, m ∣ s

Tactic:
exact ⟨s' * s, mul_mem s'.2 s.2, _, mul_left_comm _ m _ ▸ eq⟩

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

Goal state before:
pp: 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₀ : Type ?u.16
inst✝⁴ : Semiring R₀
inst✝³ : Module R₀ X
inst✝² : Module R₀ R
inst✝¹ : IsScalarTower R₀ R X
inst✝ : IsScalarTower R₀ R R
x : OreLocalization S X
⊢ 0 • x = 0

Tactic:
by rw [← smul_one_oreDiv_one_smul, zero_smul, zero_oreDiv, zero_smul]

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

Goal state before:
pp: case 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
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁ + r₂ /ₒ s₂) =
    (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁) + (universalMulHom (↑f) fS ⋯) (r₂ /ₒ s₂)

Tactic:
| _ r₂ s₂
       => 

Goal state after:
case 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
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁ + r₂ /ₒ s₂) =
    (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁) + (universalMulHom (↑f) fS ⋯) (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
f : End A (ι → M)
i : ι
x : M
j : ι
⊢ ∑ x_1, Pi.single x_1 (Pi.single i x x_1) = Pi.single i x

Tactic:
by aesop

Goal state after:
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
f g : End A (ι → M)
i✝ j✝ : ι
x✝ : M
⊢ g (Pi.single j✝ x✝) = ∑ x, Pi.single x (g (Pi.single j✝ x✝) x)

Tactic:
by aesop

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
inst✝ : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), ↑n * x = ↑n * y ↔ x = y
h : ∀ (a a_1 : R), a_1 ∈ M → ∀ (a_2 a_3 : R), a_3 ∈ M → r * (a_3 * a) = r * (a_1 * a_2) → a_3 * a = a_1 * a_2
a b : R
⊢ r * a = r * b → a = b

Tactic:
simpa using h a 1 M.one_mem b 1 M.one_mem

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)
x y : S
⊢ g ((toLocalizationMap M S).sec y).1 * g ↑((toLocalizationMap M S).sec x).2 *
        ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 +
      g ↑((toLocalizationMap M S).sec y).2 * g ((toLocalizationMap M S).sec x).1 *
        ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec y).2 * g ↑((toLocalizationMap M S).sec x).2 *
      ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1

Tactic:
change g _ * g _ * g _ + g _ * g _ * g _ = g _ * g _ * g _

Goal state after:
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)
x y : S
⊢ g ((toLocalizationMap M S).sec y).1 * g ↑((toLocalizationMap M S).sec x).2 *
        g ↑((toLocalizationMap M S).sec (x + y)).2 +
      g ↑((toLocalizationMap M S).sec y).2 * g ((toLocalizationMap M S).sec x).1 *
        g ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec y).2 * g ↑((toLocalizationMap M S).sec x).2 *
      g ((toLocalizationMap M S).sec (x + y)).1
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
z : K
x y : A
hy : y ∈ A⁰
h : mk' K x ⟨y, hy⟩ = z
⊢ (algebraMap A K) x / (algebraMap A K) y = z

Tactic:
rwa [mk'_eq_div] at h

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) * r ^ n₁ a) • l a • ↑a ∈ Subalgebra.toSubmodule B'

Tactic:
← smul_smul,

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 - n₁ a) • r ^ n₁ a • l a • ↑a ∈ Subalgebra.toSubmodule B'
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_smul,

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 - n₁ a) • (algebraMap R A) (l a) • r ^ n₁ a • ↑a ∈ Subalgebra.toSubmodule B'
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
P : Type u_3
inst✝¹⁵ : CommRing P
A✝ : Type u_4
inst✝¹⁴ : CommRing A✝
K✝ : Type u_5
B✝ : Type u_6
inst✝¹³ : CommRing B✝
inst✝¹² : IsDomain B✝
inst✝¹¹ : Field K✝
L✝ : Type u_7
inst✝¹⁰ : Field L✝
inst✝⁹ : Algebra A✝ K✝
inst✝⁸ : IsFractionRing A✝ K✝
g : A✝ →+* L✝
A : Type u_8
B : Type u_9
K : Type u_10
L : Type u_11
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Algebra B L
inst✝ : IsFractionRing B L
f : A ≃+* B
r : A
x : K
⊢ (ringEquivOfRingEquiv f).toFun (r • x) = ↑f r • (ringEquivOfRingEquiv f).toFun x

Tactic:
by simp [Algebra.smul_def]

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

Goal state before:
pp: G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst✝¹⁷ : Group G
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : MulSemiringAction G L
inst✝¹ : SMulDistribClass G B L
inst✝ : SMulCommClass G A B
g : G
y : L
a b : A
hb : b ∈ A⁰
⊢ g • ((algebraMap A K) a / (algebraMap A K) b) • y = ((algebraMap A K) a / (algebraMap A K) b) • g • y

Tactic:
obtain ⟨c, d, hd, rfl⟩ := IsFractionRing.div_surjective B y

Goal state after:
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst✝¹⁷ : Group G
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : MulSemiringAction G L
inst✝¹ : SMulDistribClass G B L
inst✝ : SMulCommClass G A B
g : G
a b : A
hb : b ∈ A⁰
c d : B
hd : d ∈ B⁰
⊢ g • ((algebraMap A K) a / (algebraMap A K) b) • ((algebraMap B L) c / (algebraMap B L) d) =
    ((algebraMap A K) a / (algebraMap A K) b) • g • ((algebraMap B L) c / (algebraMap B L) d)
Module: Mathlib.Algebra.Algebra.Rat

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionRing R
inst✝⁴ : CharZero R
inst✝³ : DivisionRing S
inst✝² : CharZero S
inst✝¹ : EquivLike F R S
inst✝ : RingEquivClass F R S
f : F
c : ℚ
x : R
⊢ f (c • x) = (RingHom.id ℚ) c • f x

Tactic:
by simp [Algebra.smul_def]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : StarMul α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹

Tactic:
ext
  simp only [mem_star, mem_inv, star_inv₀]

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ Submodule.span A ↑l.range ≤ (liftBaseChange A l).range

Tactic:
rw [Submodule.span_le]
    rintro _ ⟨x, rfl⟩
    exact ⟨1 ⊗ₜ x, by simp⟩

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : Semiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra S A
inst✝¹⁴ : IsScalarTower R S A
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Algebra R C
inst✝⁹ : Algebra S C
inst✝⁸ : IsScalarTower R S C
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Semiring E
inst✝⁴ : Algebra R E
inst✝³ : Algebra S E
inst✝² : IsScalarTower R S E
inst✝¹ : Semiring F
inst✝ : Algebra R F
⊢ (_root_.TensorProduct.lid R A) (1 ⊗ₜ[R] 1) = 1

Tactic:
by simp [Algebra.smul_def]

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

Goal state before:
pp: R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
x : A
y : C
⊢ x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y) = 1 ⊗ₜ[A] (x ⊗ₜ[R] y)

Tactic:
trans x • 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)

Goal state after:
R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
x : A
y : C
⊢ x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y) = x • 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)

R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
x : A
y : C
⊢ x • 1 ⊗ₜ[A] (1 ⊗ₜ[R] y) = 1 ⊗ₜ[A] (x ⊗ₜ[R] y)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁷ : Semifield R
inst✝⁶ : Field S
inst✝⁵ : NonUnitalRing A
inst✝⁴ : Module R A
inst✝³ : Module S A
inst✝² : Algebra R S
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass S A A
f : S → R
a b : A
⊢ QuasispectrumRestricts (a * b) f ↔ QuasispectrumRestricts (b * a) f

Tactic:
simp only [quasispectrumRestricts_iff, quasispectrum.mul_comm]

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ Function.Bijective (⇑includeLeft ∘ ⇑(TensorProduct.rid R S A))

Tactic:
convert_to Function.Bijective (map (.id R A) (Algebra.ofId R B))

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ ⇑includeLeft ∘ ⇑(TensorProduct.rid R S A) = ⇑(map (AlgHom.id R A) (ofId R B))

R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ Function.Bijective ⇑(map (AlgHom.id R A) (ofId R B))
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ Subalgebra.map (lmul' R) (map f g).range = f.range ⊔ g.range

Tactic:
map_range,

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ Subalgebra.map (lmul' R) ((includeLeft.comp f).range ⊔ (includeRight.comp g).range) = f.range ⊔ g.range
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ r • a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
induction hr using AddSubmonoid.closure_induction with
  | zero => simp
  | add r₁ r₂ _ _ hr₁ hr₂ => simpa [add_smul] using add_mem hr₁ hr₂
  | mem r hr =>
  induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra 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)
T : Subalgebra R A
hT : T ≤ iSup K
⊢ ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
intro i j x hxi hxj

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra 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)
T : Subalgebra R A
hT : T ≤ iSup K
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
h : ∀ a ∈ S, 1 ⊗ₜ[R] a * x = x * 1 ⊗ₜ[R] a
b : B
hb : b ∈ S
⊢ (Algebra.TensorProduct.comm R A B).symm (b ⊗ₜ[R] 1 * (Algebra.TensorProduct.comm R A B) x) =
    (Algebra.TensorProduct.comm R A B).symm ((Algebra.TensorProduct.comm R A B) x * b ⊗ₜ[R] 1)

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
h : ∀ a ∈ S, a ⊗ₜ[R] 1 * (Algebra.TensorProduct.comm R A B) x = (Algebra.TensorProduct.comm R A B) x * a ⊗ₜ[R] 1
b : B
hb : b ∈ S
⊢ (Algebra.TensorProduct.comm R A B) (1 ⊗ₜ[R] b * x) = (Algebra.TensorProduct.comm R A B) (x * 1 ⊗ₜ[R] b)

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
⊢ 0 ≤ star u * x * u ↔ 0 ≤ x

Tactic:
by
  simpa using hu.star.star_right_conjugate_nonneg_iff

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

Goal state before:
pp: F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F E

Tactic:
by
  rw [subalgebra_top_rank_eq_submodule_top_rank]
  exact _root_.rank_top F E

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

Goal state before:
pp: R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
⊢ Basis (m ⊕ n) R V

Tactic:
have br : W.mkQ ∘ b ∘ Sum.inr = bQ := by
    ext j
    apply Function.rightInverse_surjInv W.mkQ_surjective

Goal state after:
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ Basis (m ⊕ n) R V
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
have : Finite s := lt_aleph0_iff_finite.mp (hs' ▸ natCast_lt_aleph0)

Goal state after:
case inl
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
← mem_toNonUnitalSubring,

Goal state after:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S.toNonUnitalSubring ↔ x ∈ T
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S.toNonUnitalSubring ↔ x ∈ T

Tactic:
← mem_toNonUnitalSubring,

Goal state after:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ (iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x

Tactic:
subst hT
  dsimp [iSupLift]
  apply Set.iUnionLift_mk

Goal state after: