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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i, g i • b i = 0 → ∀ (i : n), g i = 0
⊢ ∀ (g : n → R), ∑ i, g i • b i • a = 0 → ∀ (i : n), g i = 0

Tactic:
]

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i, g i • b i = 0 → ∀ (i : n), g i = 0
⊢ ∀ (g : n → R), ∑ i, g i • b i • a = 0 → ∀ (i : n), g i = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg.inr.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : ¬f b ≤ f i
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
hsi : s ∈ f i
ht : ∃ i, ∃ (_ : i ∈ ↑t), r + s ∈ ↑(f i)
⊢ False

Tactic:
]

Goal state after:
case neg.inr.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : ¬f b ≤ f i
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
hsi : s ∈ f i
ht : ∃ i, ∃ (_ : i ∈ ↑t), r + s ∈ ↑(f i)
⊢ False
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
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
h : 0 < Module.rank R M
⊢ ¬Subsingleton M

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
h : 0 < Module.rank R M
⊢ ¬Subsingleton M
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
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
⊢ Module.rank R M ≠ 0 ↔ ¬Module.rank R M = 0

Tactic:
]

Goal state after:
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
h : Basis ι R M
⊢ toNat (Module.rank R M) = toNat (Module.rank R M)

Tactic:
]

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

Goal state before:
pp: case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
h : Basis ι R M
val✝ : Fintype ι
⊢ ↑(Fintype.card ι) = ↑(Fintype.card ι)

Tactic:
]

Goal state after:
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
inst✝ : StrongRankCondition R
ι : Type w
b : Finset ι
h : Basis (↥b) R M
⊢ b.card = b.card

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
⊢ Cardinal.lift.{u, ?u.29} 1 = Cardinal.lift.{?u.29, u} 1

Tactic:
]

Goal state after:
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
inst✝ : StrongRankCondition R
x : M
h : Bijective ⇑(LinearMap.toSpanSingleton R M x)
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : StrongRankCondition R
h : Bijective ⇑(algebraMap R S)
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ : Type v
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
ι : Type w
ι' : Type w'
inst✝⁴ : StrongRankCondition R✝
R : Type u_2
M : Type u_3
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s t : Set M
inst✝ : Module.Finite R ↥(span R t)
hs : LinearIndepOn R id s
hst : s ⊆ t
⊢ Module.rank R ↥(span R t) < ℵ₀

Tactic:
]

Goal state after:
R✝ : Type u
S : Type u_1
M✝ : Type v
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
ι : Type w
ι' : Type w'
inst✝⁴ : StrongRankCondition R✝
R : Type u_2
M : Type u_3
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s t : Set M
inst✝ : Module.Finite R ↥(span R t)
hs : LinearIndepOn R id s
hst : s ⊆ t
⊢ Module.rank R ↥(span R t) < ℵ₀
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
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ Module.rank R M = Module.rank R M

Tactic:
]

Goal state after:
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
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : ¬ℵ₀ ≤ Module.rank R M
⊢ finrank R M = 0 ↔ Subsingleton M

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : ¬ℵ₀ ≤ Module.rank R M
⊢ finrank R M = 0 ↔ Subsingleton M
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
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : Module.rank R M < ℵ₀
⊢ finrank R M = 0 ↔ Subsingleton M

Tactic:
rw [← not_le] at this

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : ¬ℵ₀ ≤ Module.rank R M
⊢ finrank R M = 0 ↔ Subsingleton M
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ x ∈ ↑u, ↑(f x)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i

Tactic:
subset_union_prime' hp'

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i

Tactic:
]

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i
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
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ Subsingleton M ↔ ¬0 < finrank R M

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ Subsingleton M ↔ ¬0 < finrank R M
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ x ∈ u, I ≤ f x

Tactic:
]

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ x ∈ u, I ≤ f x
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
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R ↥N = Module.rank R ↥N

pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R ↥N < ℵ₀

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R ↥N < ℵ₀
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
inst✝⁵ : StrongRankCondition R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ ↑(finrank R ↥L') < ℵ₀

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ ↑(finrank R ↥L') < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

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✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank S M ≤ Module.rank R M

pp: case hc
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank S M < ℵ₀

pp: case hd
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank R M < ℵ₀

Tactic:
]

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

case hc
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank S M < ℵ₀

case hd
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank R M < ℵ₀
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
]

Goal state after:
case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert a t, I ≤ f i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ I ≤ f a ∨ ∃ x ∈ t, I ≤ f x

Tactic:
]

Goal state after:
case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ I ≤ f a ∨ ∃ x ∈ t, I ≤ f x
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀) ↔ ¬∀ n > 0, 0 < finrank R (Fin n → R)

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀) ↔ ¬∀ n > 0, 0 < finrank R (Fin n → R)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
⊢ ∑ y ∈ s, ∑ x, u x * v y x = ∑ i ∈ s, ∑ i_1, u i_1 * v i i_1

Tactic:
]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
s : Finset ι
u : ι → m → α
v : m → α
⊢ ∑ y ∈ s, ∑ x, u y x * v x = ∑ i ∈ s, ∑ i_1, u i i_1 * v i_1

Tactic:
]

Goal state after:
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:
]

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 → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)
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.pred.succ → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n.pred.succ → R)

Tactic:
]

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: K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
inst✝ : Module.Finite K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : span K t = span K s
ht_indep : LinearIndependent K Subtype.val
⊢ #↑t = #↑t

Tactic:
]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ v i = v i

Tactic:
]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
i : n
v : n → α
⊢ v i = v i

Tactic:
]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ -(v ⬝ᵥ -w) = v ⬝ᵥ w

Tactic:
dotProduct_neg,

Goal state after:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ - -(v ⬝ᵥ w) = v ⬝ᵥ w
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ v ⬝ᵥ w = v ⬝ᵥ w

Tactic:
]

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert b t, I ≤ f i

Tactic:
]

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert b t, I ≤ f i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ I ≤ f b ∨ ∃ x ∈ t, I ≤ f x

Tactic:
]

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ I ≤ f b ∨ ∃ x ∈ t, I ≤ f x
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
hp : ∀ i ∈ ∅, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ∅
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ i ∈ ∅, I ≤ f i

Tactic:
]

Goal state after:
case neg.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
hp : ∀ i ∈ ∅, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ∅
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ i ∈ ∅, I ≤ f i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case refine_1
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 0 ⟨x, h⟩ * B ⟨x, h⟩ 0 else 0) +
        if h : 0 < 2 then A 0 ⟨0, h⟩ * B ⟨0, h⟩ 0 else 0) +
      if h : 1 < 2 then A 0 ⟨1, h⟩ * B ⟨1, h⟩ 0 else 0) =
    A 0 0 * B 0 0 + A 0 1 * B 1 0

Tactic:
]

Goal state after:
case refine_1
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 0 ⟨x, h⟩ * B ⟨x, h⟩ 0 else 0) +
        if h : 0 < 2 then A 0 ⟨0, h⟩ * B ⟨0, h⟩ 0 else 0) +
      if h : 1 < 2 then A 0 ⟨1, h⟩ * B ⟨1, h⟩ 0 else 0) =
    A 0 0 * B 0 0 + A 0 1 * B 1 0
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : f.symm i ≠ i'
⊢ 0 = 0

pp: case inl.hi
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : f.symm i ≠ i'
⊢ i ≠ f i'

Tactic:
]

Goal state after:
case inl.hi
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
hi : f.symm i ≠ i'
⊢ i ≠ f i'
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case refine_2
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 0 ⟨x, h⟩ * B ⟨x, h⟩ 1 else 0) +
        if h : 0 < 2 then A 0 ⟨0, h⟩ * B ⟨0, h⟩ 1 else 0) +
      if h : 1 < 2 then A 0 ⟨1, h⟩ * B ⟨1, h⟩ 1 else 0) =
    A 0 0 * B 0 1 + A 0 1 * B 1 1

Tactic:
]

Goal state after:
case refine_2
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 0 ⟨x, h⟩ * B ⟨x, h⟩ 1 else 0) +
        if h : 0 < 2 then A 0 ⟨0, h⟩ * B ⟨0, h⟩ 1 else 0) +
      if h : 1 < 2 then A 0 ⟨1, h⟩ * B ⟨1, h⟩ 1 else 0) =
    A 0 0 * B 0 1 + A 0 1 * B 1 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
]

Goal state after:
case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1