mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ (g a • ⇑a) 1 = (∑ i ∈ insert a s, g i • ⇑i) 1

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
s : { s // LinearIndepOn R id s }
le : ↑(n + 1) ≤ #↑↑s
t : Finset ↑↑s
ht : n + 1 = t.card
⊢ ↑(Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t) ⊆ ↑s

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ (∑ i ∈ insert a s, g i • ⇑i) 1 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
s : Finset M
card_s : s.card = n
ind_s : LinearIndepOn R id ↑s
⊢ #↑↑s = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
⊢ LinearIndependent L fun f ↦ ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), v default = 0 → l default = 0
hv : v default = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
v : ι → M
inst✝ : Unique ι
⊢ LinearIndependent R v ↔ v default ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ Subsingleton ι

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ (Finset.map { toFun := v, inj' := ⋯ } Finset.univ).card = n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
h : f default ≠ 0
i : ι
⊢ f i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
⊢ ↑n ≤ Module.rank R M ↔ ∃ v, LinearIndependent R v

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
⊢ ↑n ≤ Module.rank R M ↔ ∃ f, Injective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, 0 < f i

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ Module.rank R M = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 1 → R) →ₗ[R] M
hf : Injective ⇑f
⊢ Injective ⇑(f ∘ₗ ?m.100)

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ 1 ≤ Module.rank R M ↔ ∃ f, Injective ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.rank R M ≠ 0
⊢ ?m.16

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.rank R M ≠ 0
f : R →ₗ[R] M
hf : Injective ⇑f
x y : R
hxy : ∀ (a : M), x • a = y • a
⊢ f x = f y

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : ¬FaithfulSMul R M
⊢ Module.rank R M = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ finrank R M = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M = ↑n
⊢ finrank R M = n

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ finrank R M ≤ n

Tactic:
by

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ finrank R M < n

Tactic:
by

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M ≃+ M'
hi : Bijective i
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
x✝¹ : R
x✝ : M'
⊢ i x✝¹ • x✝ = j (x✝¹ • ↑j.symm x✝)

Tactic:
by

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

Goal state before:
pp: R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R' M₁
i : R' → R
j : M →+ M₁
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < Module.rank R M

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 1 < finrank R M
⊢ 1 < Module.rank R M

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} (Module.rank R N)
h' : Module.rank R N < ℵ₀
⊢ finrank R M ≤ finrank R N

Tactic:
by

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

Goal state before:
pp: R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R' M₁
i : R → R'
j : M →+ M₁
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M ≃ₗ[R] N
⊢ finrank R M = finrank R N

Tactic:
by

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

Goal state before:
pp: R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R' M₁
i : R → R'
j : M ≃+ M₁
hi : Bijective i
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
⊢ Module.rank R M = Module.rank R' M₁

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Injective ⇑f
⊢ finrank R ↥f.range = finrank R M

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ finrank R ↥⊤ = finrank R M

Tactic:
by

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

Goal state before:
pp: R₀ : Type u_1
S₀ : Type u_2
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Semiring S₀
inst✝³ : Algebra R₀ S₀
R₁ : Type u_3
S₁ : Type u_4
inst✝² : CommSemiring R₁
inst✝¹ : Semiring S₁
inst✝ : Algebra R₁ S₁
i : R₀ ≃+* R₁
j : S₀ ≃+* S₁
hc : (algebraMap R₁ S₁).comp i.toRingHom = j.toRingHom.comp (algebraMap R₀ S₀)
⊢ finrank R₀ S₀ = finrank R₁ S₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_3
⊢ univ.encard = ENat.card α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + m / k * k = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m / k * k + m % k = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬a * b ≺ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a : R
⊢ a % 0 = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a : R
this : (p : Prop) → Decidable p
h : ¬a = 0
⊢ ¬a ≺ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
⊢ P a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd 0 a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard = ↑h.toFinset.card

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.encard = ↑s.toFinset.card

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ ↑(Fintype.card ↑s) = s.encard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s).encard = ↑s.card

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
⊢ f (f ![0, 1] • ![1, 0]) = f (f ![1, 0] • ![0, 1])

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
⊢ s.encard = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard = 0 ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
⊢ ∅.encard = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
this : f ![0, 1] • ![1, 0] = f ![1, 0] • ![0, 1]
⊢ f ![0, 1] = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard ≠ 0
⊢ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≠ 0 ↔ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ 0 < s.encard ↔ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
e : α
⊢ {e}.encard = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).encard = s.encard + t.encard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
⊢ a ∉ {x | x ≠ a}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
this : f ![0, 1] • ![1, 0] = f ![1, 0] • ![0, 1]
h₁ : f ![0, 1] = 0
⊢ 0 = f ![1, 0]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdA 0 s = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
this : {x | x ≠ a}.encard + {a}.encard = ({x | x ≠ a} ∪ {a}).encard
⊢ {x | x ≠ a} ∪ {a} = univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdB 0 s = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
⊢ {x | x ≠ a}.encard + 1 = ENat.card α

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
this : f ![0, 1] • ![1, 0] = f ![1, 0] • ![0, 1]
h₁ : f ![0, 1] = 0
h₂ : 0 = f ![1, 0]
⊢ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ Disjoint s {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ (insert a s).encard = s.encard + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ ↑(a % b).natAbs < ↑b.natAbs

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs ≤ (a * b).natAbs

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ Module.rank R R = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard < ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard = ⊤ ↔ s.Infinite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≠ ⊤ ↔ s.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ s.Finite

Tactic:
by

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
x✝² : { s // LinearIndepOn R id s }
s : Set M
h : LinearIndepOn R id s
x✝¹ : M
x✝ : j x✝¹ = 0
⊢ j x✝¹ = j 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k

Tactic:
by

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
by

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

Goal state before:
pp: R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M₁
inst✝ : Module R' M₁
i : R' → R
j : M →+ M₁
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
x✝ : s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
left✝ : s.Finite
n₀ : ℕ
hs : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ s.encard ≤ ↑k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).encard = s.encard * t.encard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
h : Fintype α
ι : α → Type u_3
s : (i : α) → Set (ι i)
⊢ (univ.pi s).encard = ∏ i, (s i).encard

Tactic:
by

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

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective ⇑i
hj : Injective ⇑j
hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ t.encard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ (t \ s).encard + s.encard = t.encard

Tactic:
by

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

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')

Tactic:
by

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

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R ≃+* R'
j : S ≃+* S'
hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)
⊢ lift.{v', v} (Module.rank R S) = lift.{v, v'} (Module.rank R' S')

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : S.FG
⊢ Monoid.FG (Localization S)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
⊢ LinearIndepOn R v ↑s ↔ ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0

Tactic:
by

Goal state after: