mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ ⋃₀ (SetLike.coe '' S)) =
    Subsemiring.closure (⋃₀ (SetLike.coe '' S))

Tactic:
congr 1

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ Set.range ⇑(algebraMap R A) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
x y : (ι →₀ M) ⊗[R] N
hx : ((finsuppLeft R S M N ι) x) i = (rTensor N (Finsupp.lapply i)) x
hy : ((finsuppLeft R S M N ι) y) i = (rTensor N (Finsupp.lapply i)) y
⊢ ((finsuppLeft R S M N ι) (x + y)) i = (rTensor N (Finsupp.lapply i)) (x + y)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
x y : M ⊗[R] (ι →₀ N)
hx : ((finsuppRight R S M N ι) x) i = (lTensor M (Finsupp.lapply i)) x
hy : ((finsuppRight R S M N ι) y) i = (lTensor M (Finsupp.lapply i)) y
⊢ ((finsuppRight R S M N ι) (x + y)) i = (lTensor M (Finsupp.lapply i)) (x + y)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case single
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] g k

Tactic:
induction g using Finsupp.induction_linear with
    | zero => simp
    | add g₁ g₂ hg₁ hg₂ => simp [tmul_add, hg₁, hg₂]
    | single k' n =>
      classical
      simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp

Goal state after:
Module: Mathlib.Algebra.Field.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ unop ↑q = unop (↑q.num / ↑q.den)

Tactic:
by rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
    unop_intCast, div_eq_mul_inv]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
⊢ (selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ
      (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype =
    LinearMap.id

Tactic:
ext x <;> dsimp <;> erw [Submodule.coe_subtype, Submodule.coe_subtype]

Goal state after:
case hl.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).1 = ↑x

case hl.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).2 = 0

case hr.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).1 = 0

case hr.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).2 = ↑x
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (f j) = fromBlocks C D A B (Sum.inl val✝) (f j)

Tactic:
cases f j

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : l
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks C D A B (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : m
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks C D A B (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (f j) = fromBlocks C D A B (Sum.inr val✝) (f j)

Tactic:
cases f j

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : l
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks C D A B (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks C D A B (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
updateCol_ne h,

Goal state after:
case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M i j' = if j' = j then c i else M i j'
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0

Tactic:
congr 1

Goal state after:
case e_c
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (k = k' ∧ i = j) = (i = j ∧ k = k')
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: case tmul.add
R : Type uR
A : Type uA
N : Type uN
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : A
x y : A ⊗[R] N
hx : (cancelBaseChange R A A A N) (b ⊗ₜ[A] x) = (TensorProduct.lid A (A ⊗[R] N)) (b ⊗ₜ[A] x)
hy : (cancelBaseChange R A A A N) (b ⊗ₜ[A] y) = (TensorProduct.lid A (A ⊗[R] N)) (b ⊗ₜ[A] y)
⊢ (cancelBaseChange R A A A N) (b ⊗ₜ[A] (x + y)) = (TensorProduct.lid A (A ⊗[R] N)) (b ⊗ₜ[A] (x + y))

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case add
R : Type uR
A : Type uA
N : Type uN
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : A ⊗[A] (A ⊗[R] N)
hx : (cancelBaseChange R A A A N) x = (TensorProduct.lid A (A ⊗[R] N)) x
hy : (cancelBaseChange R A A A N) y = (TensorProduct.lid A (A ⊗[R] N)) y
⊢ (cancelBaseChange R A A A N) (x + y) = (TensorProduct.lid A (A ⊗[R] N)) (x + y)

Tactic:
| add x y hx hy =>

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
⊢ False

Tactic:
have hr' : r = r ^ (m r + n r) * (∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s := by
    rwa [pow_add, mul_assoc, mul_assoc, ← mul_assoc (r ^ n r), mul_comm (r ^ n r) _, mul_assoc,
      ← hn, ← mul_assoc, ← hm]

Goal state after:
case inr
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
⊢ False
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
⊢ p (1 + -1) ⋯

Tactic:
exact add _ _ _ _ one (neg _ _ one)

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

Goal state before:
pp: case pos
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : ¬dx = 0
hy0 : dy = 0
⊢ nx / dx + 0 ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}

Tactic:
add_zero

Goal state after:
case pos
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : ¬dx = 0
hy0 : dy = 0
⊢ nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
S : Submonoid M
p : Type u_4
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
⊢ liftOn 0 f H = f 0 1

Tactic:
← mk_zero 1,

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
S : Submonoid M
p : Type u_4
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
⊢ (mk 0 1).liftOn f H = f 0 1
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
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * f r₁ + ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f r₃ * f r₂) = ↑(fS s₁)⁻¹ * f r₁ + ↑(fS s₂)⁻¹ * f r₂

Tactic:
congr 1

Goal state after:
case c.c.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₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f r₃ * f r₂) = ↑(fS s₂)⁻¹ * f r₂
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.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₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ * f r₂ = ↑(fS s₂)⁻¹ * f r₂

Tactic:
congr 1

Goal state after:
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₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ = ↑(fS s₂)⁻¹
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₃ * ↑(fS s₂) = ↑(fS ⟨r₃ * ↑s₂, ⋯⟩)

Tactic:
← hf,

Goal state after:
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₂ = ↑(fS ⟨r₃ * ↑s₂, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
r : R
i✝ j✝ : m
⊢ Matrix.diagonal (fun x ↦ r) i✝ j✝ = (algebraMap R (Matrix m m R)) r i✝ j✝

Tactic:
algebraMap_eq_diagonal,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
r : R
i✝ j✝ : m
⊢ Matrix.diagonal (fun x ↦ r) i✝ j✝ = Matrix.diagonal ((algebraMap R (m → R)) r) i✝ 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
⊢ (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₁

Tactic:
mul_comm (_ * _),

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₁ * ((algebraMap R S) ↑(y₁ * y₂) * mk' S x₂ y₂) =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case map_units
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ (y : ↥(Submonoid.map h M)), IsUnit ((algebraMap P S) ↑y)

Tactic:
rintro ⟨_, ⟨y, hy, rfl⟩⟩

Goal state after:
case map_units
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : R
hy : y ∈ ↑M
⊢ IsUnit ((algebraMap P S) ↑⟨h y, ⋯⟩)
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x y : TensorProduct R A M
hx : x ∈ Submodule.span A ↑(Finset.image (⇑((TensorProduct.mk R A M) 1)) s)
hy : y ∈ Submodule.span A ↑(Finset.image (⇑((TensorProduct.mk R A M) 1)) s)
⊢ x + y ∈ Submodule.span A ↑(Finset.image (⇑((TensorProduct.mk R A M) 1)) s)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
add✝ : Add α := e.add
mul✝ : Mul α := e.mul
x y : α
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
by
        simp [mul_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ Semiring α

Tactic:
let npow := e.pow ℕ

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Semiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ CommSemiring α

Tactic:
let npow := e.pow ℕ

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
⊢ Ring α

Tactic:
let npow := e.pow ℕ

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Ring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
⊢ CommRing α

Tactic:
let npow := e.pow ℕ

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommRing α
Module: Mathlib.RingTheory.TensorProduct.Basic

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✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ ↑(n + 1) ⊗ₜ[R] 1 = ↑n ⊗ₜ[R] 1 + 1

Tactic:
simp [add_tmul, one_def]

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

Goal state before:
pp: case tmul.add
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass R S A
r : S
a : A
b : B
x y : A ⊗[R] B
hx : r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)
hy : r • y * a ⊗ₜ[R] b = r • (y * a ⊗ₜ[R] b)
⊢ r • (x + y) * a ⊗ₜ[R] b = r • ((x + y) * a ⊗ₜ[R] b)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case add
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass R S A
r : S
x✝ x y : A ⊗[R] B
hx : r • x✝ * x = r • (x✝ * x)
hy : r • x✝ * y = r • (x✝ * y)
⊢ r • x✝ * (x + y) = r • (x✝ * (x + y))

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case tmul.add
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
a : A
b : B
x y : A ⊗[R] B
hx : r • (x * a ⊗ₜ[R] b) = x * r • a ⊗ₜ[R] b
hy : r • (y * a ⊗ₜ[R] b) = y * r • a ⊗ₜ[R] b
⊢ r • ((x + y) * a ⊗ₜ[R] b) = (x + y) * r • a ⊗ₜ[R] b

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case add
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
x✝ x y : A ⊗[R] B
hx : r • (x✝ * x) = x✝ * r • x
hy : r • (x✝ * y) = x✝ * r • y
⊢ r • (x✝ * (x + y)) = x✝ * r • (x + y)

Tactic:
| add x y hx hy =>

Goal state after:
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
inst✝ : Subsingleton A
a : A
⊢ {r | IsUnit (↑ₐ r - a)} = univ

Tactic:
Subsingleton.elim (algebraMap R A _ - a) 1,

Goal state after:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ {r | IsUnit 1} = univ
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
k : 𝕜
⊢ {k + 0} = {k}

Tactic:
add_zero

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
⊢ {k} = {k}