mathlib-initiative/mathlib-tactics huggingface dataset:
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 K
y : L
⊢ y ∈ map f s ↔ ∃ x ∈ s, f x = y

Tactic:
unfold map

Goal state after:
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
s : Subfield K
y : L
⊢ (y ∈
      let __src := Subring.map f s.toSubring;
      { toSubring := __src, inv_mem' := ⋯ }) ↔
    ∃ x ∈ s, f x = y
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : K
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

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

Goal state before:
pp: m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
R : Type u_7
M₁ : Type u_8
M₂ : Type u_9
inst✝⁵ : Finite m
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
A : Matrix m n R
x : M₁
⊢ ((toLin v₁ v₂) A) x = 0 ↔ ∀ (j : m), (A *ᵥ ⇑(v₁.repr x)) j = 0

Tactic:
by
  have := Fintype.ofFinite m
  rw [toLin_apply]
  exact ⟨Fintype.linearIndependent_iff.mp v₂.linearIndependent _, fun h ↦ by simp [h]⟩

Goal state after:
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₁
⊢ (toLinAlgEquiv v₁) 1 = LinearMap.id

Tactic:
by
  rw [← LinearMap.toMatrixAlgEquiv_id v₁, Matrix.toLinAlgEquiv_toMatrixAlgEquiv]

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
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI₁ : Module.Finite R ↥I
hI₂ : IsTorsionFree R ↥I
this✝ : Module.Finite R ↥(restrictScalars R I)
this : IsTorsionFree R ↥(restrictScalars R I)
⊢ Free R ↥I

Tactic:
change Module.Free R (restrictScalars R I)

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI₁ : Module.Finite R ↥I
hI₂ : IsTorsionFree R ↥I
this✝ : Module.Finite R ↥(restrictScalars R I)
this : IsTorsionFree R ↥(restrictScalars R I)
⊢ Free R ↥(restrictScalars R I)
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
b✝ : ι → M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
⊢ (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n

Tactic:
by
  choose n o hno bO bN a snf using N.exists_smith_normal_form_of_le b O N_le_O
  refine
    ⟨o, n, bO, bN.map (comapSubtypeEquivOfLe N_le_O).symm, (Fin.castLEEmb hno), a,
      fun i ↦ ?_⟩
  ext
  simp only [snf, Basis.map_apply, Submodule.comapSubtypeEquivOfLe_symm_apply,
    Submodule.coe_smul_of_tower, Fin.castLEEmb_apply]

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

Goal state before:
pp: case refine_1.inl
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
r₁ r₂ : (i : ι) → R i
j : ι
S : Submonoid (R j)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R j) S
s₁ s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R j) ↑s₂, ⋯⟩ * (Pi.evalRingHom R j) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R j) ↑s₁, ⋯⟩ * (Pi.evalRingHom R j) r₂)
⊢ (↑⟨update 0 j ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 j ↑s, ⋯⟩ * (↑s₁ * r₂)) j

pp: case refine_1.inr
ι : 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
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
j : ι
ne : j ≠ i
⊢ (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₁ * r₂)) j

Tactic:
· simpa using hs

Goal state after:
case refine_1.inr
ι : 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
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
j : ι
ne : j ≠ i
⊢ (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₁ * r₂)) j
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
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (↑(y₁ * y₂) * x₁) y₁ + (algebraMap R S) ↑(y₁ * y₂) * mk' S x₂ y₂ = (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁)

Tactic:
mk'_add_eq_iff_add_mul_eq_mul,

Goal state after:
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
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑(y₁ * y₂) * x₁) + (algebraMap R S) ↑(y₁ * y₂) * mk' S x₂ y₂ * (algebraMap R S) ↑y₁ =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁
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 (↑m • mk' S r m • s') = ↑m • mk' S r m • f s'

Tactic:
← smul_assoc,

Goal state after:
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 ((↑m • mk' S r m) • s') = (↑m • mk' S r m) • f s'
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ ≃ₐ[A] K₂
f : L₁ ≃ₐ[B] L₂
x : K₁
⊢ (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)

Tactic:
by
  exact algHom_commutes e.toAlgHom f.toAlgHom _

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

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
⊢ Nontrivial R ↔ Nontrivial S

Tactic:
by_contra! ⟨_, _⟩ | ⟨_, _⟩
  · obtain ⟨c, hc⟩ := h.exists_of_eq (x := 1) (y := 0) (Subsingleton.elim _ _)
    simp at hc
  · 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
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
inst✝⁸ : IsDomain A
k : Type u_6
K : Type u_7
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A k
inst✝⁴ : Algebra A K
inst✝³ : Algebra k K
inst✝² : FaithfulSMul A k
inst✝¹ : FaithfulSMul A K
inst✝ : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x✝ : A × ↥A⁰
a₁ : A
a₂ : ↥A⁰
⊢ ↑a₂ • (Localization.mk a₁ a₂ • b) • c = ↑a₂ • Localization.mk a₁ a₂ • b • c

Tactic:
← smul_assoc,

Goal state after:
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
inst✝⁸ : IsDomain A
k : Type u_6
K : Type u_7
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A k
inst✝⁴ : Algebra A K
inst✝³ : Algebra k K
inst✝² : FaithfulSMul A k
inst✝¹ : FaithfulSMul A K
inst✝ : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x✝ : A × ↥A⁰
a₁ : A
a₂ : ↥A⁰
⊢ ((↑a₂ • Localization.mk a₁ a₂) • b) • c = (↑a₂ • Localization.mk a₁ a₂) • b • c
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
Sₘ : Type u_5
inst✝³ : CommSemiring Sₘ
inst✝² : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra R Sₘ
inst✝ : IsScalarTower R S Sₘ
y : ↥M
⊢ IsUnit ((algebraMap R Sₘ) ↑y)

Tactic:
rw [IsScalarTower.algebraMap_apply _ S]
  exact IsLocalization.map_units Sₘ ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : Surjective ⇑(algebraMap R A)
⊢ Algebra.IsEpi R A

Tactic:
by
  refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun a ↦ ?_
  obtain ⟨r, rfl⟩ := h a
  rw [algebraMap_eq_smul_one, smul_tmul]

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
⊢ NonUnitalNonAssocSemiring α

Tactic:
let zero := e.zero

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
⊢ NonUnitalNonAssocSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
⊢ NonUnitalSemiring α

Tactic:
let zero := e.zero

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
⊢ NonUnitalSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
⊢ NonUnitalCommSemiring α

Tactic:
let zero := e.zero

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
⊢ NonUnitalCommSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
⊢ NonUnitalNonAssocRing α

Tactic:
let zero := e.zero

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
⊢ NonUnitalNonAssocRing α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
⊢ NonUnitalRing α

Tactic:
let zero := e.zero

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := e.zero
⊢ NonUnitalRing α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
⊢ NonUnitalCommRing α

Tactic:
let zero := e.zero

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
⊢ NonUnitalCommRing α
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← smul_mul_assoc,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b
⊢ spectrum R (↑u * a * ↑u⁻¹) = spectrum R a

Tactic:
by
    refine le_antisymm (this a u) ?_
    apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹
    simp [mul_assoc]

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
R✝ : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝²³ : CommSemiring R✝
inst✝²² : CommSemiring S
inst✝²¹ : CommSemiring T
inst✝²⁰ : Semiring A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R✝ A
inst✝¹⁷ : Algebra R✝ B
inst✝¹⁶ : Algebra S A
inst✝¹⁵ : Algebra S B
inst✝¹⁴ : Algebra T A
inst✝¹³ : SMulCommClass R✝ T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : SMulCommClass R✝ S A
inst✝¹⁰ : CompatibleSMul R✝ S A B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ (q.den • q • m) ⊗ₜ[R] n = m ⊗ₜ[R] (q.den • q • n)

Tactic:
← smul_assoc,

Goal state after:
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
R✝ : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝²³ : CommSemiring R✝
inst✝²² : CommSemiring S
inst✝²¹ : CommSemiring T
inst✝²⁰ : Semiring A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R✝ A
inst✝¹⁷ : Algebra R✝ B
inst✝¹⁶ : Algebra S A
inst✝¹⁵ : Algebra S B
inst✝¹⁴ : Algebra T A
inst✝¹³ : SMulCommClass R✝ T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : SMulCommClass R✝ S A
inst✝¹⁰ : CompatibleSMul R✝ S A B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ ((q.den • q) • m) ⊗ₜ[R] n = m ⊗ₜ[R] (q.den • q • n)
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
R✝ : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝²³ : CommSemiring R✝
inst✝²² : CommSemiring S
inst✝²¹ : CommSemiring T
inst✝²⁰ : Semiring A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R✝ A
inst✝¹⁷ : Algebra R✝ B
inst✝¹⁶ : Algebra S A
inst✝¹⁵ : Algebra S B
inst✝¹⁴ : Algebra T A
inst✝¹³ : SMulCommClass R✝ T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : SMulCommClass R✝ S A
inst✝¹⁰ : CompatibleSMul R✝ S A B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ ((q.den • q) • m) ⊗ₜ[R] n = m ⊗ₜ[R] (q.den • q • n)

Tactic:
← smul_assoc,

Goal state after:
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
R✝ : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝²³ : CommSemiring R✝
inst✝²² : CommSemiring S
inst✝²¹ : CommSemiring T
inst✝²⁰ : Semiring A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R✝ A
inst✝¹⁷ : Algebra R✝ B
inst✝¹⁶ : Algebra S A
inst✝¹⁵ : Algebra S B
inst✝¹⁴ : Algebra T A
inst✝¹³ : SMulCommClass R✝ T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : SMulCommClass R✝ S A
inst✝¹⁰ : CompatibleSMul R✝ S A B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ ((q.den • q) • m) ⊗ₜ[R] n = m ⊗ₜ[R] ((q.den • q) • n)
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Ring (κ i)
inst✝ : (i : ι) → Algebra R (κ i)
a : (i : ι) → κ i
⊢ {r | ∀ (i : ι), IsUnit ((algebraMap R ((i : ι) → κ i)) r i - a i)} =
    {x | ∀ (i : ι), IsUnit ((algebraMap R (κ i)) x - a i)}

Tactic:
algebraMap_apply

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
⊢ ↑(iSup K) = ⋃ i, ↑(K i)

Tactic:
by
  let s : Subalgebra R A :=
    { __ := Subsemiring.copy _ _ (Subsemiring.coe_iSup_of_directed dir).symm
      algebraMap_mem' := fun _ ↦ Set.mem_iUnion.2
        ⟨Classical.arbitrary ι, Subalgebra.algebraMap_mem _ _⟩ }
  have : iSup K = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)
  simp [this, s]

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
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ star c * a ≠ star c * b

Tactic:
hc.star.left.ne_iff

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ a ≠ b
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
B : (i : η) → Basis (ChooseBasisIndex R (φ i)) R (φ i) := fun i ↦ chooseBasis R (φ i)
⊢ Module.rank R ((i : η) → φ i) = sum fun i ↦ Module.rank R (φ i)

Tactic:
let b : Basis _ R (∀ i, φ i) := Pi.basis fun i => B i

Goal state after:
case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
B : (i : η) → Basis (ChooseBasisIndex R (φ i)) R (φ i) := fun i ↦ chooseBasis R (φ i)
b : Basis ((j : η) × ChooseBasisIndex R (φ j)) R ((i : η) → φ i) := Pi.basis fun i ↦ B i
⊢ Module.rank R ((i : η) → φ i) = sum fun i ↦ Module.rank R (φ i)
Module: Mathlib.LinearAlgebra.Dimension.Finite

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_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
⊢ Nonempty (Fintype ι)

Tactic:
rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
    Cardinal.lt_aleph0_iff_fintype] at h

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ LinearIndependent R Subtype.val

Tactic:
convert! linearIndependent_empty R M using 2

Goal state after:
case e'_1
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ (fun x ↦ x ∈ ∅) = fun x ↦ x ∈ ∅

case e'_4
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
e_1✝ : ↥∅ = ↑∅
⊢ (fun x ↦ x ∈ ∅) = fun x ↦ x ∈ ∅
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
⊢ ⊥.toNonUnitalSubalgebra = ⊥

Tactic:
by
  ext x
  simp only [mem_bot, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra, NonUnitalAlgebra.mem_bot]

Goal state after: