mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} #↑(range v)

Tactic:
Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{v, w} #ι
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq : (∃ f, Injective ⇑f) → ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
rw [← n.succ_pred_eq_of_pos pos] at eq ⊢

Goal state after:
case refine_2
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq : (∃ f, Injective ⇑f) → ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ StrongRankCondition R ↔ ∀ n > 0, 0 < finrank R (Fin n → R)

Tactic:
rw [strongRankCondition_iff_forall_rank_lt_aleph0, ← not_iff_not]
  push Not
  simp_rw [finrank, Nat.le_zero, toNat_eq_zero]
  refine ⟨fun ⟨n, le⟩ ↦ ⟨n + 1, n.succ_pos, ?_⟩, fun ⟨n, pos, eq⟩ ↦ ⟨n, ?_⟩⟩
  · exact .inr <| le.trans <| LinearMap.rank_le_of_injective
      (ExtendByZero.linearMap R _) <| extend_injective (Fin.castSucc_injective n) _
  · rw [or_iff_not_imp_left, ← Ne, ← Cardinal.one_le_iff_ne_zero, one_le_rank_iff] at eq
    rw [← n.succ_pred_eq_of_pos pos] at eq ⊢
    exact eq ⟨.single R (fun _ ↦ _) 0, Pi.single_injective (M := fun _ ↦ _) _⟩

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
h : Function.Injective (dotProduct a)
b : m → α
hb : b ≠ 0
hba : b ⬝ᵥ a = 0
⊢ False

Tactic:
simpa [dotProduct_comm a b, hba, hb] using @h b 0

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
b : n
M : Matrix m n α
⊢ (single i j c * M) i b = c * M j b

Tactic:
by simp [mul_apply, single]

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : m
j : n
a : l
M : Matrix l m α
⊢ (M * single i j c) a j = M a i * c

Tactic:
by simp [mul_apply, single]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
⊢ (algebraMap R A) r * a ∈
    { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I * M

Tactic:
exact Submodule.mul_mem_mul ⟨r, hr, rfl⟩ ha

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
M : Matrix n m R
v : n → R
i : m
⊢ f ((v ᵥ* M) i) = (⇑f ∘ v ᵥ* M.map ⇑f) i

Tactic:
by
  simp only [Matrix.vecMul, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (↑(toAlgHom R (↥S) A)).range = toSubmodule S

Tactic:
ext
  simp [algebraMap_eq]

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

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

Tactic:
sSup_def,

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
⊢ motive x

Tactic:
let T : Subalgebra R A :=
  { carrier := {x | motive x}
    mul_mem' {a b} := mul a b
    add_mem' {a b} := add a b
    algebraMap_mem' := algebraMap }
  suffices iSup S ≤ T from this mem
  rwa [iSup_le_iff]

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

Goal state before:
pp: case mul
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : x ∈ adjoin R s), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : x ∈ adjoin R s), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : x ∈ adjoin R s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ * y✝) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: case mul
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
hx : x ∈ adjoin R s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ * y✝) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
s : Set A
t : Subalgebra R B
⊢ adjoin R (⇑f '' s) ≤ t ↔ Subalgebra.map f (adjoin R s) ≤ t

Tactic:
simp [Subalgebra.map_le, adjoin_le_iff]

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
h : x ∈ adjoin R s
⊢ f x ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
by
  induction h using adjoin_induction with
  | mem a ha => exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
  | algebraMap r =>
    have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
    convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
    rw [algebraMap_eq_smul_one]
    exact f.map_smul _ _
  | add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
  | mul y z _ _ hy hz => simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n : M₂'
i : ι₁
⊢ component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
      ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n =
    (AlgebraTensorModule.mk R S (M₁ i) M₂').flip n ∘ₗ component S ι₁ M₁ i

Tactic:
ext j n

Goal state after:
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
i j : ι₁
n : M₁ j
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₂ : Type v₂
inst✝⁶ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n : ⨁ (i : ι₂), M₂ i
i : ι₂
⊢ ↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) i) ∘ₗ ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m =
    (mk R M₁' (M₂ i)) m ∘ₗ component R ι₂ M₂ i

Tactic:
ext j n

Goal state after:
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₂ : Type v₂
inst✝⁶ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n✝ : ⨁ (i : ι₂), M₂ i
i j : ι₂
n : M₂ j
⊢ ((↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) i) ∘ₗ
          ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m) ∘ₗ
        lof R ι₂ M₂ j)
      n =
    (((mk R M₁' (M₂ i)) m ∘ₗ component R ι₂ M₂ i) ∘ₗ lof R ι₂ M₂ j) n
Module: Mathlib.LinearAlgebra.Matrix.RowCol

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

Tactic:
updateCol_self,

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

Goal state before:
pp: case inl.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ (diagonal v).updateCol j (Pi.single j x) j j = Function.update v j x j

Tactic:
updateCol_self,

Goal state after:
case inl.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ Pi.single j x j = Function.update v j x j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol k (Pi.single k x) j k = 0

Tactic:
updateCol_self,

Goal state after:
case inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ Pi.single k x j = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := ⋯
d : R := ⋯
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := ⋯
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ ϕ.submoduleImage N ≤ R ∙ d

Tactic:
← span_singleton_generator (ϕ.submoduleImage N)

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ R ∙ generator (ϕ.submoduleImage N) ≤ R ∙ d
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
n : ℕ
⊢ LinearEquiv.baseChange R A M M (f ^ n) = LinearEquiv.baseChange R A M M f ^ n

Tactic:
by
  induction n with
  | zero => simp
  | succ n h =>
    simp [pow_succ, LinearEquiv.baseChange_mul, h]

Goal state after:
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
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
⊢ add'' r₁ s₁ r₂ s₂ = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Tactic:
simp only [add'']

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
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
⊢ (oreDenom (↑s₁) s₂ • r₁ + oreNum (↑s₁) s₂ • r₂) /ₒ (oreDenom (↑s₁) s₂ * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
⊢ (fun f i j ↦ f ((single R (fun x ↦ R) i) 1) j) M.vecMulLinear = M

Tactic:
by
    ext i j
    simp

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : m ∈ nonZeroDivisors M
n : N
ms : M × ↥S
h0 : n * f ↑ms.2 * f m = 0
eq : n * f ↑ms.2 = f ms.1
⊢ n = 0

Tactic:
eq,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : m ∈ nonZeroDivisors M
n : N
ms : M × ↥S
h0 : f ms.1 * f m = 0
eq : n * f ↑ms.2 = f ms.1
⊢ n = 0
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : m ∈ nonZeroDivisors M
n : N
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
h0 : ∃ s, ↑s * ms.1 = 0
⊢ n * f ↑ms.2 = 0

Tactic:
eq,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : m ∈ nonZeroDivisors M
n : N
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
h0 : ∃ s, ↑s * ms.1 = 0
⊢ f ms.1 = 0
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f ↑s₃ * f r₁ + f r₃ * f r₂) = ↑(fS s₁)⁻¹ * f r₁ + ↑(fS s₂)⁻¹ * f r₂

Tactic:
rw [mul_add, mul_assoc, ← mul_assoc _ (f s₃), hf, ← Units.val_mul]

Goal state after:
case c.c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * (↑((fS s₃)⁻¹ * fS s₃) * f r₁) + ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f r₃ * f r₂) =
    ↑(fS s₁)⁻¹ * f r₁ + ↑(fS s₂)⁻¹ * f r₂
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
⊢ finrank R ↥(restrictScalars R I) = finrank R S

Tactic:
obtain ⟨_, bS, bI, _, _, _⟩ := (I.restrictScalars R).smithNormalForm b

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
fst✝ : ℕ
bS : Basis ι R S
bI : Basis (Fin fst✝) R ↥(restrictScalars R I)
f✝ : Fin fst✝ ↪ ι
a✝ : Fin fst✝ → R
snf✝ : ∀ (i : Fin fst✝), ↑(bI i) = a✝ i • bS (f✝ i)
⊢ finrank R ↥(restrictScalars R I) = finrank R S
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ adjoin S s ≤ adjoin S ↑(adjoin R s)

pp: R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ ↑(adjoin R s) ⊆ ↑(adjoin S s)

Tactic:
· exact adjoin_mono subset_adjoin

Goal state after:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ ↑(adjoin R s) ⊆ ↑(adjoin S s)
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : (algebraMap A K) x / (algebraMap A K) ↑y = 1
hy : (algebraMap A K) ↑y ≠ 0
⊢ x = ↑y

Tactic:
div_eq_one_iff_eq hy

Goal state after:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : (algebraMap A K) x = (algebraMap A K) ↑y
hy : (algebraMap A K) ↑y ≠ 0
⊢ x = ↑y
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ IsLocalization (Submonoid.map h M) S → IsLocalization M S

Tactic:
intro (H : IsLocalization (Submonoid.map (h : R ≃* P) M) S)

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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ IsLocalization M S
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
C : Type u_5
inst✝³ : Semiring C
inst✝² : Algebra R C
F : Type u_6
inst✝¹ : FunLike F (Unitization R A) C
inst✝ : AlgHomClass F R (Unitization R A) C
φ ψ : F
h : ∀ (a : A), φ ↑a = ψ ↑a
r : R
⊢ φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)

Tactic:
by simp only [AlgHomClass.commutes]

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
r : R
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ ((algebraMap R ↥(iSup K)) r) =
    (algebraMap R B) r

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

Goal state after:
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
x : R
⊢ star x < 1 ↔ x < 1

Tactic:
by
  simpa using star_lt_star_iff (x := x) (y := 1)

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

Tactic:
by
    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: