mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : f.symm i ≠ i'
⊢ single i j r (f i') (g j') = single (f.symm i) (g.symm j) r i' j'

Tactic:
rw [single_apply_of_row_ne hi, single_apply_of_row_ne]
    exact f.symm_apply_eq.not.1 hi

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ (M - M') * N = M * N - M' * N

Tactic:
rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]

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:
simpa using fun r ↦ congr($(hx (single i i r)) i i)

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y = a
⊢ a = y

Tactic:
exact hy.symm

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

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ toNat (Module.rank F K) * toNat (Module.rank K A) = toNat (Module.rank F A)

Tactic:
rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
    lift_rank_mul_lift_rank, toNat_lift]

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

Goal state before:
pp: case inl
R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : OrzechProperty R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
h : finrank R M ≤ finrank R M'
h✝ : Subsingleton R
⊢ Bijective ⇑f

pp: case inr
R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : OrzechProperty R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
h : finrank R M ≤ finrank R M'
h✝ : Nontrivial R
⊢ Bijective ⇑f

Tactic:
· have := Module.subsingleton R M
    exact ⟨Function.injective_of_subsingleton f, hf⟩

Goal state after:
case inr
R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : OrzechProperty R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
h : finrank R M ≤ finrank R M'
h✝ : Nontrivial R
⊢ Bijective ⇑f
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Subring R
i✝ : ℤ
i : ℕ
ih : (algebraMap ℤ R) (-↑i) ∈ S.carrier
⊢ ↑(-↑i - 1) ∈ S

Tactic:
rw [Int.cast_sub, Int.cast_one]
          exact S.sub_mem ih S.one_mem

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

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
ϕ ψ : A →ₐ[R] B
x : R
⊢ (algebraMap R A) x ∈ {a | ϕ a = ψ a}

Tactic:
simp only [Set.mem_ofPred_eq, AlgHomClass.commutes]

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

Goal state before:
pp: case inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')

Tactic:
rw [single_apply_of_row_ne hi,
      single_apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
⊢ (blockDiagonal M)ᵀ = blockDiagonal fun k ↦ (M k)ᵀ

Tactic:
by
  ext
  simp only [transpose_apply, blockDiagonal_apply, eq_comm]
  split_ifs with h
  · rw [h]
  · rfl

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq l
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
i : l
r : m → α
j : n
c : m → α
⊢ (updateCol 0 j (0 *ᵥ c)).updateRow i (Function.update (r ᵥ* 0) j (r ⬝ᵥ c)) = of (Pi.single i (Pi.single j (r ⬝ᵥ c)))

Tactic:
vecMul_zero,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq l
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
i : l
r : m → α
j : n
c : m → α
⊢ (updateCol 0 j (0 *ᵥ c)).updateRow i (Function.update 0 j (r ⬝ᵥ c)) = of (Pi.single i (Pi.single j (r ⬝ᵥ c)))
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : ⟨k, i⟩ = ⟨k, j⟩
⊢ i = j

Tactic:
cases h

Goal state after:
case refl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
hij : i ≠ i
⊢ i = i
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ (A * B).toBlock p q i k = (A.toBlock p ⊤ * B.toBlock ⊤ q) i k

Tactic:
simp only [toBlock_apply, mul_apply]

Goal state after:
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∑ j, A (↑i) j * B j ↑k = ∑ j, A ↑i ↑j * B ↑j ↑k
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // r a }
⊢ (A * B).toBlock p r i k =
    (A.toBlock p q * B.toBlock q r + (A.toBlock p fun i ↦ ¬q i) * B.toBlock (fun i ↦ ¬q i) r) i k

Tactic:
simp only [toBlock_apply, mul_apply]

Goal state after:
R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // r a }
⊢ ∑ j, A (↑i) j * B j ↑k = (A.toBlock p q * B.toBlock q r + (A.toBlock p fun i ↦ ¬q i) * B.toBlock (fun i ↦ ¬q i) r) i k
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ d ∈ ψ'.submoduleImage N

Tactic:
LinearMap.mem_submoduleImage_of_le hNO

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ ∃ y, ∃ (yN : y ∈ N), ψ' ⟨y, ⋯⟩ = d
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✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : ↑sb * ↑(r₂, s₂).snd = rb * ↑(r₁, s₁).snd
⊢ add' (r₁, s₁).fst (r₁, s₁).snd x = add' (r₂, s₂).fst (r₂, s₂).snd x

Tactic:
induction x with | _ r₃ s₃
       =>  _ 

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : ↑sb * ↑(r₂, s₂).snd = rb * ↑(r₁, s₁).snd
r₃ : X
s₃ : ↥S
⊢ add' (r₁, s₁).fst (r₁, s₁).snd (r₃ /ₒ s₃) = add' (r₂, s₂).fst (r₂, s₂).snd (r₃ /ₒ s₃)
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
⊢ IsGLB S (sInf S)

Tactic:
have : ∀ {s t : Subfield K}, (s : Set K) ≤ t ↔ s ≤ t := by simp [SetLike.coe_subset_coe]
  refine IsGLB.of_image this ?_
  convert! isGLB_biInf (s := S) (f := SetLike.coe)
  exact coe_sInf _

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
⊢ ∀ x ∈ {x | ∃ (hx : x ∈ closure s), p x hx}, x⁻¹ ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
by rintro _ ⟨_, hx⟩; exact ⟨_, inv _ _ hx⟩

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
M : Matrix m n R
⊢ (fun f ↦ of fun i j ↦ f (Pi.single j 1) i) M.mulVecLin = M

Tactic:
ext i j
    simp only [Matrix.mulVec_single_one, col_apply, Matrix.mulVecLin_apply, of_apply]

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
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
⊢ (universalMulHom (↑f) fS ⋯) 0 = 0

Tactic:
rw [OreLocalization.zero_def, universalMulHom_apply]

Goal state after:
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)
⊢ ↑(fS 1)⁻¹ * ↑f 0 = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty ↥⊥)
⊢ n = 0

