mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.ModEq

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

pp: case inr
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hca : c ≤ a
⊢ a - c ≡ b - d [MOD n]

Tactic:
·

Goal state after:
case inl
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hac : a < c
⊢ a - c ≡ b - d [MOD n]
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
·

Goal state after:
case inr.inr
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k
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 ≤ k.castSucc

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

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 ≤ k.castSucc
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:
·

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: case mp
ι : 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

pp: case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ (∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j) → i.Maximal

Tactic:
·

Goal state after:
case mp
ι : 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
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
ih : ∀ (f : Fin n → Fin 0), ∑ i, ↑(f i) * 0 ^ ↑i < 0 ^ n
f : Fin (n + 1) → Fin 0
⊢ ∑ i, ↑(f i) * 0 ^ ↑i < 0 ^ (n + 1)

pp: case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ (n + 1)

Tactic:
·

Goal state after:
case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
ih : ∀ (f : Fin n → Fin 0), ∑ i, ↑(f i) * 0 ^ ↑i < 0 ^ n
f : Fin (n + 1) → Fin 0
⊢ ∑ i, ↑(f i) * 0 ^ ↑i < 0 ^ (n + 1)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ (∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j) → i.Maximal

Tactic:
·

Goal state after:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ (∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j) → i.Maximal
Module: Mathlib.Algebra.BigOperators.Fin

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

pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
b : Fin (n + 1)
⊢ ↑a / m ^ ↑b % m < m

Tactic:
·

Goal state after:
case zero
ι : Type u_1
M : Type u_2
m : ℕ
a : Fin (m ^ 0)
b : Fin 0
⊢ ↑a / m ^ ↑b % m < m
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a : Fin (0 ^ (n + 1))
⊢ ↑a / 0 ^ ↑b % 0 < 0

pp: case succ.succ
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
m : ℕ
a : Fin ((m + 1) ^ (n + 1))
⊢ ↑a / (m + 1) ^ ↑b % (m + 1) < m + 1

Tactic:
·

Goal state after:
case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a : Fin (0 ^ (n + 1))
⊢ ↑a / 0 ^ ↑b % 0 < 0
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
·

Goal state after:
case succ.succ
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
m : ℕ
a : Fin ((m + 1) ^ (n + 1))
⊢ ↑a / (m + 1) ^ ↑b % (m + 1) < m + 1
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 lia

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 lia

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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, f i = g i

Tactic:
·

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
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)

pp: case refine_2
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).gcd (↑c / ↑d) = 1

Tactic:
·

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
⊢ ∑ i ∈ s ∪ t, (if i ∈ s then f i else 0) • v i = ∑ i ∈ s ∪ t, (if i ∈ t then f i else 0) • v i

pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0

Tactic:
·

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
⊢ ∑ i ∈ s ∪ t, (if i ∈ s then f i else 0) • v i = ∑ i ∈ s ∪ t, (if i ∈ t then f i else 0) • v i
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case refine_2
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).gcd (↑c / ↑d) = 1

Tactic:
·

Goal state after:
case refine_2
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).gcd (↑c / ↑d) = 1
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
simpa [mul_comm] using h

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

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

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

Tactic:
·

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

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

Tactic:
simpa [mul_comm] using h

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0

Tactic:
refine ⟨fun i hi => ?_, fun i hi => ?_⟩

Goal state after:
case refine_1.refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ s
⊢ f i = 0

case refine_1.refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ a [MOD n]

pp: case right
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ b [MOD m]

Tactic:
·

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

Goal state before:
pp: case right
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ b [MOD m]

Tactic:
·

Goal state after:
case right
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ b [MOD m]
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1.refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ s
⊢ f i = 0

pp: case refine_1.refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0

Tactic:
·

Goal state after:
case refine_1.refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ s
⊢ f i = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n]

pp: case right
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ b [MOD m]

Tactic:
·

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

Goal state before:
pp: case right
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ b [MOD m]

Tactic:
·

Goal state after:
case right
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ b [MOD m]
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1.refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0

Tactic:
·

Goal state after:
case refine_1.refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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, f i = g i

Tactic:
·

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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, f i = g i
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})

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
⊢ ∑ i ∈ s with g i ≤ f i, (if g i ≤ f i then f i - g i else g i - f i) • v i =
    ∑ i ∈ s with f i < g i, (if g i ≤ f i then f i - g i else g i - f i) • v i

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
h :
  (∀ i ∈ {i ∈ s | g i ≤ f i}, (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ i ∈ {i ∈ s | f i < g i}, (if g i ≤ f i then f i - g i else g i - f i) = 0
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∀ i ∈ s, f i = g i

Tactic:
·

Goal state after:
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})
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.zero
ι : 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)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin 0
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * 0

pp: case succ.succ
ι : 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)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (n✝ + 1)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * (n✝ + 1)

Tactic:
·

Goal state after:
case succ.zero
ι : 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)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin 0
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * 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)

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

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)

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

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.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_1
ι : 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
⊢ LinearIndependent R v →
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))

pp: case refine_2
ι : 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
⊢ LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr)) →
    LinearIndependent R v

Tactic:
·

Goal state after:
case refine_1
ι : 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
⊢ LinearIndependent R v →
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))