mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)

Tactic:
exact fun H => H.1 rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
        (∑ i ∈ insert a s, g i).support = (insert a s).biUnion fun i ↦ (g i).support

Tactic:
intro i

Goal state after:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
⊢ ∀ (s : Finset ι),
    i ∉ s →
      ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
        (∑ i ∈ insert i s, g i).support = (insert i s).biUnion fun i ↦ (g i).support
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
n : ℕ
⊢ abv ↑n ≤ ↑n

Tactic:
cases subsingleton_or_nontrivial R
  · simp [Subsingleton.eq_zero (α := R)]
  induction n with
  | zero => simp
  | succ n ih =>
  · grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∀ x ∈ s, x ∉ (indicator s f).support → single x ((indicator s f) x) = 0

Tactic:
intro i

Goal state after:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
⊢ i ∈ s → i ∉ (indicator s f).support → single i ((indicator s f) i) = 0
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h₂.h0
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ ∀ (i : ι), i ∈ s → 0 ≤ f i

Tactic:
intro i

Goal state after:
case h₂.h0
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
⊢ i ∈ s → 0 ≤ f i
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ ∀ (i : ι), i ∈ s → f i ≤ g i

Tactic:
intro i

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
⊢ i ∈ s → f i ≤ g i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
⊢ (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)

Tactic:
by
  classical
    refine Finset.induction_on s
      (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) ?_
    intro a s ha ih H
    have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
    rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
      forall_mem_insert, ih this]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #s ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
← Finset.card_filter_add_card_filter_not fun i ↦ f i = ∅,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #({i ∈ s | f i = ∅}) + #({a ∈ s | ¬f a = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
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✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x

Tactic:
have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
  classical calc
    ∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x := by
      rw [← prod_union, filter_union_filter_not_eq]
      exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
    _ ≤ ∏ x ∈ t, f x :=
      mul_le_of_le_one_of_le
        (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
        (prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp])

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
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
⊢ ∀ (a : ι), a ∈ l.splitSupport ↔ g a (l.split a) ≠ 0

Tactic:
intro i

Goal state after:
α : 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
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
i : ι
⊢ i ∈ l.splitSupport ↔ g i (l.split i) ≠ 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
⊢ ¬(mapDomain f x) t = 0 → ∃ a ∈ x.support, f a = t

pp: case refine_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
x✝ : ∃ a ∈ x.support, f a = t
i : α
i_in : i ∈ x.support
hi : f i = t
⊢ ¬(mapDomain f x) t = 0

Tactic:
· simpa [mapDomain, sum, single_apply] using fun i h h' _ ↦ ⟨i, h, h'⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
x✝ : ∃ a ∈ x.support, f a = t
i : α
i_in : i ∈ x.support
hi : f i = t
⊢ ¬(mapDomain f x) t = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Tactic:
have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ∀ (i : α), (h i) 0 = 0

Tactic:
intro i

Goal state after:
α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
i : α
⊢ (h i) 0 = 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ (fun i ↦ f i) = fun x ↦ 1

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case neg
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
⊢ ∏ᶠ (i : p), f i = 1

Tactic:
· have : IsEmpty p := ⟨h⟩
    exact finprod_of_isEmpty f

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

Goal state before:
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:
exact fun _ ↦ by simp only [zero_smul]

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

Goal state before:
pp: case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
⊢ ∀ (a : α), a ∈ s ∧ v a = x → x ∈ ↑(map (linearCombination R v) (supported R R s))

Tactic:
intro i

Goal state after:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
⊢ i ∈ s ∧ v i = x → x ∈ ↑(map (linearCombination R v) (supported R R s))
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
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ (linearCombination R v) (single i 1) = x

Tactic:
simp [hi.2]

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (i : ι), (fun i_1 ↦ (b.reindexRange.repr (b i)) ⟨b i_1, ⋯⟩) = ⇑(single i 1)

Tactic:
intro i

Goal state after:
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
i✝ : ι
a✝ : Nontrivial R
i : ι
⊢ (fun i_1 ↦ (b.reindexRange.repr (b i)) ⟨b i_1, ⋯⟩) = ⇑(single i 1)
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 : Finset α
⊢ x ∈ span R (v '' ↑s) ↔ ∃ c, ∑ i ∈ s, c i • v i = x

