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

Goal state before:
pp: 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) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).1 =
    ↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).1

Tactic:
dsimp

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))
          ((selfAdjoint.submodule R A).subtype x + (skewAdjoint.submodule R A).subtype 0)).1 =
    ↑x
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: 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) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).2 =
    ↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).2

Tactic:
dsimp

Goal state after:
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))
          ((selfAdjoint.submodule R A).subtype x + (skewAdjoint.submodule R A).subtype 0)).2 =
    0
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: 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) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).1 =
    ↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).1

Tactic:
dsimp

Goal state after:
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))
          ((selfAdjoint.submodule R A).subtype 0 + (skewAdjoint.submodule R A).subtype x)).1 =
    0
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: 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) ∘ₗ
              (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ∘ₗ
            LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A))
          x).2 =
    ↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A)) x).2

Tactic:
dsimp

Goal state after:
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))
          ((selfAdjoint.submodule R A).subtype 0 + (skewAdjoint.submodule R A).subtype 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).submatrix Sum.swap f (Sum.inl val✝) j = (fromBlocks C D A B).submatrix id f (Sum.inl val✝) j

Tactic:
dsimp

Goal state after:
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)
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).submatrix Sum.swap f (Sum.inr val✝) j = (fromBlocks C D A B).submatrix id f (Sum.inr val✝) j

Tactic:
dsimp

Goal state after:
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)
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 → n ⊕ o
i : p
val✝ : m
⊢ (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inl val✝) = (fromBlocks B A D C).submatrix f id i (Sum.inl val✝)

Tactic:
dsimp

Goal state after:
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 → n ⊕ o
i : p
val✝ : m
⊢ fromBlocks A B C D (f i) (Sum.inr val✝) = fromBlocks B A D C (f i) (Sum.inl 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 → n ⊕ o
i : p
val✝ : l
⊢ (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inr val✝) = (fromBlocks B A D C).submatrix f id i (Sum.inr val✝)

Tactic:
dsimp

Goal state after:
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 → n ⊕ o
i : p
val✝ : l
⊢ fromBlocks A B C D (f i) (Sum.inl val✝) = fromBlocks B A D C (f i) (Sum.inr val✝)
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
⊢ v ᵥ* B.updateCol j r = Function.update (v ᵥ* B) j (v ⬝ᵥ r)

Tactic:
ext j'

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
j' : n
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (v ᵥ* B) j (v ⬝ᵥ r) j'
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
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
⊢ (diagonal d).blockDiag' k i i = diagonal (fun i ↦ d ⟨k, i⟩) i i

Tactic:
blockDiag'_apply,

Goal state after:
case inl
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
⊢ diagonal d ⟨k, i⟩ ⟨k, i⟩ = diagonal (fun i ↦ d ⟨k, i⟩) i i
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
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
⊢ (diagonal d).blockDiag' k i j = diagonal (fun i ↦ d ⟨k, i⟩) i j

Tactic:
blockDiag'_apply,

Goal state after:
case inr
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
⊢ diagonal d ⟨k, i⟩ ⟨k, j⟩ = diagonal (fun i ↦ d ⟨k, i⟩) i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
⊢ (of (vecCons v A))ᵀ = of fun i ↦ vecCons (v i) (Aᵀ i)

Tactic:
by
  ext i j
  refine Fin.cases ?_ ?_ j <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = (b.repr 0) i

Tactic:
rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = (b.repr 0) i
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = (b.repr 0) i

Tactic:
rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = (b.repr 0) i
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_2.«0»
α : Type u_1
x y : α
h : x ≠ y
b : Fin (Nat.succ 0).succ
h' : ![x, y] ((fun i ↦ i) ⟨0, ⋯⟩) = ![x, y] b
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = b

Tactic:
fin_cases b

Goal state after:
case refine_2.«0».«0»
α : Type u_1
x y : α
h : x ≠ y
h' : ![x, y] ((fun i ↦ i) ⟨0, ⋯⟩) = ![x, y] ((fun i ↦ i) ⟨0, ⋯⟩)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩

case refine_2.«0».«1»
α : Type u_1
x y : α
h : x ≠ y
h' : ![x, y] ((fun i ↦ i) ⟨0, ⋯⟩) = ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_2.«1»
α : Type u_1
x y : α
h : x ≠ y
b : Fin (Nat.succ 0).succ
h' : ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩) = ![x, y] b
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = b

Tactic:
fin_cases b

Goal state after:
case refine_2.«1».«0»
α : Type u_1
x y : α
h : x ≠ y
h' : ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩) = ![x, y] ((fun i ↦ i) ⟨0, ⋯⟩)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩

case refine_2.«1».«1»
α : Type u_1
x y : α
h : x ≠ y
h' : ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩) = ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: 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
⊢ a ∈ ⊤

Tactic:
exact mem_top _

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

Goal state before:
pp: 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 : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
⊢ b ∈ ⊤

Tactic:
exact mem_top _

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
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : n r = 0
⊢ False

Tactic:
· obtain rfl : b = 1 := by simpa [h, Finset.prod_eq_one hr'.2] using hn
      simp at hb

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization S R
⊢ 0 * x = 0

Tactic:
induction x using OreLocalization.ind with

Goal state after:
case c
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ 0 * (r /ₒ s) = 0
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization S R
⊢ x * 0 = 0

Tactic:
induction x using OreLocalization.ind with

Goal state after:
case c
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * 0 = 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
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
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
⊢ add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂ = add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂

Tactic:
dsimp at *

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : K
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
by
  let s : Subfield K :=
    { __ := Subring.copy _ _ (Subring.coe_iSup_of_directed hS).symm
      inv_mem' := fun _ hx ↦ have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
        Set.mem_iUnion.mpr ⟨i, (S i).inv_mem hi⟩ }
  have : iSup S = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set K)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
  exact this ▸ Set.mem_iUnion

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ (numeratorRingHom.comp (algebraMap R₀ R)) r * x = x * (numeratorRingHom.comp (algebraMap R₀ R)) r

Tactic:
induction x using OreLocalization.ind with

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₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
⊢ (numeratorRingHom.comp (algebraMap R₀ R)) r * (r₁ /ₒ s₁) = r₁ /ₒ s₁ * (numeratorRingHom.comp (algebraMap R₀ R)) r
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₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
⊢ (numeratorRingHom.comp (algebraMap R₀ R)) r * (r₁ /ₒ s₁) = r₁ /ₒ s₁ * (numeratorRingHom.comp (algebraMap R₀ R)) r

Tactic:
dsimp

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₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
⊢ (algebraMap R₀ R) r /ₒ 1 * (r₁ /ₒ s₁) = r₁ /ₒ s₁ * ((algebraMap R₀ R) r /ₒ 1)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ r • x = (numeratorRingHom.comp (algebraMap R₀ R)) r * x

Tactic:
dsimp

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
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ r • x = (algebraMap R₀ R) r /ₒ 1 * x
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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : ι
hi : i ∉ range ⇑snf.f
⊢ (snf.bM.repr ↑m) i = 0

Tactic:
by
  obtain ⟨m, hm⟩ := m
  obtain ⟨c, rfl⟩ := snf.bN.mem_submodule_iff.mp hm
  replace hi : ∀ j, snf.f j ≠ i := by simpa using hi
  simp [hi, snf.snf, map_finsuppSum]

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

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : 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)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x✝ : A
⊢ (ringEquivOfRingEquiv S Q h.toRingEquiv H).toFun ((algebraMap A S) x✝) = (algebraMap A Q) x✝

Tactic:
dsimp

Goal state after:
R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : 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)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x✝ : A
⊢ (map Q ↑h ⋯) ((algebraMap A S) x✝) = (algebraMap A Q) x✝
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ (↑((toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg)).toFun (x + y) =
    (↑((toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg)).toFun x +
      (↑((toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg)).toFun y

Tactic:
dsimp

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ ((toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg) (x + y) =
    ((toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg) x +
      ((toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg) y
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial (R ⧸ I)
x : M
⊢ ∃ a, ψ a = ϕ x

Tactic:
obtain ⟨y, hy⟩ := hϕ 1

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial (R ⧸ I)
x y : M
hy : ϕ y = 1
⊢ ∃ a, ψ a = ϕ x
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : StarMul α
s t : Set α
⊢ star '' image2 (fun x1 x2 ↦ x1 * x2) s t = image2 (fun x1 x2 ↦ x1 * x2) (star '' t) (star '' s)

Tactic:
image_image2,

Goal state after:
α : Type u_1
inst✝¹ : Mul α
inst✝ : StarMul α
s t : Set α
⊢ image2 (fun a b ↦ (a * b)⋆) s t = image2 (fun x1 x2 ↦ x1 * x2) (star '' t) (star '' s)
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
s t : Set α
⊢ star '' image2 (fun x1 x2 ↦ x1 + x2) s t = image2 (fun x1 x2 ↦ x1 + x2) (star '' s) (star '' t)

Tactic:
image_image2,

Goal state after:
α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
s t : Set α
⊢ image2 (fun a b ↦ (a + b)⋆) s t = image2 (fun x1 x2 ↦ x1 + x2) (star '' s) (star '' t)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case tmul.tmul
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
a' : A
b' : B
⊢ r • a' ⊗ₜ[R] b' * a ⊗ₜ[R] b = r • (a' ⊗ₜ[R] b' * a ⊗ₜ[R] b)

Tactic:
dsimp

Goal state after:
case tmul.tmul
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
a' : A
b' : B
⊢ r • a' ⊗ₜ[R] b' * a ⊗ₜ[R] b = r • (a' * a) ⊗ₜ[R] (b' * b)