mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simpa using

Goal state after:
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₁
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:
simpa using

Goal state after:
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₁
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:
simpa using

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

Goal state after:
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₁
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ ¬↑2 ≤ Module.rank R R ∧ 1 ≤ Module.rank R R

Tactic:
Module.le_rank_iff_exists_linearMap,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (¬∃ f, Injective ⇑f) ∧ 1 ≤ Module.rank R R
Module: Mathlib.Algebra.EuclideanDomain.Defs

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

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a : R
⊢ a % 0 = a
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:
simpa using

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a : R
this : (p : Prop) → Decidable p
h : ¬a = 0
⊢ ¬a ≺ 1
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:
simpa using

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

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

Goal state after:
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]
⊢ False
Module: Mathlib.Algebra.EuclideanDomain.Int

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

Tactic:
rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ b0), ← Int.abs_eq_natAbs]
      exact Int.emod_lt_abs _ b0

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:
simpa using

Goal state after:
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₁
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : 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 ι
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
h : (if h : ↑i ∈ s then f ⟨↑i, h⟩ else 0) = 0
⊢ f i = 0

Tactic:
simpa using

Goal state after:
case refine_2
ι : 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 ι
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
h : (if h : ↑i ∈ s then f ⟨↑i, h⟩ else 0) = 0
⊢ f i = 0
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'
inst✝² : CommSemiring R'
S' : Type v
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'
⊢ Module.rank R S ≤ Module.rank R' S'

Tactic:
simpa using

Goal state after:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
inst✝² : CommSemiring R'
S' : Type v
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'
⊢ Module.rank R S ≤ Module.rank R' S'
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'
inst✝² : CommSemiring R'
S' : Type v
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)
⊢ Module.rank R S ≤ Module.rank R' S'

Tactic:
simpa using

Goal state after:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
inst✝² : CommSemiring R'
S' : Type v
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)
⊢ Module.rank R S ≤ Module.rank R' S'
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'
inst✝² : CommSemiring R'
S' : Type v
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)
⊢ Module.rank R S = Module.rank R' S'

Tactic:
simpa using

Goal state after:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
inst✝² : CommSemiring R'
S' : Type v
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)
⊢ Module.rank R S = Module.rank R' S'
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
⊢ Module.rank R ↥f.range ≤ Module.rank R M

Tactic:
simpa using

Goal state after:
R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
⊢ Module.rank R ↥f.range ≤ Module.rank R M
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
p : Submodule R M
⊢ Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p

Tactic:
simpa using

Goal state after:
R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
p : Submodule R M
⊢ Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
p : Submodule R M
⊢ Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p

Tactic:
by simpa using lift_rank_map_le f p

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ Module.rank R ↥f.range = Module.rank R M'

Tactic:
by
  rw [LinearMap.range_eq_top.2 h, rank_top]

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
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
L L' : Submodule R M
s : S
hr : IsSMulRegular M s
h✝ : ∀ x ∈ L, s • x ∈ L'
x✝¹ x✝ : ↥L
h : (LinearMap.restrict ((Algebra.lsmul S R M) s) h✝) x✝¹ = (LinearMap.restrict ((Algebra.lsmul S R M) s) h✝) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
L L' : Submodule R M
s : S
hr : IsSMulRegular M s
h✝ : ∀ x ∈ L, s • x ∈ L'
x✝¹ x✝ : ↥L
h : (LinearMap.restrict ((Algebra.lsmul S R M) s) h✝) x✝¹ = (LinearMap.restrict ((Algebra.lsmul S R M) s) h✝) x✝
⊢ x✝¹ = x✝
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R'
T : Type u'
inst✝⁶ : Module R R'
inst✝⁵ : NonAssocSemiring T
inst✝⁴ : Module R T
inst✝³ : Module R' T
inst✝² : IsScalarTower R' T T
inst✝¹ : FaithfulSMul R' T
inst✝ : IsScalarTower R R' T
⊢ Module.rank R R' ≤ Module.rank R T

Tactic:
simpa using

Goal state after:
R : Type u
R' : Type u'
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R'
T : Type u'
inst✝⁶ : Module R R'
inst✝⁵ : NonAssocSemiring T
inst✝⁴ : Module R T
inst✝³ : Module R' T
inst✝² : IsScalarTower R' T T
inst✝¹ : FaithfulSMul R' T
inst✝ : IsScalarTower R R' T
⊢ Module.rank R R' ≤ Module.rank R T
Module: Mathlib.Data.Set.Card

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

Tactic:
rw [← encard_union_eq disjoint_sdiff_left, sdiff_union_self]

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

Goal state before:
pp: case neg
ι : 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 ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∑ i ∈ s \ t, f i • v i = ∑ i ∈ s \ (s \ t), f i • v i

Tactic:
simpa using

Goal state after:
case neg
ι : 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 ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∑ i ∈ s \ t, f i • v i = ∑ i ∈ t, f i • v i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : LinearIndependent R (-v)
⊢ LinearIndependent R v

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : LinearIndependent R (-v)
⊢ LinearIndependent R v
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard = s.encard - 1

Tactic:
rw [← encard_sdiff_singleton_add_one h,
    (ENat.addLECancellable_of_ne_top ENat.one_ne_top).add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard

Tactic:
refine s.eq_empty_or_nonempty.elim Or.inl (Or.inr ∘ fun ⟨a,ha⟩ ↦
    (s.finite_or_infinite.elim (fun hfin ↦ Or.inr ⟨a, ha, ?_⟩) (Or.inl ∘ Infinite.encard_eq)))

Goal state after:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < s.encard
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
H : LinearIndependent R v
g : ι → R
⊢ ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
H : LinearIndependent R v
g : ι → R
⊢ ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ g, ∑ i, g i • v i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ g, ∑ i, g i • v i = 0 ∧ ∃ i, ¬g i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
hv : ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
f : ↑↑s → R
hf₀ : ∑ i, f i • v ↑i = 0
i : ↑↑s
⊢ f i = 0

Tactic:
simpa using

Goal state after:
case mpr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
hv : ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
f : ↑↑s → R
hf₀ : ∑ i, f i • v ↑i = 0
i : ↑↑s
⊢ f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ ¬LinearIndepOn R v ↑s ↔ ∃ f, ∑ i ∈ s, f i • v i = 0 ∧ ∃ i ∈ s, f i ≠ 0

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ ¬LinearIndepOn R v ↑s ↔ ∃ f, ∑ i ∈ s, f i • v i = 0 ∧ ∃ i ∈ s, ¬f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ ∑ i ∈ t.preimage Subtype.val ⋯, g ↑i • v ↑i = 0

Tactic:
rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ ∀ x ∈ t, x ∉ range Subtype.val → g x • v x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
t : Finset ↑s
g : ↑s → R
h0 : ∑ i ∈ t, g i • v ↑i = 0
i : ↑s
hit : i ∈ t
⊢ ∀ (i : ι) (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
t : Finset ↑s
g : ↑s → R
h0 : ∑ i ∈ t, g i • v ↑i = 0
i : ↑s
hit : i ∈ t
⊢ ∀ (i : ι) (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
⊢ ∀ i ∈ t, g i = 0

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
⊢ ∀ i ∈ t, g i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : ↑n + 1 ≤ t₀.encard
⊢ False

Tactic:
rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk

Goal state after:
α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : n + 1 ≤ n
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
P Q : Set α
x✝¹ x✝ : ↑(P ↓∩ Q)
h :
  (fun x ↦
        match x with
        | ⟨⟨x, property⟩, hx⟩ => ⟨x, hx⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨⟨x, property⟩, hx⟩ => ⟨x, hx⟩)
      x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
α : Type u_1
P Q : Set α
x✝¹ x✝ : ↑(P ↓∩ Q)
h :
  (fun x ↦
        match x with
        | ⟨⟨x, property⟩, hx⟩ => ⟨x, hx⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨⟨x, property⟩, hx⟩ => ⟨x, hx⟩)
      x✝
⊢ x✝¹ = x✝
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x = 0
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ False

Tactic:
simpa using

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x = 0
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ False
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
p : α → Prop
this : Fintype α
⊢ Nat.card { x // p x } ≤ Nat.card α

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Finite α
p : α → Prop
this : Fintype α
⊢ Fintype.card { x // p x } ≤ Fintype.card α
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card { x // p x } < Nat.card α

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Fintype.card { x // p x } < Fintype.card α
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case neg
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : ¬j = i
⊢ Function.update x i 1 j = 1

Tactic:
simpa using

Goal state after:
case neg
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : ¬j = i
⊢ x j = 1
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : ¬j = i
⊢ j ∉ insert i I

Tactic:
simpa using

Goal state after:
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : ¬j = i
⊢ j ∉ I