Tactic:
rw [Submodule.mem_span_image_finset_iff_exists_fun]

Goal state after:
α : 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 : Finset α
⊢ (∃ c, ∑ i, c i • v ↑i = x) ↔ ∃ c, ∑ i ∈ s, c i • v i = x
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ #(Ioi a) = n - 1 - ↑a

Tactic:
rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioo, Nat.sub_right_comm]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u_1
h : 0 = 0 + 0
⊢ vecAlt0 h ![] = ![]

Tactic:
simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u_1
h : 0 = 0 + 0
⊢ vecAlt1 h ![] = ![]

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i

Tactic:
rw [finprod_mem_range]

Goal state after:
case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ Injective some
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
⊢ ⊤ = supported R R univ

Tactic:
Finsupp.supported_univ

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
⊢ ⊤ = ⊤
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
⊢ (↑b.repr).range = supported R R univ

Tactic:
by
  rw [LinearEquiv.range, Finsupp.supported_univ]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Icc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Icc a b, f (Fin.cast h i)

Tactic:
simp [← map_finCongr_Icc]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Icc a.succ b.succ, f i = ∏ i ∈ Icc a b, f i.succ

Tactic:
by
  simp [← map_succEmb_Icc]

Goal state after:
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),
    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:
intro i

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
⊢ 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
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
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v) l = ↑x
this✝ : ↑(↑hv.linearCombinationEquiv l) = (Finsupp.linearCombination R v) l
this : ↑hv.linearCombinationEquiv l = x
⊢ hv.repr x = l

Tactic:
rw [← LinearEquiv.symm_apply_apply hv.linearCombinationEquiv l]

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
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v) l = ↑x
this✝ : ↑(↑hv.linearCombinationEquiv l) = (Finsupp.linearCombination R v) l
this : ↑hv.linearCombinationEquiv l = x
⊢ hv.repr x = hv.linearCombinationEquiv.symm (hv.linearCombinationEquiv l)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
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
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
⊢ Surjective ⇑f

Tactic:
intro i

Goal state after:
ι : Type u'
ι' : Type u_1
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
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
⊢ ∃ a, f a = i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
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
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
⊢ (Finsupp.linearCombination R v) (Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)) = v i

Tactic:
rw [Finsupp.linearCombination_mapDomain]

Goal state after:
ι : Type u'
ι' : Type u_1
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
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
⊢ (Finsupp.linearCombination R (v ∘ ⇑f)) (repr ⟨v i, ⋯⟩) = v i
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m / ↑d ∣ ↑c / ↑d * (↑b - ↑a)

Tactic:
show (m / d : ℤ) ∣ c / d * (b - a)
    rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]
    apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)
    rw [Int.mul_sub]
    exact modEq_iff_dvd.mp h

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

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑(n.gcd m) ≠ 0

Tactic:
norm_cast

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ¬n.gcd m = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

Tactic:
norm_cast

Goal state after:
case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑n ∣ ↑(n.lcm m)

Tactic:
norm_cast

Goal state after:
case left.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ n ∣ n.lcm m
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

Tactic:
norm_cast

Goal state after:
case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case right.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑m ∣ ↑(n.lcm m)

Tactic:
norm_cast

Goal state after:
case right.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ m ∣ n.lcm m
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑(n.gcd m) ∣ ↑(n.gcd m) * ↑a

Tactic:
norm_cast

Goal state after:
case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ n.gcd m ∣ n.gcd m * a
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2.specialize_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
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
⊢ ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
      ∑ i ∈ s with f i < g i, f i • v i =
    ∑ i ∈ s with g i ≤ f i, g i • v i +
      ∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x)

Tactic:
convert! heq

Goal state after:
case e'_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
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
⊢ ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
      ∑ i ∈ s with f i < g i, f i • v i =
    ∑ i ∈ s, f i • v i

case e'_3
ι : 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
⊢ ∑ i ∈ s with g i ≤ f i, g i • v i +
      ∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x) =
    ∑ i ∈ s, g i • v i