mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
K✝ : Type u_5
inst✝⁸ : IsDomain A
k : Type u_6
K : Type u_7
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A k
inst✝⁴ : Algebra A K
inst✝³ : Algebra k K
inst✝² : FaithfulSMul A k
inst✝¹ : FaithfulSMul A K
inst✝ : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x✝ : A × ↥A⁰
a₁ : A
a₂ : ↥A⁰
⊢ (Localization.mk (a₁, a₂).1 (a₁, a₂).2 • b) • c = Localization.mk (a₁, a₂).1 (a₁, a₂).2 • b • c

Tactic:
by
    rw [← smul_right_inj (nonZeroDivisors.coe_ne_zero a₂)]
    simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
      IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (N ⊗[R] M)
hs : s.Finite
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
⊢ ∃ J, ∃ (_ : J.FG), s ⊆ ↑(rTensor M J.subtype).range

Tactic:
← Set.finite_coe_iff

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
⊢ ∃ J, ∃ (_ : J.FG), s ⊆ ↑(rTensor M J.subtype).range
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
s : Set (↥I ⊗[R] M)
hs : s.Finite
J : ↥I ⊗[R] M → Submodule R N
fg : ∀ (x : ↥I ⊗[R] M), (J x).FG
hle : ∀ (x : ↥I ⊗[R] M), J x ≤ I
y : (x : ↥I ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : ↥I ⊗[R] M), x = (rTensor M (inclusion ⋯)) (y x)
⊢ ∃ J, ∃ (_ : J.FG) (hle : J ≤ I), s ⊆ ↑(rTensor M (inclusion hle)).range

Tactic:
← Set.finite_coe_iff

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
s : Set (↥I ⊗[R] M)
hs : Finite ↑s
J : ↥I ⊗[R] M → Submodule R N
fg : ∀ (x : ↥I ⊗[R] M), (J x).FG
hle : ∀ (x : ↥I ⊗[R] M), J x ≤ I
y : (x : ↥I ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : ↥I ⊗[R] M), x = (rTensor M (inclusion ⋯)) (y x)
⊢ ∃ J, ∃ (_ : J.FG) (hle : J ≤ I), s ⊆ ↑(rTensor M (inclusion hle)).range
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: 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 : TensorProduct R A M
⊢ x ∈ Submodule.span A ↑(Finset.image (⇑((TensorProduct.mk R A M) 1)) s)

Tactic:
induction x with
    | zero => exact zero_mem _
    | tmul x y =>
      rw [Finset.coe_image, ← Submodule.span_span_of_tower R, Submodule.span_image, hs,
        Submodule.map_top, LinearMap.coe_range, ← mul_one x, ← smul_eq_mul,
        ← TensorProduct.smul_tmul']
      exact Submodule.smul_mem _ x (Submodule.subset_span <| Set.mem_range_self y)
    | add x y hx hy => exact Submodule.add_mem _ hx hy

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

Goal state before:
pp: case inr
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
⊢ Surjective ⇑(algebraMap R A)

Tactic:
have : Subsingleton ((A ⧸ R') ⊗[R] (A ⧸ R')) := by
    refine subsingleton_of_forall_eq 0 fun y ↦ ?_
    induction y with
    | zero => rfl
    | add a b e₁ e₂ => rwa [e₁, zero_add]
    | tmul x y =>
      obtain ⟨x, rfl⟩ := R'.mkQ_surjective x
      obtain ⟨y, rfl⟩ := R'.mkQ_surjective y
      obtain ⟨s, hs⟩ : ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y := by
        use x * y
        trans x ⊗ₜ 1 * 1 ⊗ₜ y
        · simp [(isEpi_iff_forall_one_tmul_eq R A).mp]
        · simp
      have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R A)⟩
      rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]

Goal state after:
case inr
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
this : Subsingleton ((A ⧸ R') ⊗[R] (A ⧸ R'))
⊢ Surjective ⇑(algebraMap R A)
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
this : ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m
⊢ Injective ⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))

Tactic:
let f : M →ₗ[R] A ⊗[R] M :=
      { toFun m := 1 ⊗ₜ m
        map_add' m n := tmul_add _ _ _
        map_smul' r m := tmul_smul _ _ _ }

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
this : ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m
f : M →ₗ[R] A ⊗[R] M := { toFun := fun m ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ Injective ⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Semiring C
inst✝⁶ : Algebra R C
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
⊢ f = g

Tactic:
apply AlgHom.toLinearMap_injective
  ext a b
  have := congr_arg₂ HMul.hMul (AlgHom.congr_fun ha a) (AlgHom.congr_fun hb b)
  dsimp at *
  rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this

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

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y : B), (x ⊗ₜ[R] y * 0) • m = x ⊗ₜ[R] y • 0 • m

Tactic:
intro a b
      simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
x y : R
inst✝ : IsCancelAdd R
⊢ x < y ↔ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + p

Tactic:
by
  rw [lt_iff_le_and_ne, and_comm, StarOrderedRing.le_iff, ← exists_and_left]
  congr! 2 with p
  simp +contextual [← and_assoc]

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
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ ⟨↑x, ⋯⟩ = (f i) x

Tactic:
Set.iUnionLift_mk

Goal state after:
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
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 : 0 < r
a b : A
hab : a < b
⊢ r • a < r • b

Tactic:
rw [StarOrderedRing.pos_iff] at hr
    rw [StarOrderedRing.lt_iff] at hab ⊢
    obtain ⟨a, ha₀, ha, rfl⟩ := hab
    obtain ⟨hr₀, hr⟩ := hr
    exact ⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, smul_add ..⟩

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
⊢ x ≤ y

Tactic:
let f_inv : S →⋆ₙ+* R := (f : R ≃⋆+* S).symm

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
⊢ x ≤ y
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i ↦ ↑i) → s.card ≤ n
⊢ Module.rank R M ≤ ↑n

Tactic:
rw [Module.rank_def]
  apply ciSup_le'
  rintro ⟨s, li⟩
  exact linearIndependent_bounded_of_finset_linearIndependent_bounded H _ li

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ (∃ x, ∀ (a : R), a ≠ 0 → a • x ≠ 0) → Module.rank R M ≠ 0

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
⊢ Module.rank R M ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ #↑↑⟨s, hs⟩ ≤ 0

Tactic:
rw [nonpos_iff_eq_zero, Cardinal.mk_eq_zero_iff, ← not_nonempty_iff]

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ ¬Nonempty ↑↑⟨s, hs⟩
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ Module.rank R M ≤ 0 ↔ ∀ (x : M), x = 0

Tactic:
rw [nonpos_iff_eq_zero]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case inr
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n < Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_set_linearIndependent_of_lt_rank h

Goal state after:
case inr
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
⊢ ∃ s, W = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
refine ⟨_, submodule_eq_sSup_le_nonzero_spans W, ?_⟩

Goal state after:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
⊢ ∀ a ∈ {T | ∃ m ∈ W, m ≠ 0 ∧ T = K ∙ m}, IsAtom a
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (shift x) • shift x = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e • e = 0

Tactic:
Embedding.coeFn_mk

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e • e = 0
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : NonUnitalSemiring A
inst✝² : StarRing A
inst✝¹ : Module R A
inst✝ : StarModule R A
S : NonUnitalSubalgebra R A
x y : A
hx : x ∈ star S.carrier
hy : y ∈ star S.carrier
⊢ x + y ∈ star S.carrier

Tactic:
by simpa only [Set.mem_star, NonUnitalSubalgebra.mem_carrier]
        using (star_add x y).symm ▸ add_mem hx hy

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B✝ : Type w
C✝ : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B✝
inst✝¹² : StarRing B✝
inst✝¹¹ : Module R B✝
inst✝¹⁰ : FunLike F A B✝
inst✝⁹ : NonUnitalAlgHomClass F R A B✝
inst✝⁸ : StarHomClass F A B✝
S : NonUnitalStarSubalgebra R A
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B✝ B✝
inst✝² : SMulCommClass R B✝ B✝
inst✝¹ : StarModule R B✝
inst✝ : Subsingleton A
B C : NonUnitalStarSubalgebra R A
x : A
⊢ x ∈ B ↔ x ∈ C

Tactic:
by simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
i : ι
x : ↥(K i)
h : K i ≤ iSup K
⊢ (iSupLift K dir f hf (iSup K) ⋯) ((inclusion h) x) = (f i) x

Tactic:
dsimp [iSupLift]

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
i : ι
x : ↥(K i)
h : K i ≤ iSup K
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ ((inclusion h) x) = (f i) x
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
i : ι
x : ↥(K i)
hx : ↑x ∈ iSup K
⊢ (iSupLift K dir f hf (iSup K) ⋯) ⟨↑x, hx⟩ = (f i) x

Tactic:
dsimp [iSupLift]

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
i : ι
x : ↥(K i)
hx : ↑x ∈ iSup K
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ ⟨↑x, hx⟩ = (f i) x
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf (iSup K) ⋯) x = (f i) ⟨↑x, hx⟩

Tactic:
dsimp [iSupLift]

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ x = (f i) ⟨↑x, hx⟩
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ star ↑(centralizer R s) = ↑(NonUnitalSubalgebra.centralizer R (s ∪ star s))

Tactic:
rw [StarMemClass.star_coe_eq]

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ ↑(centralizer R s) = ↑(NonUnitalSubalgebra.centralizer R (s ∪ star s))
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
have : LinearIndepOn K id (Set.range t') := by
      convert! t.linearIndependent.linearIndepOn_id
      ext
      simp [t]

Goal state after:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this✝ : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ r, r • v₀ = v
h' : ⟨v₀, hv₀⟩ = 0
⊢ v₀ = 0

Tactic:
AddSubmonoid.mk_eq_zero

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ r, r • v₀ = v
h' : v₀ = 0
⊢ v₀ = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.e_a
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n + 1)) = Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n)) + 1

Tactic:
exact Quot.sound Rel.add_scalar

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x 0 = 0

Tactic:
by simp [eval₂_eq_sum]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (C a) = f a

Tactic:
by simp [eval₂_eq_sum]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x X = x

Tactic:
by simp [eval₂_eq_sum]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (X * p) = eval₂ f x p * x

Tactic:
rw [X_mul, eval₂_mul_X]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Algebra

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q : R[X]
⊢ eval₂ (algebraMap R S) x (p * q) = eval₂ (algebraMap R S) x p * eval₂ (algebraMap R S) x q

Tactic:
exact eval₂_mul_noncomm _ _ fun k => Algebra.commute_algebraMap_left (coeff q k) x

Goal state after: