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

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
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ (f i) x = (f i) x

pp: case h
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
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ ↑(K i) ⊆ ↑(iSup K)

Tactic:
]

Goal state after:
case h
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
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ ↑(K i) ⊆ ↑(iSup K)
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ x
⊢ 0 ≤ x

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ x
⊢ 0 ≤ x
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ (∃ p ∈ AddSubmonoid.comap opAddEquiv (AddSubmonoid.map opAddEquiv (AddSubmonoid.closure (range fun s ↦ star s * s))),
      unop y = unop x + p) ↔
    ∃ x_1, op x_1 ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + op x_1

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ (∃ p ∈ AddSubmonoid.comap opAddEquiv (AddSubmonoid.map opAddEquiv (AddSubmonoid.closure (range fun s ↦ star s * s))),
      unop y = unop x + p) ↔
    ∃ x_1, op x_1 ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + op x_1
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] ↥(centralizer R S)
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A))
      ((Algebra.TensorProduct.comm R A ↥(centralizer R S)) x) =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A))
      ((Algebra.TensorProduct.comm R A ↥(centralizer R S)) x)

Tactic:
]

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

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
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ (f i) x = (f i) x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : a ≤ b
⊢ r • a ≤ r • b

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : a ≤ b
⊢ r • a ≤ r • b
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), b = a + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), r • b = r • a + p

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), b = a + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), r • b = r • a + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : r ≤ s
⊢ r • a ≤ s • a

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : r ≤ s
⊢ r • a ≤ s • a
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), s = r + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), s • a = r • a + p

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), s = r + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), s • a = r • a + p
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

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
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ (f ?i) ⟨↑(Set.inclusion hT x), ?hx⟩ = (f i) ⟨↑x, hx⟩

pp: case i
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
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ ι

pp: case hx
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
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ ↑(Set.inclusion hT x) ∈ ↑(K ?i)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : a < b
⊢ r • a < r • b

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : a < b
⊢ r • a < r • b
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ b = a + p
⊢ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ r • b = r • a + p

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ b = a + p
⊢ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ r • b = r • a + p
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a ↦ a • g i) ∈ span R (range fun x ↦ ↑(f x))
h₂ : (c.sum fun i a ↦ a • g i) ∈ span R (range g)
this : (c.sum fun a b ↦ b • Submodule.Quotient.mk (g a)) = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁵ : Semiring R
inst✝¹⁴ : PartialOrder R
inst✝¹³ : StarRing R
inst✝¹² : StarOrderedRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : Module R A
inst✝⁶ : StarModule R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : r < s
⊢ r • a < s • a

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁵ : Semiring R
inst✝¹⁴ : PartialOrder R
inst✝¹³ : StarRing R
inst✝¹² : StarOrderedRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : Module R A
inst✝⁶ : StarModule R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : r < s
⊢ r • a < s • a
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁵ : Semiring R
inst✝¹⁴ : PartialOrder R
inst✝¹³ : StarRing R
inst✝¹² : StarOrderedRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : Module R A
inst✝⁶ : StarModule R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ s = r + p
⊢ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ s • a = r • a + p

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁵ : Semiring R
inst✝¹⁴ : PartialOrder R
inst✝¹³ : StarRing R
inst✝¹² : StarOrderedRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : Module R A
inst✝⁶ : StarModule R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ s = r + p
⊢ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ s • a = r • a + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), f y = f x + p

Tactic:
]

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), f y = f x + p
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (⇑M'.mkQ) t
⊢ LinearIndepOn R (⇑(span R s).mkQ ∘ id) t

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (⇑M'.mkQ) t
⊢ LinearIndepOn R (⇑(span R s).mkQ ∘ id) t
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case e'_3.mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
y : ↥(centralizer R S) ⊗[R] A
hy : (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y = (Algebra.TensorProduct.comm R A B) x
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y

Tactic:
]

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁹ : NonUnitalSemiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : NonUnitalSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : StarRing S
inst✝² : StarOrderedRing S
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
h : f x ≤ f y
f_inv : S →⋆ₙ+* R := ↑(↑f).symm
f_inv_f : ∀ (r : R), f_inv (f r) = r
⊢ f_inv (f x) ≤ f_inv (f y)

Tactic:
]

Goal state after:
R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁹ : NonUnitalSemiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : NonUnitalSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : StarRing S
inst✝² : StarOrderedRing S
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
h : f x ≤ f y
f_inv : S →⋆ₙ+* R := ↑(↑f).symm
f_inv_f : ∀ (r : R), f_inv (f r) = r
⊢ f_inv (f x) ≤ f_inv (f y)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
⊢ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t ↔ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t

Tactic:
]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R M

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R M
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
⊢ centralizer R ↑includeLeft.range = centralizer R ↑(map includeLeft ⊤)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
⊢ centralizer R ↑includeLeft.range = centralizer R ↑(map includeLeft ⊤)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R (M × M₁)

Tactic:
]

Goal state after:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R (M × M₁)
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = centralizer R ↑(map includeRight ⊤)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = centralizer R ↑(map includeRight ⊤)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Nontrivial R
⊢ Module.rank R (ULift.{v', v} M) + Module.rank R (ULift.{v, v'} M') ≤ Module.rank R (M × M')

Tactic:
]

Goal state after:
R : Type u
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Nontrivial R
⊢ Module.rank R (ULift.{v', v} M) + Module.rank R (ULift.{v, v'} M') ≤ Module.rank R (M × M')
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
⊢ centralizer R ↑(Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range = centralizer R ↑includeLeft.range

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
⊢ centralizer R ↑(Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range = centralizer R ↑includeLeft.range
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range =
    centralizer R ↑includeRight.range

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range =
    centralizer R ↑includeRight.range
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
⊢ lift.{v, w} #ι * lift.{w, v} #fst✝ = lift.{v, w} #ι * lift.{w, v} #fst✝

Tactic:
]

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

Goal state before:
pp: case intro.intro
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
I : Type v
b : Basis I R M
⊢ #(m × n × I) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)

Tactic:
]

Goal state after:
case intro.intro
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
I : Type v
b : Basis I R M
⊢ #(m × n × I) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)