mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α✝ : Type u_11
β : Type u_12
γ : Type u_13
α : Type u_14
inst✝² : MulOne α
inst✝¹ : AddCommMonoid α
inst✝ : IsStablyFiniteRing α
n : ℕ
⊢ RingEquiv.mopMatrix 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_14
inst✝¹ : MulOne α
inst✝ : AddCommMonoid α
x✝ : IsStablyFiniteRing αᵐᵒᵖ
n : ℕ
⊢ map 1 (op ∘ op) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ (m.sum fun x ↦ id) < n.sum fun x ↦ id

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
n : ℕ
⊢ ∀ (a : Multiset α), a.card = n ↔ ((Multiset.toFinsupp.toEquiv a).sum fun x ↦ id) = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
⊢ ∀ (a : α →₀ ℕ), (a.sum fun x ↦ id) = n ↔ ∑ i, Finsupp.equivFunOnFinite a i = n

Tactic:
by

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

Goal state before:
pp: α : Type u_14
inst✝¹ : MulOne α
inst✝ : AddCommMonoid α
x✝² : IsStablyFiniteRing αᵐᵒᵖ
n : ℕ
x✝¹ x✝ : Matrix (Fin n) (Fin n) α
⊢ { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun (x✝¹ * x✝) =
    { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝¹ *
      { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝

Tactic:
by

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq m
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring α
inst✝⁴ : Semiring β
inst✝³ : Semiring γ
inst✝² : Algebra R α
inst✝¹ : Algebra R β
inst✝ : Algebra R γ
x✝ : R
⊢ MulOpposite.unop (RingEquiv.mopMatrix.toFun ((algebraMap R (Matrix m m αᵐᵒᵖ)) x✝)) =
    MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ) x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : { P // ∑ i, P i = n }
⊢ ↑((equivNatSumOfFintype α n).symm P) = ∑ a, ↑P a • {a}

Tactic:
by

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β✝ : Type u_12
γ : Type u_13
ι : Type u_14
β : ι → Type u_15
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → Mul (β i)
inst✝ : Fintype n
x✝¹ x✝ : Matrix n n ((i : ι) → β i)
⊢ piAddEquiv.toFun (x✝¹ * x✝) = piAddEquiv.toFun x✝¹ * piAddEquiv.toFun x✝

Tactic:
by

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Algebra R α
r : R
⊢ (transposeRingEquiv m α).toFun ((algebraMap R (Matrix m m α)) r) = (algebraMap R (Matrix m m α)ᵐᵒᵖ) r

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
⊢ (∑ i ∈ s, x i) *ᵥ y = ∑ i ∈ s, x i *ᵥ y

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : Matrix m n α
s : Finset ι
y : ι → n → α
⊢ x *ᵥ ∑ i ∈ s, y i = ∑ i ∈ s, x *ᵥ y i

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
s : Finset ι
x : ι → n → α
y : Matrix n m α
⊢ (∑ i ∈ s, x i) ᵥ* y = ∑ i ∈ s, x i ᵥ* y

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
⊢ x ᵥ* ∑ i ∈ s, y i = ∑ i ∈ s, x ᵥ* y i

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
by

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

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)

Tactic:
by

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

Goal state before:
pp: F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F K * Module.rank K A = Module.rank F A

Tactic:
by

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

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ finrank F K * finrank K A = finrank F A

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
⊢ ∃ f, Injective ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N : Type v
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type v
v : ι → N
hv : LinearIndependent R v
cnd : Module.rank R M ≤ #ι
⊢ lift.{v, v} (Module.rank R M) ≤ lift.{v, v} #ι

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
cnd : lift.{v', v} (Module.rank R M) < lift.{v, v'} (Module.rank R N')
⊢ ∃ f, Injective ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N : Type v
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
cnd : Module.rank R M < Module.rank R N
⊢ lift.{v, v} (Module.rank R M) < lift.{v, v} (Module.rank R N)

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = Fintype.card (ChooseBasisIndex R M)

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ lift.{u, v} ℵ₀ ≤ lift.{v, u} #R

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ Module.rank R M = #M

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Free R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : Free R M'
inst✝ : StrongRankCondition R
h : lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')
⊢ ∃ f, Injective ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Free R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : Free R M₁
inst✝ : StrongRankCondition R
⊢ Module.rank R M ≤ Module.rank R M₁ ↔ ∃ f, Injective ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
⊢ finrank R M ≤ finrank R M' ↔ ∃ f, Injective ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Free R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : Free R M'
inst✝ : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
⊢ lift.{v', v} #α = lift.{v, v'} #β

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Free R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : Free R M'
inst✝ : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
cond : finrank R M = finrank R M'
⊢ lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : Module.rank R M = 0
⊢ Subsingleton M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
I✝ : TwoSidedIdeal R
inst✝ : Nontrivial R
I J : RingCon R
h : I ≠ J
⊢ { ringCon := I } ≠ { ringCon := J }

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
inst✝ : Nontrivial R
⊢ Nontrivial (TwoSidedIdeal R)

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
⊢ Module.rank R M < ℵ₀ ↔ Module.Finite R M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
⊢ Function.Injective fun t ↦ {r | t.ringCon r 0}

Tactic:
rintro ⟨t₁⟩ ⟨t₂⟩ (h : {x | _} = {x | _})

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
⊢ { ringCon := t₁ } = { ringCon := t₂ }
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : ¬Module.Finite R M
⊢ finrank R M = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : 0 < finrank R M
⊢ Module.Finite R M

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < finrank R M

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Free R M
inst✝³ : StrongRankCondition R
W : Type v
inst✝² : AddCommMonoid W
inst✝¹ : Module R W
inst✝ : Free R W
n : ℕ
hn : n ≠ 0
hVW : Module.rank R M = n • Module.rank R W
⊢ Module.Finite R M ↔ Module.Finite R W

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
⊢ Function.Injective fun t ↦ {r | t.ringCon r 0}

Tactic:
by

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon (x - y) 0
⊢ I.ringCon x y

Tactic:
convert! I.ringCon.add h (I.ringCon.refl y) <;> abel

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y ↔ x - y ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h : ↑I ⊆ ↑J
x y : R
r : ({ toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I) x y
⊢ ({ toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J) x y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h :
  { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I ≤
    { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J
x : R
hx : x ∈ ↑I
⊢ x ∈ ↑J

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
⊢ Function.Injective ringCon

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I < J ↔ ↑I ⊂ ↑J

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
hy : y ∈ I
⊢ x + y ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x : R
hx : x ∈ I
⊢ -x ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hy : y ∈ I
⊢ x * y ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
⊢ x * y ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ x - x ∈ carrier

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x✝ y✝ : R
h : x✝ - y✝ ∈ carrier
⊢ y✝ - x✝ ∈ carrier

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
⊢ finrank S M ≤ finrank R M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x y z : R
h1 : x - y ∈ carrier
h2 : y - z ∈ carrier
⊢ x - z ∈ carrier

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
⊢ finrank R S ≤ finrank R T

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
⊢ Nonempty (R ≃ₗ[R] M) ↔ Module.rank R M = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I ≤ { ringCon := I.ringCon ⊔ J.ringCon }

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
⊢ Nonempty (R ≃ₗ[R] M) ↔ finrank R M = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ x ∈ mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right ↔ x ∈ carrier

Tactic:
by

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Free R S
⊢ Nonempty (R ≃ₐ[R] S) ↔ finrank R S = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I I' J' : TwoSidedIdeal R
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } I' ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } J' ↔
    I' ≤ J'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J ≤ { ringCon := I.ringCon ⊔ J.ringCon }

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I ≤ K
h2 : J ≤ K
⊢ { ringCon := I.ringCon ⊔ J.ringCon } ≤ K

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
⊢ Nonempty (Unique ι)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ x : R
hx : x ∈ I
y : R
hy : y ∈ J
a : R
ha : a ∈ I
b : R
hb : b ∈ J
⊢ x + a + (y + b) = x + y + (a + b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x y : R},
    x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} →
      y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → x + y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Unique ι
h : finrank R M = 1
v : M
i : ι
hv : v = 0
⊢ ((basisUnique ι h).repr v) i = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ -x + -y = -(x + y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x : R}, x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → -x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x y : R}, y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → x * y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Equivalence fun x y ↦ f x = f y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ∀ {w x y z : R}, f w = f x → f y = f z → f (w * y) = f (x * z)

Tactic:
by

Goal state after: