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

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₂).support, x ∈ s

Tactic:
simpa using

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ∀ (x : ι) (x_1 : x ∈ s), ¬l₂ ⟨x, ⋯⟩ = 0 → x ∈ s
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: n : ℕ
R : Type u_3
inst✝ : CommSemiring R
a b : R
⊢ ∑ s, a ^ #s * b ^ (n - #s) = (a + b) ^ n

Tactic:
simpa using

Goal state after:
n : ℕ
R : Type u_3
inst✝ : CommSemiring R
a b : R
⊢ ∑ s, a ^ #s * b ^ (n - #s) = (a + b) ^ n
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = (partialProd g ∘ a.succ.succAbove) i.castSucc
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.succ = (partialProd g ∘ a.succ.succAbove) i.succ

Tactic:
simp only [Function.comp_apply, succ_succAbove_succ] at *

Goal state after:
case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.succ = partialProd g (a.succAbove i).succ
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k ∣ n * c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c

Tactic:
simpa using

Goal state after:
case inr.inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k ∣ n * c
hm : m > 0
hn : n > 0
⊢ k ∣ m.gcd n * c
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
⊢ (Finsupp.linearCombination R v) (Finsupp.single i c) = (Finsupp.linearCombination R v) (Finsupp.single j d)

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
⊢ c • v i = d • v j
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case mp
a b n k l : ℕ
h : k • n + a = l • n + b
⊢ a % n = b % n

Tactic:
simpa using

Goal state after:
case mp
a b n k l : ℕ
h : k • n + a = l • n + b
⊢ a % n = b % n
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoidWithOne M
inst✝ : CharZero M
a b n : ℕ
⊢ ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoidWithOne M
inst✝ : CharZero M
a b n : ℕ
⊢ ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

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✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ Disjoint {x} s

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ x ∉ s
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

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✝ : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
w : (Finsupp.linearCombination R v) f = v x
⊢ ∀ x ∈ Finsupp.supported R R ↑f.support, (Finsupp.linearCombination R v) x ≠ (Finsupp.linearCombination R v) f

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
w : (Finsupp.linearCombination R v) f = v x
⊢ ∀ x ∈ Finsupp.supported R R ↑f.support, ¬(Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) f
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
f : M →ₗ[R] M'
hs : LinearIndepOn R id s
hf_inj : InjOn ⇑f ↑(span R s)
⊢ InjOn ⇑f ↑(span R (id '' s))

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
f : M →ₗ[R] M'
hs : LinearIndepOn R id s
hf_inj : InjOn ⇑f ↑(span R s)
⊢ InjOn ⇑f ↑(span R s)
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✝ : Nontrivial R
hv : LinearIndependent R v
i : ι
hi : v i ∈ span R (v '' {i}ᶜ)
⊢ 1 • v i ∈ span R (v '' (univ \ {i}))

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
i : ι
hi : v i ∈ span R (v '' {i}ᶜ)
⊢ v i ∈ span R (v '' (univ \ {i}))
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
i : ι
inst✝ : Nontrivial R
hv : LinearIndepOn R v s
hi : i ∈ s
hi' : v i ∈ span R (v '' (s \ {i}))
⊢ 1 • v i ∈ span R (v '' (s \ {i}))

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
i : ι
inst✝ : Nontrivial R
hv : LinearIndepOn R v s
hi : i ∈ s
hi' : v i ∈ span R (v '' (s \ {i}))
⊢ v i ∈ span R (v '' (s \ {i}))
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
i : ι
inst✝ : Nontrivial R
hv : LinearIndepOn R v (insert i s)
hi : i ∉ s
⊢ v i ∉ span R (v '' s)

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
i : ι
inst✝ : Nontrivial R
hv : LinearIndepOn R v (insert i s)
hi : i ∉ s
⊢ v i ∉ span R (v '' s)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
p : Surjective fun i ↦ ⟨v i, ⋯⟩
q : (fun x ↦ ↑⟨v x, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range v = w

Tactic:
simpa using

Goal state after:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
p : Surjective fun i ↦ ⟨v i, ⋯⟩
q : (fun x ↦ ↑⟨v x, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range v = w
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]

Tactic:
simpa using

Goal state after:
m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ a * c ≡ b * c [MOD m]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inr
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
hm : m > 0
⊢ a ≡ b [MOD m]

Tactic:
simpa using

Goal state after:
case inr
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
hm : m > 0
⊢ a ≡ b [MOD m]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b c : ℕ
hmc : m.gcd c = 1
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]

Tactic:
simpa using

Goal state after:
m a b c : ℕ
hmc : m.gcd c = 1
h : a * c ≡ b * c [MOD m]
⊢ a * c ≡ b * c [MOD m]
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1.refine_1
ι : 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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ s
⊢ f i = 0

Tactic:
simpa using

Goal state after:
case refine_1.refine_1
ι : 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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ s
⊢ f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1.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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0

Tactic:
simpa using

Goal state after:
case refine_1.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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n : ℕ
co : n.Coprime m
a b z : ℕ
hzan : z ≡ a [MOD n]
hzbm : z ≡ b [MOD m]
⊢ z ≡ ↑(chineseRemainder co a b) [MOD n * m]

Tactic:
simpa using

Goal state after:
m n : ℕ
co : n.Coprime m
a b z : ℕ
hzan : z ≡ a [MOD n]
hzbm : z ≡ b [MOD m]
⊢ z ≡ ↑(chineseRemainder co a b) [MOD n * m]
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin 0 → ℕ
⊢ IsEmpty (Fin (∑ i, n i))

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin 0 → ℕ
⊢ IsEmpty (Fin 0)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n m : ℕ
⊢ n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1

Tactic:
simpa using

Goal state after:
n m : ℕ
⊢ n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n : ℕ
⊢ n % 4 = 1 → n % 2 = 1

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ n % 4 = 1 → n % 2 = 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n : ℕ
⊢ n % 4 = 3 → n % 2 = 1

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ n % 4 = 3 → n % 2 = 1
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ IsEmpty (Fin ↑ij.fst)

Tactic:
simpa using

Goal state after:
n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ IsEmpty (Fin 0)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case pos
ι : 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
this✝ : Sub R := ⋯
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : g i ≤ f i
⊢ f i ≤ g i

Tactic:
simpa using

Goal state after:
case pos
ι : 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
this✝ : Sub R := ⋯
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : g i ≤ f i
⊢ f i ≤ g i
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
this✝ : Sub R := ⋯
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
⊢ g i ≤ f 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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
⊢ False
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
n : ℕ
f : α ≃ Fin n
⊢ Nat.card α = n

Tactic:
simpa using

Goal state after:
α : Type u_3
n : ℕ
f : α ≃ Fin n
⊢ Nat.card α = n
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Fintype α
⊢ α ≃ Fin (Nat.card α)

Tactic:
simpa using

Goal state after:
case inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Fintype α
⊢ α ≃ Fin (Fintype.card α)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
h : 3 ≤ card α
x y : α
⊢ 3 ≤ #α

Tactic:
simpa using

Goal state after:
α : Type u_1
h : 3 ≤ card α
x y : α
⊢ 3 ≤ #α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inl.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Infinite β
⊢ card α ≠ 0

Tactic:
rwa [card_ne_zero_iff_nonempty]

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
ι : Type v
v : ι → M
hv : LinearIndependent R v
⊢ #ι ≤ 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
inst✝ : Nontrivial R
ι : Type v
v : ι → M
hv : LinearIndependent R v
⊢ #ι ≤ Module.rank R M
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
ι : Type u_1
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
⊢ s.encard ≤ toENat (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
inst✝ : Nontrivial R
ι : Type u_1
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
⊢ s.encard ≤ toENat (Module.rank R M)
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
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
⊢ ?m.41 < iSup ?m.43

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
⊢ ?m.41 < iSup ?m.43
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
c : Cardinal.{v}
h : c < Module.rank R M
⊢ ∃ s, #↑s = c ∧ LinearIndepOn R id s

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{v}
h : c < Module.rank R M
⊢ ∃ s, #↑s = c ∧ LinearIndepOn R id s
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).card = n + 1

Tactic:
simpa using

Goal state after:
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
⊢ t.card = n + 1
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:
simpa using

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

Goal state before:
pp: case refine_2.refine_1
ι : 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 ι
t₁ t₂ : Finset ι
f : ι → R
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
i : ι
hi : i ∈ t₁
⊢ f i = 0

Tactic:
simpa using

Goal state after:
case refine_2.refine_1
ι : 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 ι
t₁ t₂ : Finset ι
f : ι → R
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
i : ι
hi : i ∈ t₁
⊢ f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2.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 ι
inst✝ : Fintype ι
t₁ t₂ : Finset ι
f : ι → R
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
i : ι
hi : i ∈ t₂
⊢ f i = 0

Tactic:
simpa using

Goal state after:
case refine_2.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 ι
inst✝ : Fintype ι
t₁ t₂ : Finset ι
f : ι → R
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
i : ι
hi : i ∈ t₂
⊢ f i = 0
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:
simpa using

Goal state after:
ι : 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 ι
⊢ (∀ (l : ι →₀ R), v default = 0 → l default = 0) → ¬v default = 0
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:
simpa using

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

Goal state before:
pp: case refine_2
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
⊢ LinearIndepOn R id ↑(Finset.map { toFun := v, inj' := ⋯ } Finset.univ)

Tactic:
simpa using

Goal state after:
case refine_2
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
⊢ LinearIndepOn R id (range fun a ↦ v a)
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:
← Cardinal.one_le_iff_ne_zero,

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h✝ : Module.rank R M ≠ 0
h : 1 ≤ Module.rank R M
⊢ ?m.16
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:
simpa using

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