mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ (∏ i, ∏ j with i ≤ j.castSucc, f i j) * ∏ i, ∏ j with j.castSucc < i, f i j =
    (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j = (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≥ i, f j.succ i

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≥ i, f j.succ i = ∏ i, ∏ j ≥ i, f i.castSucc j * f j.succ i

Tactic:
by

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

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ a ≡ b [PMOD p] ↔ ∃ i, i < n ∧ a ≡ b + i • p [PMOD n • p]

Tactic:
by

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

Goal state before:
pp: case succ
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
⊢ ∑ n_1, (-1) ^ ↑n_1 = if Even (n + 1) then 0 else 1

Tactic:
simp only [Fin.sum_univ_castSucc, Fin.val_castSucc, IH, Fin.val_last, Nat.even_add_one, ite_not]
    split_ifs with h
    · simp [*]
    · simp [(Nat.not_even_iff_odd.mp h).neg_pow]

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

Goal state before:
pp: R : Type u_3
inst✝ : Ring R
m : ℕ
⊢ ∑ n, (-1) ^ ↑n = if Even m then 0 else 1

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
f : Fin n → M
⊢ partialProd f 0 = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
f : Fin n → M
j : Fin n
⊢ partialProd f j.succ = partialProd f j.castSucc * f j

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
f : Fin (n + 1) → M
j : Fin (n + 1)
⊢ partialProd f j.succ = f 0 * partialProd (tail f) j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
⊢ (a.gcd b).gcd c = (a.gcd c).gcd b

Tactic:
gcd_assoc,

Goal state after:
a b c : ℕ
⊢ a.gcd (b.gcd c) = (a.gcd c).gcd b
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
⊢ a.gcd (b.gcd c) = (a.gcd c).gcd b

Tactic:
gcd_assoc,

Goal state after:
a b c : ℕ
⊢ a.gcd (b.gcd c) = a.gcd (c.gcd b)
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
⊢ (a.gcd b).gcd c = (a.gcd c).gcd b

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
⊢ partialProd (init f) 0 = partialProd f (castSucc 0)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
f : Fin (n + 1) → M
i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (init f) i.castSucc = partialProd f i.castSucc.castSucc
⊢ partialProd (init f) i.succ = partialProd f i.succ.castSucc

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x : Fin (n + 1)
⊢ (f 0 • partialProd fun i ↦ (f i.castSucc)⁻¹ * f i.succ) 0 = f 0

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : LinearIndependent R v
w : ι → G
⊢ LinearIndependent R (w • v)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : (f 0 • partialProd fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ (f 0 • partialProd fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : Fin n
⊢ (partialProd f i.castSucc)⁻¹ * partialProd f i.succ = f i

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : MulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m.Coprime n
⊢ m.lcm n = m * n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ m.Coprime (n + m) ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ m.Coprime (m + n) ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ (m + n).Coprime n ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ (m + n).Coprime m ↔ n.Coprime m

Tactic:
by

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
⊢ LinearIndepOn R v s ↔
    ∀ f ∈ Finsupp.supported R R s,
      ∀ g ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.Coprime (n + k * m) ↔ m.Coprime n

Tactic:
by

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
⊢ ¬LinearIndepOn R v s ↔
    ∃ f g,
      f ∈ Finsupp.supported R R s ∧
        g ∈ Finsupp.supported R R s ∧ (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g ∧ f ≠ g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.Coprime (n + m * k) ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.Coprime (k * m + n) ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.Coprime (m * k + n) ↔ m.Coprime n

Tactic:
by

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
⊢ LinearIndepOn R v s ↔ Injective ⇑(Finsupp.linearCombinationOn ι M R v s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (m + k * n).Coprime n ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (m + n * k).Coprime n ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (k * n + m).Coprime n ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (n * k + m).Coprime n ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
h : c ∣ b
⊢ (a + b).Coprime c ↔ a.Coprime c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
h : c ∣ a
⊢ (a + b).Coprime c ↔ b.Coprime c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
h : a ∣ c
⊢ a.Coprime (b + c) ↔ a.Coprime b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
h : a ∣ b
⊢ a.Coprime (b + c) ↔ a.Coprime c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ (n - m).Coprime m ↔ n.Coprime m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ m.Coprime (n - m) ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ (n - m).Coprime n ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ n.Coprime (n - m) ↔ n.Coprime m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n : ℕ
hn : 0 < n
a b : ℕ
⊢ (a ^ n).Coprime b ↔ a.Coprime b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n : ℕ
hn : 0 < n
a b : ℕ
⊢ a.Coprime (b ^ n) ↔ a.Coprime b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: ⊢ ¬Coprime 0 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n : ℕ
⊢ Coprime 1 n ↔ True

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n : ℕ
⊢ n.Coprime 1 ↔ True

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
hac : a.Coprime c
b_dvd_c : b ∣ c
⊢ (a * b).gcd c = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ m.Coprime n ↔ IsRelPrime m n

Tactic:
by

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ (ι →₀ R) ≃ₗ[R] ↥(span R (range v))

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
⊢ hv.repr.ker = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
⊢ a * m + b * n ≠ m * n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: x n m : ℕ
hcop : n.Coprime m
⊢ x.gcd n * x.gcd m = x ↔ x ∣ n * m

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
w : ι → Rˣ
⊢ LinearIndependent R (w • v)

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
⊢ hv.repr.range = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
⊢ k / m * (m / n) = k / n

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
by

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:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
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
⊢ ↑hv.linearCombinationEquiv l = x

Tactic:
by

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
⊢ Injective fun x ↦ ⟨x.1, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
⊢ (k / m).lcm (k / n) = k / m.gcd n

Tactic:
by

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

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

Goal state before:
pp: a b n : ℕ
⊢ a ≡ b [PMOD n] ↔ a ≡ b [MOD n]

Tactic:
by

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 [MOD n]
⊢ ↑a ≡ ↑b [PMOD ↑n]

Tactic:
by

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

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

Goal state before:
pp: n a : ℕ
⊢ a ≡ 0 [MOD n] ↔ n ∣ a

Tactic:
by

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

Goal state before:
pp: n a b : ℕ
⊢ a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a

Tactic:
by

Goal state after:
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
⊢ i = j

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n a b : ℕ
h : a ≤ b
⊢ a ≡ b [MOD n] ↔ n ∣ b - a

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v) l = ↑x
⊢ hv.repr x = l

Tactic:
by

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

Goal state before:
pp: n a b : ℕ
h : a ≡ b [MOD n]
⊢ n ∣ b - a

Tactic:
by

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

Goal state before:
pp: m a b : ℕ
⊢ m * a + b ≡ b [MOD m]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
x : ↥(span R (range v))
hx : ↑x = v i
⊢ hv.repr x = Finsupp.single i 1

Tactic:
by

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

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
⊢ Disjoint (span R (v '' s)) (span R (v '' t))

Tactic:
by

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

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n * c]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) = hv.repr x

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n]

Tactic:
by

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

Goal state before:
pp: n a b m : ℕ
h : a ≡ b [MOD n]
⊢ a ^ m ≡ b ^ m [MOD n]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ Span.repr R (range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)

Tactic:
by

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

Goal state before:
pp: n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ a + c ≡ b + d [MOD n]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
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
⊢ v x ∉ span R (v '' s)

Tactic:
by

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

Goal state before:
pp: n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ c ≡ d [MOD n]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : l ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
⊢ (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i a)

Tactic:
by

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
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:
by

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

Goal state before:
pp: n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
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:
by

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

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
hn : ¬a = 0
⊢ i ∈ ↑(Finsupp.single i a).support

Tactic:
by

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

Goal state before:
pp: n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
⊢ a - c ≡ b - d [MOD n]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
ha : a • v i ∈ span R (v '' (univ \ {i}))
⊢ a = 0

Tactic:
by

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

Goal state before:
pp: a b c m : ℕ
hc : c ≠ 0
⊢ c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]

Tactic:
by

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
i : ι
hv : LinearIndepOn R v s
hi : i ∈ s
a : R
ha : a • v i ∈ span R (v '' (s \ {i}))
⊢ a • v ↑⟨i, hi⟩ ∈ span R ((fun x ↦ v ↑x) '' (univ \ {⟨i, hi⟩}))

Tactic:
by

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

Goal state before:
pp: a b c m : ℕ
hc : c ≠ 0
⊢ a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n a b m : ℕ
h : a ≡ b [MOD m * n]
⊢ a ≡ b [MOD n]

Tactic:
by

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

Goal state before:
pp: case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j.succ ≤ k.castSucc.castSucc

Tactic:
le_iff_val_le_val,

Goal state after:
case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ ↑j.succ ≤ ↑k.castSucc.castSucc
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:
by

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
i : ι
inst✝ : Nontrivial R
hv : LinearIndepOn R v (insert i s)
hi : i ∉ s
⊢ v i ∉ span R (v '' s)

Tactic:
by

Goal state after: