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

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k

Tactic:
by

Goal state after:
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) l = v i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m n : ℕ
⊢ Fintype.card (Fin n → Fin m) = Fintype.card (Fin (m ^ n))

Tactic:
by

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

Goal state before:
pp: m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a ≡ b [MOD m]

Tactic:
by

Goal state after:
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, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
⊢ (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : 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
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
⊢ (Subtype.val ∘ fun i ↦ ⟨v i, ⋯⟩) = v

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m n : ℕ
f : Fin n → Fin m
⊢ ∑ i, ↑(f i) * m ^ ↑i < m ^ n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : 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
⊢ i.Maximal ↔ ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ n)
b : Fin n
⊢ ↑a / m ^ ↑b % m < m

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : ℕ
h : b ≤ a
⊢ ↑(a - b) ∣ ↑a - ↑b

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ a ≡ b [MOD 0] ↔ a = b

Tactic:
by

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

Goal state before:
pp: n a : ℕ
⊢ n + a ≡ a [MOD n]

Tactic:
by

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

Goal state before:
pp: n a : ℕ
⊢ a + n ≡ a [MOD n]

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
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
⊢ Surjective ⇑f

Tactic:
by

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

Goal state before:
pp: n a b : ℕ
h : a ≤ b
⊢ a ≡ b [MOD n] ↔ ∃ t, b = a + n * t

Tactic:
by

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

Goal state before:
pp: m a b : ℕ
h1 : a ≡ b [MOD m]
h2 : a < b + m
h3 : b ≤ a
⊢ a - b < m

Tactic:
by

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

Goal state before:
pp: m a b : ℕ
h1 : a ≡ b [MOD m]
h2 : a < b
⊢ a + m < b + m

Tactic:
by

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

Goal state before:
pp: m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ d ∣ a ↔ d ∣ b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ a = b

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
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
⊢ s = t

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
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
⊢ s ⊆ t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ n)
⊢ (fun f ↦ ⟨∑ i, ↑(f i) * m ^ ↑i, ⋯⟩) ((fun a b ↦ ⟨↑a / m ^ ↑b % m, ⋯⟩) a) = a

Tactic:
by

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

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

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✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : ∑ i, f i • v i = ∑ i, g i • v i
i : ι
⊢ f i = g i

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : f.ker = ⊥
⊢ Disjoint (span R (range v)) f.ker

Tactic:
by

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ Fintype.card ((i : Fin m) → Fin (n i)) = Fintype.card (Fin (∏ i, n i))

Tactic:
by

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

Tactic:
by

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

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
this :
  ∀ (n : Fin m → ℕ) (nn : ℕ) (f : (i : Fin m) → Fin (n i)) (fn : Fin nn),
    ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * nn
⊢ ∑ i, ↑(f i.castSucc) * ∏ j, n (Fin.castLE ⋯ j) + ↑(f (Fin.last m)) * ∏ j, n (Fin.castLE ⋯ j) <
    (∏ i, n i.castSucc) * n (Fin.last 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
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ LinearIndependent R' (⇑j ∘ v)

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : f.ker = ⊥
⊢ Disjoint (span R (Set.range v)) f.ker

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x, g x.succ • v x = 0
⊢ g 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : LinearIndependent R v
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
⊢ LinearIndependent R (Fin.cons x v)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
⊢ LinearIndependent R (Fin.snoc v x)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i, n i)
b : Fin m
⊢ (↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b < n b

Tactic:
by

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
⊢ (match n.xgcd m with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      a [MOD n] ∧
    (match n.xgcd m with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      b [MOD m]

Tactic:
by

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) +
      ∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i) =
    0

Tactic:
by

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

Goal state before:
pp: m n a✝ b✝ c d : ℕ
co : n.Coprime m
a b : ℕ
⊢ a ≡ b [MOD n.gcd m]

Tactic:
by

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

Goal state before:
pp: m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(chineseRemainder' h) < n.lcm m

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ 0 * b = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : c = 0
⊢ ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ a % c + b % c < c * 2

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
⊢ ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ Function.RightInverse (fun a b ↦ ⟨(↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b, ⋯⟩) fun f ↦
    ⟨∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j), ⋯⟩

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = a % c + b % c

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
hc : c ≤ a % c + b % c
⊢ (a + b) % c + c = a % c + b % c

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
hc0 : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
hca : c ∣ a
h : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ a % c + b % c < c

Tactic:
by

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)
⊢ ↑(finPiFinEquiv (Pi.single i j)) = ↑j * ∏ j, n (Fin.castLE ⋯ j)

Tactic:
by

Goal state after:
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 Fin.isEmpty'

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

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

Goal state before:
pp: a b c : ℕ
hca : c ∣ b
⊢ (a + b) / c = a / c + b / c

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
hc : c ≤ a % c + b % c
hc0 : 0 < c
⊢ (a + b) / c = a / c + b / c + 1

Tactic:
by

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
⊢ ?m.326

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
⊢ (a + b) / c ≤ a / c + b / c + 1

Tactic:
by

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

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

Goal state before:
pp: case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (a - b) % n

Tactic:
nth_rw 2 [← div_add_mod a n]

Goal state after:
case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (n * (a / n) + a % n - b) % n
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b n : ℕ
h : b ≤ a % n
⊢ a % n - b = (a - b) % n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
h : n = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ 1 ≤ m

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ (fun x ↦ 2 * x) (m * n / 2) = (fun x ↦ 2 * x) (m * (n / 2) + m / 2)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3

Tactic:
by

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

Goal state before:
pp: n : ℕ
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
hn : n % 2 = 1
⊢ 0 < 4

Tactic:
by

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

Goal state before:
pp: n : ℕ
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
hn : n % 2 = 1
⊢ 2 ∣ 4

Tactic:
by

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

Goal state before:
pp: n a b : ℕ
h : a / n = b / n
⊢ a ≡ b [MOD n] ↔ a = b

Tactic:
by

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

Goal state before:
pp: m : ℕ
n : Fin m → ℕ
k : (i : Fin m) × Fin (n i)
⊢ ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd

Tactic:
by

Goal state after:
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 Fin.isEmpty'

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

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

Tactic:
by

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

Goal state before:
pp: n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ ↑(finSigmaFinEquiv ij) = ↑ij.snd

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ x < 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ ¬↑n ∣ x

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ 0 < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
⊢ ↑↑x = (x % ↑n).toNat

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 → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : i < n
⊢ i < (ofFn f).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
x✝² x✝¹ x✝ : Fin n
a : ℕ
isLt✝² : a < n
b : ℕ
isLt✝¹ : b < n
c : ℕ
isLt✝ : c < n
⊢ a * b * c ≡ a * (b * c) [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
x✝² x✝¹ x✝ : Fin n
a : ℕ
isLt✝² : a < n
b : ℕ
isLt✝¹ : b < n
c : ℕ
isLt✝ : c < n
⊢ a * (b + c) ≡ a * b + a * c [MOD n]

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 → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : i < n
this : i < (ofFn f).length
⊢ {j | ↑j < i + 1} = insert ⟨i, h⟩ {j | ↑j < i}

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
a b c : Fin n
⊢ (a + b) * c = a * c + b * c

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : Fintype (ZMod n)
⊢ Fintype.card (ZMod n) = n

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 → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < n
⊢ take i (ofFn f) = take i.succ (ofFn f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Nat.card ↥s = s.card

Tactic:
by

Goal state after: