mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case ha
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ 0 ≤ h i

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h0
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∀ i_1 ∈ s \ {i}, 0 ≤ h i_1

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i✝ : ι
f g h : ι → R
hi : i✝ ∈ s
h2i : g i✝ + h i✝ ≤ f i✝
hgf : ∀ j ∈ s, j ≠ i✝ → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i✝ → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
i : ι
a✝ : i ∈ s \ {i✝}
⊢ h i ≤ f i

Tactic:
aesop

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, ↑a ∈ v.support

Tactic:
aesop

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ a₁ ∈ (subtypeDomain p v).support, ∀ a₂ ∈ (subtypeDomain p v).support, ↑a₁ = ↑a₂ → a₁ = a₂

Tactic:
aesop

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

Goal state before:
pp: case refine_3
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ b ∈ v.support, ∃ a, ∃ (_ : a ∈ (subtypeDomain p v).support), ↑a = b

Tactic:
aesop

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

Goal state before:
pp: case refine_4
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, (fun a b ↦ h (↑a) b) a ((subtypeDomain p v) a) = h (↑a) (v ↑a)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α →₀ β →₀ M
⊢ ∀ (a : α × β), a ∈ f.support.disjiUnion (fun a ↦ map (Embedding.sectR a β) (f a).support) ⋯ ↔ (f a.1) a.2 ≠ 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f g : ι → M
s : Finset ι
inst✝ : MulLeftStrictMono M
hs : s.Nonempty
hlt : ∀ i ∈ s, f i < g i
⊢ s.val ≠ ∅

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
⊢ x ∈ Set.range (embDomain f) ↔ ↑x.support ⊆ Set.range ⇑f

Tactic:
convert! mem_range_mapDomain_iff _ f.injective _

Goal state after:
case e'_1.e'_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
⊢ embDomain f = mapDomain ⇑f

case e'_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
⊢ ↑x.support ⊆ Set.range ⇑f ↔ ∀ b ∉ Set.range ⇑f, x b = 0
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: N : Type u_2
inst✝³ : CommMonoid N
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G N
inst✝ : Fintype G
b : N
g : G
⊢ g • ∏ h, h • b = ∏ h, h • b

Tactic:
by
  simp only [smul_prod', smul_smul]
  exact Finset.prod_bijective (g * ·) (Group.mulLeft_bijective g) (by simp) (fun _ _ ↦ rfl)

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ f a • Pi.single a c a = f a • c

pp: case h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ ∀ (b : α), f b ≠ 0 → b ≠ a → f b • Pi.single a c b = 0

pp: case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ f a = 0 → 0 • Pi.single a c a = 0

Tactic:
Pi.single_eq_same

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ f a • c = f a • c

case h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ ∀ (b : α), f b ≠ 0 → b ≠ a → f b • Pi.single a c b = 0

case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ f a = 0 → 0 • Pi.single a c a = 0
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
f : M →ₗ[R] M'
⊢ linearCombination R (⇑f ∘ v) = f ∘ₗ linearCombination R v

Tactic:
by
  ext
  simp [linearCombination_apply]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr ((linearCombination R ⇑b) v) = v

Tactic:
← b.coe_repr_symm

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr (↑b.repr.symm v) = v
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ (linearCombination R ⇑b) (b.repr x) = x

Tactic:
← b.coe_repr_symm

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ ↑b.repr.symm (b.repr x) = x
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ (linearCombination R A) ((linearCombination R B) f) = (linearCombination R fun b ↦ (linearCombination R A) (B b)) f

Tactic:
classical
  simp only [linearCombination_apply]
  induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case hs
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∃ i ∈ hf.toFinset, 1 < f i

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
v : α → M
f : α' → α
⊢ linearCombination R (v ∘ f) = linearCombination R v ∘ₗ lmapDomain R R f

Tactic:
by
  ext
  simp [linearCombination_apply]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
⊢ ∃ x ∈ s, f x ≠ 1

Tactic:
by
  by_contra! h'
  exact h (finprod_mem_of_eqOn_one h')

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝¹ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : ↥t → R
hx : ∑ i, c i • v ↑i = x
a : ↥t
x✝ : a ∈ Finset.univ
⊢ v ↑a ∈ v '' s

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ n - ↑a - 1 = n - 1 - ↑a

Tactic:
Nat.sub_right_comm

Goal state after:
n : ℕ
a : Fin n
⊢ n - 1 - ↑a = n - 1 - ↑a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (support fun x ↦ r * f x) = support f

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (support fun x ↦ f x * r) = support f

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case h
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ Finite.toFinset ⋯ ⊆ Finite.toFinset ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case hf
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ ∀ x ∈ Finite.toFinset ⋯, x ∉ Finite.toFinset ⋯ → f x a = 1

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), (a, a_1) ∈ {x ∈ s | x.1 = a}

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ {x ∈ s | x.1 = a}, a_1.2 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), (a, a_1).2 = a_1

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ {x ∈ s | x.1 = a}, (a, a_1.2) = a_1

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_5
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, a_1) = f (a, a_1)

Tactic:
aesop

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

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

Tactic:
simp only [h, if_true, mk_coord_apply_eq i]

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
hv : LinearIndependent R v
i : ι
⊢ Injective fun r ↦ r • v i

Tactic:
convert! hv.comp (Finsupp.single_injective i)

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
hv : LinearIndependent R v
i : ι
x✝ : R
⊢ x✝ • v i = (⇑(Finsupp.linearCombination R v) ∘ Finsupp.single i) x✝
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
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ (Finsupp.single j (f j)) i = 0

Tactic:
Finsupp.single_eq_of_ne' hji

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
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ 0 = 0
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
⊢ x ^ y = 1 ↔ x = 1 ∨ y = 0

Tactic:
refine ⟨fun h ↦ or_iff_not_imp_right.2 fun y_0 ↦ ?_, fun h ↦ by rcases h with h | h <;> simp [h]⟩

Goal state after:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
⊢ x = 1
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
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (if i ∈ s then f i else 0) • v i = ∑ i ∈ s, (if i ∈ s then g i else 0) • v i

Tactic:
by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]

Goal state after:
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
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
t : Finset ↑s
x : ↥t
⊢ ∀ ⦃a₂ : ↥t⦄, (fun x ↦ ⟨↑↑x, ⋯⟩) x = (fun x ↦ ⟨↑↑x, ⋯⟩) a₂ → x = a₂

Tactic:
aesop

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hfv : Injective ⇑(Finsupp.linearCombination R (⇑f ∘ v))
⊢ LinearIndependent R v

Tactic:
Finsupp.linearCombination_linear_comp,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hfv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ LinearIndependent R v
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ Injective ⇑(Finsupp.linearCombination R (⇑f ∘ v)) ↔ Injective ⇑(Finsupp.linearCombination R v)

Tactic:
Finsupp.linearCombination_linear_comp,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ Injective ⇑(f ∘ₗ Finsupp.linearCombination R v) ↔ Injective ⇑(Finsupp.linearCombination R v)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ ↑m • p + a = ↑n • p + b

Tactic:
exact mod_cast h

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
x✝ : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)
⊢ x✝.1 ∈ s

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
exact h.map (Nat.castAddMonoidHom M)

Goal state after:
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
⊢ (Finsupp.linearCombination R v) f ≠ v x

Tactic:
replace h : x ∉ (f.support : Set ι) := h

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
⊢ (Finsupp.linearCombination R v) f ≠ v x
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ↑(Pi.single i j i) * m ^ ↑i = ↑j * m ^ ↑i

pp: m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∀ (x : Fin n), x ≠ i → ↑(Pi.single i j x) * m ^ ↑x = 0

Tactic:
Pi.single_eq_same

Goal state after:
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ↑j * m ^ ↑i = ↑j * m ^ ↑i

m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∀ (x : Fin n), x ≠ i → ↑(Pi.single i j x) * m ^ ↑x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2.specialize_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
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ Disjoint ({i ∈ s | g i ≤ f i}) ({i ∈ s | f i < g i})

Tactic:
simp_rw [Finset.disjoint_left, Finset.mem_filter]
      exact fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt hi'

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ↑(Pi.single i j i) * ∏ j, n (Fin.castLE ⋯ j) = ↑j * ∏ j, n (Fin.castLE ⋯ j)

pp: m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j, n (Fin.castLE ⋯ j) = 0

Tactic:
Pi.single_eq_same

Goal state after:
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ↑j * ∏ j, n (Fin.castLE ⋯ j) = ↑j * ∏ j, n (Fin.castLE ⋯ j)

m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j, n (Fin.castLE ⋯ j) = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
⊢ False

Tactic:
by
    have : (a + b) % c = a % c + b % c := add_mod_of_add_mod_lt (lt_of_not_ge hc)
    simp_all [dvd_iff_mod_eq_zero]

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

Goal state before:
pp: case e'_4
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hdj : Disjoint s t
h : LinearIndepOn R v (s ∪ t)
⊢ v '' s = (fun x ↦ v ↑x) '' Subtype.val ⁻¹' s

Tactic:
aesop

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

Goal state before:
pp: case e'_5
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hdj : Disjoint s t
h : LinearIndepOn R v (s ∪ t)
⊢ v '' t = (fun x ↦ v ↑x) '' Subtype.val ⁻¹' t

Tactic:
aesop

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: n : ℕ
c : Cardinal.{u_3}
⊢ ↑n ≤ toENat c ∧ toENat c ≤ ↑n ↔ ↑n ≤ c ∧ c ≤ ↑n

Tactic:
Cardinal.toENat_le_natCast,

Goal state after:
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n ≤ toENat c ∧ c ≤ ↑n ↔ ↑n ≤ c ∧ c ≤ ↑n
Module: Mathlib.Data.Set.Card

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

Tactic:
rw [← encard_lt_top_iff]

Goal state after:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ s.encard < ⊤
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ 1 + 1 + 1 = 3

Tactic:
aesop

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ y ∉ {z}

Tactic:
aesop

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ x ∉ {y, z}

Tactic:
aesop

Goal state after:
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 : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
⊢ l i = 0 i

Tactic:
simp only [Finsupp.zero_apply]

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 : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
⊢ l i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case e'_2
k : ℕ
⊢ {i | i < k}.encard = (↑(Finset.range k)).encard

pp: case e'_3
k : ℕ
⊢ ↑k = ↑(Finset.range k).card

Tactic:
· rw [Finset.coe_range, Iio_def]

Goal state after:
case e'_3
k : ℕ
⊢ ↑k = ↑(Finset.range k).card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
hs : ∅.ncard ≠ 0
⊢ False

Tactic:
simp at hs

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).ncard ≤ 1

Tactic:
rw [← Nat.cast_le (α := ℕ∞), (toFinite _).cast_ncard_eq, Nat.cast_one]

Goal state after:
α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).encard ≤ 1
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i x✝ : ι
⊢ (mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr) ((restrictScalars R b) x✝) =
    ((↑R ↑b.repr).domRestrict (span R (range ⇑b))) ((restrictScalars R b) x✝)

Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply, map_one,
    Basis.repr_self, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single,
    Algebra.linearMap_apply, LinearMap.domRestrict_apply,
    Basis.restrictScalars_apply, LinearMap.coe_restrictScalars]

Goal state after: