mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
⊢ replicateRow ι (x • v) = x • replicateRow ι v

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
v : m → α
⊢ (replicateCol ι v)ᵀ = replicateRow ι v

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
v : m → α
⊢ (replicateRow ι v)ᵀ = replicateCol ι v

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
⊢ (replicateCol ι v)ᴴ = replicateRow ι (star v)

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
⊢ (replicateRow ι v)ᴴ = replicateCol ι (star v)

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ replicateRow ι (v ᵥ* M) = replicateRow ι v * M

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ replicateCol ι (v ᵥ* M) = (replicateRow ι v * M)ᵀ

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ replicateCol ι (M *ᵥ v) = M * replicateCol ι v

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ replicateRow ι (M *ᵥ v) = (M * replicateCol ι v)ᵀ

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : DistribMulAction R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), f (m • x) = (MonoidHom.id R) m • f x
h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y
h₅ :
  ∀ (a : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) =
      star ({ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)
⊢ { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ } = f

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Star A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Star B
f : A →⋆ₐ[R] B
h₁ : f 1 = 1
h₂ :
  ∀ (x y : A),
    { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) =
      { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y
h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0
h₄ :
  ∀ (x y : A),
    (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
      (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x +
        (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y
h₅ :
  ∀ (r : R),
    (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
      (algebraMap R B) r
h₆ :
  ∀ (x : A),
    (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                  commutes' := h₅ }.toRingHom).toFun
        (star x) =
      star
        ((↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                    commutes' := h₅ }.toRingHom).toFun
          x)
⊢ { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆ } = f

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
x : O
xN : x ∈ N
hx : (ϕ ∘ₗ inclusion N_le_M) ⟨x, xN⟩ = 0
⊢ N.subtype ⟨x, xN⟩ ∈ M'

Tactic:
exact ⟨⟨x, N_le_M xN⟩, hx, rfl⟩

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

Goal state before:
pp: K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
p q : Subfield K
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
cases p; cases q; congr; exact SetLike.ext' h

Goal state after:
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
⊢ ∀ {a b : K},
    a ∈ {x | ∃ (hx : x ∈ closure s), p x hx} →
      b ∈ {x | ∃ (hx : x ∈ closure s), p x hx} → a * b ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
by rintro _ _ ⟨_, hx⟩ ⟨_, hy⟩; exact ⟨_, mul _ _ _ _ hx hy⟩

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

Goal state before:
pp: case c.c.c.e_a.e_a
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₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ rc • r₃ /ₒ (sc * (sa * s₁)) = r₃ /ₒ s₃

Tactic:
rw [OreLocalization.expand r₃ s₃ rc (hc.symm ▸ (sc * (sa * s₁)).2)]; congr; ext; exact hc

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

Goal state before:
pp: case c
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
⊢ 0 + r✝ /ₒ s✝ = r✝ /ₒ s✝

Tactic:
← zero_oreDiv,

Goal state after:
case c
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
⊢ 0 /ₒ ?c✝ + r✝ /ₒ s✝ = r✝ /ₒ s✝

case c
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
⊢ ↥S
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c
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✝ /ₒ s✝ + 0 = r✝ /ₒ s✝

Tactic:
← zero_oreDiv,

Goal state after:
case c
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✝ /ₒ s✝ + 0 /ₒ ?c✝ = r✝ /ₒ s✝

case c
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
⊢ ↥S
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M₂ : Type u_6
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Finite m
v₁ : Basis n R R
v₂ : Basis m R M₂
x : M₂
⊢ (toMatrix v₁ v₂) (toSpanSingleton R M₂ x) = vecMulVec ⇑(v₂.repr x) ⇑v₁

Tactic:
by
  ext; simp [toMatrix_apply, vecMulVec_apply, mul_comm]

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

Goal state before:
pp: K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
a✝ b✝ : K
x_mem : a✝ ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
y_mem : b✝ ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
⊢ a✝ + b✝ ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}

Tactic:
by
    -- Use `id` in the next 2 `obtain`s so that assumptions stay there for the `rwa`s below
    obtain ⟨nx, hnx, dx, hdx, rfl⟩ := id x_mem
    obtain ⟨ny, hny, dy, hdy, rfl⟩ := id y_mem
    by_cases hx0 : dx = 0; · rwa [hx0, div_zero, zero_add]
    by_cases hy0 : dy = 0; · rwa [hy0, div_zero, add_zero]
    exact
      ⟨nx * dy + dx * ny, Subring.add_mem _ (Subring.mul_mem _ hnx hdy) (Subring.mul_mem _ hdx hny),
        dx * dy, Subring.mul_mem _ hdx hdy, (div_add_div nx ny hx0 hy0).symm⟩

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

Goal state before:
pp: case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ ∀ b ∈ Finset.univ, b ≠ i → M j b * (Finsupp.single i 1) b = 0

pp: case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ i ∉ Finset.univ → M j i * (Finsupp.single i 1) i = 0

Tactic:
· intro i' _ i'_ne
    rw [Finsupp.single_eq_of_ne i'_ne, mul_zero]

Goal state after:
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ i ∉ Finset.univ → M j i * (Finsupp.single i 1) i = 0
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:
rw [← mk_zero 1, liftOn_mk]

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

Goal state before:
pp: ι✝ : Type u_1
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : DecidableEq ι✝
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
ι : Type u_5
inst✝¹ : Finite ι
inst✝ : IsStablyFiniteRing A
this : Fintype ι
⊢ IsStablyFiniteRing (End A (ι → A))

Tactic:
rw [← MulOpposite.isStablyFiniteRing_iff,
    ← RingEquiv.isStablyFiniteRing_iff (matrixRingEquivEndVecMulOpposite (ι := ι) (A := A))]

Goal state after:
ι✝ : Type u_1
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : DecidableEq ι✝
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
ι : Type u_5
inst✝¹ : Finite ι
inst✝ : IsStablyFiniteRing A
this : Fintype ι
⊢ IsStablyFiniteRing (Matrix ι ι A)
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 y : ↥M
⊢ mk' S (↑y * ↑x) (y * x) = 1

Tactic:
exact mk'_self _ _

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M : Submonoid R
hM : Algebra.algebraMapSubmonoid S M ≤ IsUnit.submonoid S
h : Bijective ⇑(algebraMap R S)
y : S
⊢ ∃ x, y * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
by
    obtain ⟨x, rfl⟩ := h.surjective y
    use ⟨x, 1⟩
    simp

Goal state after:
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
x y : ℤ
⊢ (algebraMap ℤ ℚ) x = (algebraMap ℤ ℚ) y → ∃ c, ↑c * x = ↑c * y

Tactic:
by
    rw [eq_intCast, eq_intCast, Int.cast_inj]
    rintro rfl
    use 1

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

Goal state before:
pp: A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap K₂ L₂) (e ((algebraMap A K₁) r / (algebraMap A K₁) s)) =
    f ((algebraMap K₁ L₁) ((algebraMap A K₁) r / (algebraMap A K₁) s))

Tactic:
simp_rw [map_div₀, AlgHom.commutes, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply A B L₁, AlgHom.commutes, ← IsScalarTower.algebraMap_apply]

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
I : Submodule R N
s : Set (↥I ⊗[R] M)
hs : s.Finite
⊢ ∃ J, ∃ (_ : J.FG) (hle : J ≤ I), s ⊆ ↑(rTensor M (inclusion hle)).range

Tactic:
choose J fg hle y eq using exists_fg_le_eq_rTensor_inclusion (M := M) (I := I)

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 : 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
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝ : InvolutiveStar α
s t : Set α
⊢ s⋆ ⊆ t ↔ s ⊆ t⋆

Tactic:
← star_subset_star,

Goal state after:
α : Type u_1
inst✝ : InvolutiveStar α
s t : Set α
⊢ s⋆⋆ ⊆ t⋆ ↔ s ⊆ t⋆
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
x : R
⊢ x ∈ resolventSet R (-a) ↔ x ∈ -resolventSet R a

Tactic:
simp only [mem_neg, mem_resolventSet_iff, map_neg, ← neg_add', IsUnit.neg_iff, sub_neg_eq_add]

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

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ (algebraMap R C) (toProd 1).1 + φ (toProd 1).2 = 1

Tactic:
simp only [fst_one, map_one, snd_one, φ.map_zero, add_zero]

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
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✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
⊢ (↑(TensorProduct.comm R C D)).comp (map f g) = (map g f).comp ↑(TensorProduct.comm R A B)

Tactic:
ext <;> rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ (lmul' R).comp (map f g) = lift f g ⋯

Tactic:
ext <;> rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ productMap f g = (lmul' R).comp (map f g)

Tactic:
ext <;> rfl

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
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * c

Tactic:
by
  nth_rewrite 2 [← hc]; exact star_right_conjugate_nonneg ha c

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
S : Subalgebra R A
ι : 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
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ 0 = 0

Tactic:
by
        dsimp
        exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)

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

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{w, v} (Module.rank R M) = lift.{w, v} ↑(finrank R M)

Tactic:
finrank_eq_rank

Goal state after:
ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{w, v} (Module.rank R M) = lift.{w, v} (Module.rank R M)
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✝⁸ : 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
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
a✝ : A
x✝ : a✝ ∈ (NonUnitalAlgebra.adjoin R (s ∪ star s)).carrier
⊢ a✝ ∈ NonUnitalAlgebra.adjoin R (star (s ∪ star s))

Tactic:
Set.union_star,

Goal state after:
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✝⁸ : 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
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
a✝ : A
x✝ : a✝ ∈ (NonUnitalAlgebra.adjoin R (s ∪ star s)).carrier
⊢ a✝ ∈ NonUnitalAlgebra.adjoin R (star s ∪ star (star s))
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝¹ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝¹.extend ⋯)) K V := Basis.extend this✝¹
b_eq : b = Basis.extend this✝¹
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this✝ : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝¹.extend ⋯
this : span K (Set.range ⇑bS) = ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))

Tactic:
rw [bS_eq, Basis.coe_ofVectorSpace, Subtype.range_coe] at this

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝¹ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝¹.extend ⋯)) K V := Basis.extend this✝¹
b_eq : b = Basis.extend this✝¹
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this✝ : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝¹.extend ⋯
this : span K (Basis.ofVectorSpaceIndex K ↥S) = ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥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₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
h' : v₀ = 0
H : ¬⟨0, ⋯⟩ = 0
⊢ False

Tactic:
exact H rfl

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

Goal state before:
pp: case pos
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : Module.rank F ↥S = 1
⊢ S = ⊥

Tactic:
refine bot_unique fun x hx ↦ Algebra.mem_bot.2 ?_

Goal state after:
case pos
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : Module.rank F ↥S = 1
x : E
hx : x ∈ S
⊢ x ∈ range ⇑(algebraMap F E)