Tactic:
by simpa using Fintype.card_eq.mpr ⟨e⟩

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

Goal state before:
pp: case c.c.e_a.e_a
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
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
h₃' : s₃ * s₁ = ⟨r₃ * ↑s₂, ⋯⟩
⊢ f r₃ * f ↑s₂ = f ↑⟨r₃ * ↑s₂, ⋯⟩

Tactic:
simp only [map_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : ↑u * r₂ - ↑u * r₁ = 0
h₂ : ↑u = v
⊢ r₁ = r₂

Tactic:
← mul_sub

Goal state after:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : ↑u * (r₂ - r₁) = 0
h₂ : ↑u = v
⊢ r₁ = r₂
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case right
ι : 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
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := ⋯
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := ⋯
_sI : ↑I → ↥N := ⋯
sI_basis : Basis (↑I) R ↥N := ⋯
i : ι
hi : i ∈ I
⊢ 1 • s i ∈ N

Tactic:
one_smul

Goal state after:
case right
ι : 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
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
i : ι
hi : i ∈ I
⊢ s i ∈ N
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x * IsFractionRing.inv A x = 1

Tactic:
by
  rw [IsFractionRing.inv, dif_neg hx, ←
    IsUnit.mul_left_inj
      (map_units K
        ⟨(sec _ x).1,
          mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
            hx <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) x) h0⟩),
    one_mul, mul_assoc]
  rw [mk'_spec, ← eq_mk'_iff_mul_eq]
  exact (mk'_sec _ x).symm

Goal state after:
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
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
x✝ : L
⊢ x✝ ∈ Subfield.closure ↑(Subring.closure s) ↔ x✝ ∈ Subfield.closure s

Tactic:
simp_rw [Subfield.mem_closure_iff, Subring.closure_eq]

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
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:
simp [Algebra.smul_def]

Goal state after:
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:
simp [Algebra.smul_def]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
this✝ : Semiring α := e.semiring
this : SMul R α := Equiv.smul R e
r : R
x : α
⊢ e.symm (r • e x) = e.symm (e (e.symm ((algebraMap R β) r)) * e x)

Tactic:
simp [Algebra.smul_def]

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

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

Tactic:
let add := e.add

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

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

Tactic:
let add := e.add

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

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

Tactic:
let add := e.add

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

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

Tactic:
let add := e.add

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

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

Tactic:
let add := e.add

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

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

Tactic:
let add := e.add

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
⊢ NonUnitalCommRing α
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
s : Set R
h : ∀ a ∈ s, star a ∈ s
ha : a ∈ s.centralizer
y : R
hy : y ∈ s
⊢ y * star a = star a * y

Tactic:
by simpa using congr_arg star (ha _ (h _ hy)).symm

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 1 = σ (1 • 1)

Tactic:
one_smul

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 1 = σ 1
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:
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) = x • 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)

Tactic:
simp [Algebra.smul_def]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
R' : Type u_6
S' : Type u_7
T' : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : CommSemiring R'
inst✝³ : CommSemiring S'
inst✝² : CommSemiring T'
inst✝¹ : Algebra R' S'
inst✝ : Algebra R' T'
fR : R →+* R'
fS : S →+* S'
fT : T →+* T'
HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR
HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR
s : S
t : T
⊢ (mapRingHom fR fS fT HS HT) (s ⊗ₜ[R] t) = fS s ⊗ₜ[R'] fT t

Tactic:
by
  trans (fS s * 1 : S') ⊗ₜ[R'] (1 * fT t : T')
  · dsimp [mapRingHom, lift_tmul, algebraMap]
  · simp

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
r : R
hr : IsUnit r
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔ ∃ i, ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))

pp: case neg
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
r : R
hr : ¬IsUnit r
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔ ∃ i, ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))

Tactic:
· lift r to Rˣ using hr with r' hr'
    simp [isQuasiregular_pi_iff]

Goal state after:
case neg
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
r : R
hr : ¬IsUnit r
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔ ∃ i, ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
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 < star y ↔ x < y

Tactic:
by_cases h : x = y

Goal state after:
case pos
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : x = y
⊢ star x < star y ↔ x < y

case neg
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : ¬x = y
⊢ star x < star y ↔ x < y
Module: Mathlib.LinearAlgebra.Dimension.Constructions

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

Tactic:
← bs.mk_eq_rank'',

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