mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_1
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ ((linearCombination R fun j ↦ single j 1 + single i (c j)) ∘ₗ
      linearCombination R fun j ↦ single j 1 - single i (c j)) =
    LinearMap.id

pp: case refine_2
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ ((linearCombination R fun j ↦ single j 1 - single i (c j)) ∘ₗ
      linearCombination R fun j ↦ single j 1 + single i (c j)) =
    LinearMap.id

Tactic:
<;>

Goal state after:
case refine_1
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ ((linearCombination R fun j ↦ single j 1 + single i (c j)) ∘ₗ
      linearCombination R fun j ↦ single j 1 - single i (c j)) =
    LinearMap.id

case refine_2
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ ((linearCombination R fun j ↦ single j 1 - single i (c j)) ∘ₗ
      linearCombination R fun j ↦ single j 1 + single i (c j)) =
    LinearMap.id
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_1
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
j k : ι
⊢ ((((linearCombination R fun j ↦ single j 1 + single i (c j)) ∘ₗ
            linearCombination R fun j ↦ single j 1 - single i (c j)) ∘ₗ
          lsingle j)
        1)
      k =
    ((LinearMap.id ∘ₗ lsingle j) 1) k

pp: case refine_2
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
j k : ι
⊢ ((((linearCombination R fun j ↦ single j 1 - single i (c j)) ∘ₗ
            linearCombination R fun j ↦ single j 1 + single i (c j)) ∘ₗ
          lsingle j)
        1)
      k =
    ((LinearMap.id ∘ₗ lsingle j) 1) k

Tactic:
<;>

Goal state after:
case refine_1
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
j k : ι
⊢ ((((linearCombination R fun j ↦ single j 1 + single i (c j)) ∘ₗ
            linearCombination R fun j ↦ single j 1 - single i (c j)) ∘ₗ
          lsingle j)
        1)
      k =
    ((LinearMap.id ∘ₗ lsingle j) 1) k

case refine_2
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
j k : ι
⊢ ((((linearCombination R fun j ↦ single j 1 - single i (c j)) ∘ₗ
            linearCombination R fun j ↦ single j 1 + single i (c j)) ∘ₗ
          lsingle j)
        1)
      k =
    ((LinearMap.id ∘ₗ lsingle j) 1) k
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case none
m n : ℕ
i : Fin (n + 1)
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) none) = none

pp: case some
m n : ℕ
i : Fin (n + 1)
val✝ : Fin n
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) (some val✝)) = some val✝

Tactic:
<;>

Goal state after:
case none
m n : ℕ
i : Fin (n + 1)
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) none) = none

case some
m n : ℕ
i : Fin (n + 1)
val✝ : Fin n
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) (some val✝)) = some val✝
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inl
m n : ℕ
y : Fin m
⊢ (fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inl y)) = Sum.inl y

pp: case inr
m n : ℕ
y : Fin n
⊢ (fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inr y)) = Sum.inr y

Tactic:
<;>

Goal state after:
case inl
m n : ℕ
y : Fin m
⊢ (fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inl y)) = Sum.inl y

case inr
m n : ℕ
y : Fin n
⊢ (fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inr y)) = Sum.inr y
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case refine_1
m n : ℕ
x : Fin (m + n)
i : Fin m
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Fin.castAdd n i)) = Fin.castAdd n i

pp: case refine_2
m n : ℕ
x : Fin (m + n)
i : Fin n
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Fin.natAdd m i)) = Fin.natAdd m i

Tactic:
<;>

Goal state after:
case refine_1
m n : ℕ
x : Fin (m + n)
i : Fin m
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Fin.castAdd n i)) = Fin.castAdd n i

case refine_2
m n : ℕ
x : Fin (m + n)
i : Fin n
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Fin.natAdd m i)) = Fin.natAdd m i
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case pos
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ v ⟨↑i + ↑i, ⋯⟩ = v (i + i)

pp: case neg
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ v ⟨↑i + ↑i - n, ⋯⟩ = v (i + i)

Tactic:
<;>

Goal state after:
case pos
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ v ⟨↑i + ↑i, ⋯⟩ = v (i + i)

case neg
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ v ⟨↑i + ↑i - n, ⋯⟩ = v (i + i)
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inl
n i : ℕ
val✝ : Fin n
⊢ (Sum.inl val✝).isRight = !(Sum.inl val✝).isLeft

pp: case inr
n i val✝ : ℕ
⊢ (Sum.inr val✝).isRight = !(Sum.inr val✝).isLeft

Tactic:
<;>

Goal state after:
case inl
n i : ℕ
val✝ : Fin n
⊢ (Sum.inl val✝).isRight = !(Sum.inl val✝).isLeft

case inr
n i val✝ : ℕ
⊢ (Sum.inr val✝).isRight = !(Sum.inr val✝).isLeft
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case pos
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ↑i + ↑i + 1 < n + 1 + 1
⊢ v ⟨↑i + ↑i + 1, ⋯⟩ = v (i + i + 1)

pp: case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ v ⟨↑i + ↑i + 1 - (n + 1 + 1), ⋯⟩ = v (i + i + 1)

Tactic:
<;>

Goal state after:
case pos
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ↑i + ↑i + 1 < n + 1 + 1
⊢ v ⟨↑i + ↑i + 1, ⋯⟩ = v (i + i + 1)

case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ v ⟨↑i + ↑i + 1 - (n + 1 + 1), ⋯⟩ = v (i + i + 1)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∈ s
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∉ s
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∈ s
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∉ s
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∈ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∉ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∈ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∉ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
Module: Mathlib.Algebra.BigOperators.Finprod

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

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

Tactic:
<;>

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

case hf
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ ∀ x ∈ Finite.toFinset ⋯, x ∉ Finite.toFinset ⋯ → f x a = 1
Module: Mathlib.Algebra.BigOperators.Finprod

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

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

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

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

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

Tactic:
<;>

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

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

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

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

case refine_5
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, a_1) = f (a, a_1)
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:
LinearEquiv.range,

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
⊢ ⊤ = supported R R univ
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬x = 1

pp: case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬x = 0

pp: case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬⊤ < ⊤

Tactic:
<;>

Goal state after:
case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬x = 1

case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬x = 0

case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬⊤ < ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y : ℕ∞
h : x = 1
⊢ x ^ y = 1

pp: case inr
x y : ℕ∞
h : y = 0
⊢ x ^ y = 1

Tactic:
<;>

Goal state after:
case inl
x y : ℕ∞
h : x = 1
⊢ x ^ y = 1

case inr
x y : ℕ∞
h : y = 0
⊢ x ^ y = 1
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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∀ x ∈ f.support ∪ g.support, x ∉ g.support → g x • v x = 0

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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∀ x ∈ f.support ∪ g.support, x ∉ f.support → f x • v x = 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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∀ x ∈ f.support ∪ g.support, x ∉ g.support → g x • v x = 0

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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∀ x ∈ f.support ∪ g.support, x ∉ f.support → f x • v x = 0
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1

Tactic:
· have := epow_right_mono x_2.ne_zero (Order.one_le_iff_ne_zero.2 y_0)
    simp only [epow_one, h] at this
    exact (not_lt_of_ge this x_2).rec

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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
i : ι
hi : i ∉ g.support
⊢ g i • v i = 0

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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
i : ι
hi : i ∉ f.support
⊢ f i • v 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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
i : ι
hi : i ∉ g.support
⊢ g i • v i = 0

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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
i : ι
hi : i ∉ f.support
⊢ f i • v i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: 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
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = if i ∈ s then f i else 0

pp: 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
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0

Tactic:
<;>

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
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = if i ∈ s then f i else 0

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
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

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

Tactic:
rw [← Finsupp.range_linearCombination, LinearMap.coe_range]

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 : Fin n
⊢ ∏ i < a.castSucc, f i = ∏ i < a, f i.castSucc

Tactic:
by
  simp [← map_castSuccEmb_Iio]

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

Goal state before:
pp: case pos
b c : ℕ
h✝² : c = 0
h✝¹ : b = 0
h✝ : c % b = 0
⊢ (1 - 1) % (1 - 1) = 1 - 1

pp: case neg
b c : ℕ
h✝² : c = 0
h✝¹ : b = 0
h✝ : ¬c % b = 0
⊢ (1 - 1) % (1 - 1) = 0 - 1

pp: case pos
b c : ℕ
h✝² : c = 0
h✝¹ : ¬b = 0
h✝ : c % b = 0
⊢ (1 - 1) % (0 - 1) = 1 - 1

pp: case neg
b c : ℕ
h✝² : c = 0
h✝¹ : ¬b = 0
h✝ : ¬c % b = 0
⊢ (1 - 1) % (0 - 1) = 0 - 1

pp: case pos
b c : ℕ
h✝² : ¬c = 0
h✝¹ : b = 0
h✝ : c % b = 0
⊢ (0 - 1) % (1 - 1) = 1 - 1

pp: case neg
b c : ℕ
h✝² : ¬c = 0
h✝¹ : b = 0
h✝ : ¬c % b = 0
⊢ (0 - 1) % (1 - 1) = 0 - 1

pp: case pos
b c : ℕ
h✝² : ¬c = 0
h✝¹ : ¬b = 0
h✝ : c % b = 0
⊢ (0 - 1) % (0 - 1) = 1 - 1

pp: case neg
b c : ℕ
h✝² : ¬c = 0
h✝¹ : ¬b = 0
h✝ : ¬c % b = 0
⊢ (0 - 1) % (0 - 1) = 0 - 1

Tactic:
<;>

Goal state after:
case pos
b c : ℕ
h✝² : c = 0
h✝¹ : b = 0
h✝ : c % b = 0
⊢ (1 - 1) % (1 - 1) = 1 - 1

case neg
b c : ℕ
h✝² : c = 0
h✝¹ : b = 0
h✝ : ¬c % b = 0
⊢ (1 - 1) % (1 - 1) = 0 - 1

case pos
b c : ℕ
h✝² : c = 0
h✝¹ : ¬b = 0
h✝ : c % b = 0
⊢ (1 - 1) % (0 - 1) = 1 - 1

case neg
b c : ℕ
h✝² : c = 0
h✝¹ : ¬b = 0
h✝ : ¬c % b = 0
⊢ (1 - 1) % (0 - 1) = 0 - 1

case pos
b c : ℕ
h✝² : ¬c = 0
h✝¹ : b = 0
h✝ : c % b = 0
⊢ (0 - 1) % (1 - 1) = 1 - 1

case neg
b c : ℕ
h✝² : ¬c = 0
h✝¹ : b = 0
h✝ : ¬c % b = 0
⊢ (0 - 1) % (1 - 1) = 0 - 1

case pos
b c : ℕ
h✝² : ¬c = 0
h✝¹ : ¬b = 0
h✝ : c % b = 0
⊢ (0 - 1) % (0 - 1) = 1 - 1

case neg
b c : ℕ
h✝² : ¬c = 0
h✝¹ : ¬b = 0
h✝ : ¬c % b = 0
⊢ (0 - 1) % (0 - 1) = 0 - 1
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ i.castSucc < a

pp: case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ i.castSucc.castSucc < a.succ

Tactic:
<;>

Goal state after:
case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ i.castSucc < a

case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ i.castSucc.castSucc < a.succ
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ ↑i < ↑a

pp: case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ ↑i < ↑a + 1

Tactic:
<;>

Goal state after:
case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ ↑i < ↑a

case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ ↑i < ↑a + 1
Module: Mathlib.Data.Nat.GCD.Basic

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

pp: case refine_1.refine_2
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x.gcd m ∣ m

Tactic:
<;>

Goal state after:
case refine_1.refine_1
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x.gcd n ∣ n

case refine_1.refine_2
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x.gcd m ∣ m
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case refine_2.refine_1
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd n ∣ x

pp: case refine_2.refine_2
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd m ∣ x

Tactic:
<;>

Goal state after:
case refine_2.refine_1
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd n ∣ x

case refine_2.refine_2
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd m ∣ x