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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ ↑(toNat (Module.rank R M)) = Module.rank R M

Tactic:
cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ Module.rank R M = Module.rank R M
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]

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

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

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]

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

Goal state before:
pp: case refine_1
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0

Tactic:
· rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
    simp

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

Goal state before:
pp: case refine_2
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1

Tactic:
· rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
    simp

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

Goal state before:
pp: case refine_3
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0

Tactic:
· rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
    simp

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

Goal state before:
pp: case refine_4
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
· rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
    simp

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
rw [mul_comm] at h
  rw [or_comm]
  exact mul_mem_pow _ h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
hs : s ⊆ ↑(I ⊔ J).radical
⊢ ∃ t, Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical

Tactic:
replace hs : ∀ z : s, ∃ (m : ℕ) (a b : R) (ha : a ∈ I) (hb : b ∈ J), a + b = z ^ m := by
    rintro ⟨z, hzs⟩
    simp only [Ideal.radical, Submodule.mem_sup] at hs
    obtain ⟨m, y, hyq, b, hb, hy⟩ := hs hzs
    exact ⟨m, y, b, hyq, hb, hy⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
hs : ∀ (z : ↑s), ∃ m a b, ∃ (_ : a ∈ I) (_ : b ∈ J), a + b = ↑z ^ m
⊢ ∃ t, Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j : n
M : Matrix n n α
hM : Commute (single i j 1) M
⊢ M i i = M j j

Tactic:
by
  have := ext_iff.mpr hM i j
  simp_all

Goal state after:
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.smulTower c).repr (b (i, j).1 • c (i, j).2)) (i', j') = (single (i, j) 1) (i', j')

Tactic:
Basis.smulTower_repr,

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 ((c.repr (b (i, j).1 • c (i, j).2)) (i', j').2)) (i', j').1 = (single (i, j) 1) (i', j')
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a * c - b * d ∈ carrier

Tactic:
rw [show a * c - b * d = a * (c - d) + (a - b) * d by rw [mul_sub, sub_mul]; abel]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a * (c - d) + (a - b) * d ∈ carrier
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
⊢ finrank R S ≤ finrank R T

Tactic:
by_cases H : Module.Finite R S
  · have := Module.Finite.trans (R := R) S T
    exact finrank_bot_le_finrank_of_isScalarTower R S T
  · rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
    · exact zero_le
    · rwa [← not_lt, Module.rank_lt_aleph0_iff]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (⨆ i, I i).ringCon = ⨆ i, (I i).ringCon

Tactic:
simp only [iSup, sSup_ringCon]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sSup (ringCon '' Set.range fun i ↦ I i) = sSup (Set.range fun i ↦ (I i).ringCon)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ n * (m * a) + n * m * b ∈ s

Tactic:
mul_comm n m,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ n * (m * a) + m * n * b ∈ s
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
i : ι
x : ↥(A i)
⊢ ((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) i = x

Tactic:
← coeLinearMap_of,

Goal state after:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
i : ι
x : ↥(A i)
⊢ ((LinearEquiv.ofBijective (coeLinearMap A) h).symm ((coeLinearMap A) ((of (fun i ↦ ↥(A i)) i) x))) i = x
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
i j : ι
hij : i ≠ j
x : ↥(A i)
⊢ ((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) j = 0

Tactic:
← coeLinearMap_of,

Goal state after:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
i j : ι
hij : i ≠ j
x : ↥(A i)
⊢ ((LinearEquiv.ofBijective (coeLinearMap A) h).symm ((coeLinearMap A) ((of (fun i ↦ ↥(A i)) i) x))) j = 0
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
⊢ S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : NonUnitalSubalgebra R A
⊢ S.toNonUnitalSubring = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
i : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) i = (𝒞.repr n) i • m

Tactic:
by
  simp only [equivFinsuppOfBasisRight_apply_tmul, Finsupp.mapRange_apply]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ op (star y)⁻¹ * op (star x) = (op (star y))⁻¹ * op (star x)

Tactic:
op_inv

Goal state after:
R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ (op (star y))⁻¹ * op (star x) = (op (star y))⁻¹ * op (star x)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
⊢ fromBlocks A B C D * fromBlocks A' B' C' D' =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')

Tactic:
ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp only [fromBlocks, mul_apply, of_apply,
      Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]

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

Goal state before:
pp: case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0

Tactic:
updateCol_ne hki,

Goal state after:
case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ diagonal v j k = 0
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
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
⊢ ↑sc * rb * ↑s₂ = rc * ↑sa * ↑s₁

Tactic:
← hc,

Goal state after:
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₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
⊢ ↑sc * rb * ↑s₂ = ↑sc * sb * ↑s₁
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
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
⊢ ↑sd * (rc * ↑s₂) = ↑sd * ↑sc * ↑s₃

Tactic:
← hc,

Goal state after:
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₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
⊢ ↑sd * (↑sc * ↑s₃) = ↑sd * ↑sc * ↑s₃
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
S : Set (Subfield K)
x : K
hx : x ∈ (sInf (toSubring '' S)).carrier
⊢ x⁻¹ ∈ (sInf (toSubring '' S)).carrier

Tactic:
apply Subring.mem_sInf.mpr

Goal state after:
K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
S : Set (Subfield K)
x : K
hx : x ∈ (sInf (toSubring '' S)).carrier
⊢ ∀ p ∈ toSubring '' S, x⁻¹ ∈ p
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
r r' : X
s s' : ↥S
⊢ r /ₒ s + r' /ₒ s' = (oreDenom (↑s) s' • r + oreNum (↑s) s' • r') /ₒ (oreDenom (↑s) s' * s)

Tactic:
with_unfolding_all rfl

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

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

Goal state after:
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
⊢ 0 • x✝ = 0

Tactic:
with_unfolding_all rfl

Goal state after:
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✝¹ : ℕ
x✝ : OreLocalization S X
⊢ (x✝¹ + 1) • x✝ = x✝¹ • x✝ + x✝

Tactic:
with_unfolding_all rfl

Goal state after:
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✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) = -r /ₒ s

Tactic:
with_unfolding_all rfl

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

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

Tactic:
intro r t s hst

Goal state after:
R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : t * ↑s ∈ R⁰
⊢ (if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = if hr : t • r = 0 then 0 else ↑⟨t * ↑s, hst⟩ /ₒ ⟨t • r, ⋯⟩
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

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

Tactic:
by_cases ht : t = 0

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

case neg
R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : t * ↑s ∈ R⁰
hr : ¬r = 0
ht : ¬t = 0
⊢ (if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = if hr : t • r = 0 then 0 else ↑⟨t * ↑s, hst⟩ /ₒ ⟨t • r, ⋯⟩
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
r : R
s : ↥R⁰
⊢ (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩

Tactic:
with_unfolding_all rfl

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

Goal state before:
pp: case 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
r : X
s : ↥S
⊢ 0 • (r /ₒ s) = 0

Tactic:
rw [OreLocalization.zero_def, oreDiv_smul_char 0 r 1 s 0 1 (by simp)]

Goal state after:
case 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
r : X
s : ↥S
⊢ 0 • r /ₒ (1 * 1) = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Finite ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
val✝ : Fintype ι
⊢ Free R M

Tactic:
obtain ⟨n, b⟩ : Σ n, Basis (Fin n) R M := Module.basisOfFiniteTypeTorsionFree hs

Goal state after:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Finite ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
val✝ : Fintype ι
n : ℕ
b : Basis (Fin n) R M
⊢ Free R M
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
m : Matrix ι ι (End A M)
m✝ : A
x✝¹ : ι → M
x✝ : ι
⊢ ∑ j, (m x✝ j) ((m✝ • x✝¹) j) = ((RingHom.id A) m✝ • fun i ↦ ∑ j, (m i j) (x✝¹ j)) x✝

Tactic:
simp [Finset.smul_sum]

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)
⊢ (fun i j ↦ { toFun := fun x ↦ (f * g) (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) =
    (fun i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) * fun i j ↦
      { toFun := fun x ↦ g (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext
    simp only [Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, Matrix.mul_apply,
      LinearMap.coe_sum, Finset.sum_apply]
    rw [← Fintype.sum_apply, ← map_sum]
    exact congr_arg₂ _ (by aesop) rfl

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
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : Submodule R M
inst✝ : Finite ι
b : Basis ι R M
h : finrank R ↥N = finrank R M
val✝ : Fintype ι
bM : Basis ι R M
bN : Basis (Fin (Fintype.card ι)) R ↥N
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf : ∀ (i : Fin (Fintype.card ι)), ↑(bN i) = a i • bM (f i)
e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective ⇑f ⋯
fe : ∀ (i : ι), f (e.symm i) = i
i : ι
⊢ ↑((bN.reindex e) i) = (a ∘ ⇑e.symm) i • bM i

Tactic:
simp only [snf, fe,
          Basis.coe_reindex, (· ∘ ·)]

Goal state after:
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
inst✝ : Finite R
⊢ Finite S

Tactic:
by
  have : Function.Surjective (Function.uncurry (mk' (M := M) S)) := fun x ↦ by
    simpa using IsLocalization.exists_mk'_eq M x
  exact .of_surjective _ this

Goal state after:
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
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ f = ↑(algEquiv M S Q)

Tactic:
apply IsLocalization.ringHom_ext M; rw [hf]; ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ (RingHom.id S) x = x

pp: R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ ∀ (x : R), (RingHom.id S) ((algebraMap R S) x) = (algebraMap R S) (((↑h.symm).comp ↑h) x)

Tactic:
RingHom.id_apply

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)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ x = x

R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ ∀ (x : R), (RingHom.id S) ((algebraMap R S) x) = (algebraMap R S) (((↑h.symm).comp ↑h) x)