mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
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:
simp

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

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
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:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (finSumNatEquiv n).symm ↑i = Sum.inl i

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ (finSumNatEquiv n).symm (i + n) = Sum.inr i

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ (finSumNatEquiv n).symm (n + i) = Sum.inr i

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(uIcc a b) = #(uIcc ↑a ↑b)

Tactic:
← map_valEmbedding_uIcc,

Goal state after:
n : ℕ
a b : Fin n
⊢ #(uIcc a b) = #(map valEmbedding (uIcc a b))
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ n m : ℕ
h : n ≤ m
i : Fin n
⊢ ↑(castLE h i) < n

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ n m : ℕ
h : n ≤ m
x✝ : Fin n
⊢ (fun i ↦ ⟨↑↑i, ⋯⟩) ((fun i ↦ ⟨castLE h i, ⋯⟩) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ n m : ℕ
h : n ≤ m
x✝ : { i // ↑i < n }
⊢ (fun i ↦ ⟨castLE h i, ⋯⟩) ((fun i ↦ ⟨↑↑i, ⋯⟩) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ : ℕ
α : Type u_1
m n : ℕ
fg : (Fin m → α) × (Fin n → α)
⊢ (fun f ↦ (fun i ↦ f (castAdd n i), fun i ↦ f (natAdd m i))) ((fun fg ↦ append fg.1 fg.2) fg) = fg

Tactic:
simp

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin (n + 1) → α
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) = v ∘ fun n_1 ↦ n_1 + n_1 + 1

Tactic:
ext i
  simp_rw [Function.comp, vecAlt1, vecAppend_eq_ite]
  cases n with
  | zero =>
    obtain ⟨i, hi⟩ := i
    simp only [Nat.zero_add, Nat.lt_one_iff] at hi; subst i; rfl
  | succ n =>
    split_ifs with h <;> congr
    · simp [Nat.mod_eq_of_lt, h]
    · rw [Fin.val_mk, not_lt] at h
      simp only [Nat.mod_add_mod,
        Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by lia)]
      refine (Nat.mod_eq_of_lt ?_).symm
      lia

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), (t i).Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a

Tactic:
by
  cases nonempty_fintype ι
  lift t to ι → Finset α using ht
  classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a

Tactic:
Set.sUnion_eq_biUnion

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i ∈ t, i), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ none ∉ range some

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
⊢ (vecCons a (vecCons b x) ∘ ⇑(Equiv.swap 0 1)) 0 = vecCons b (vecCons a x) 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
⊢ (vecCons a (vecCons b x) ∘ ⇑(Equiv.swap 0 1)) 1 = vecCons b (vecCons a x) 1

Tactic:
simp

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

Goal state before:
pp: case inr.inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : i.succ ≠ 0
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) i.succ = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) i.succ

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : j.succ ≠ 0
hki : j.succ ≠ i.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) j.succ = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) j.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case zero
a : Fin (0 + 1)
⊢ ↑(a - 1) = if a = 0 then 0 else ↑a - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin (n + 2)
⊢ k < k - 1 ↔ k = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k = k + 1 → k = 0

Tactic:
simp

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

Goal state before:
pp: case funProp.discharger
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ 1 a = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
⊢ (finCongr ⋯) ⟨n - n, ⋯⟩ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (finRotate (n + 1)) i = i + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
⊢ (finRotate n.succ) 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ (Equiv.symm (finRotate n)) i = i - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun i ↦ i - k) ((fun i ↦ i + k) i) = i

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun i ↦ i + k) ((fun i ↦ i - k) i) = i

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case zero
n✝ n : ℕ
i : Fin (n + 1)
⊢ ↑((finCycle 0) i) = ↑((⇑(finRotate (n + 1)))^[↑0] i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b) =
    ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (a_1 : β) (b : γ) (_ :
      b ∈ Finset.image Prod.snd ({ab ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}) | ab.1 = a_1})), f (a, a_1, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
⊢ ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
⊢ ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a

Tactic:
simp

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

Goal state before:
pp: ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)

Tactic:
by
  by_cases hf : f.HasFiniteMulSupport
  · exact map_finprod (Nat.castRingHom R) hf
  · have H : ¬ (fun i ↦ (f i : R)).HasFiniteMulSupport :=
      fun h ↦ hf <| h.of_comp cast_one cast_injective
    rw [finprod_of_not_hasFiniteMulSupport hf, finprod_of_not_hasFiniteMulSupport H, cast_one]

Goal state after:
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
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
i : ι
⊢ (linearCombination R v) (single i 1) = v i

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y✝ : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
⊢ (span R (range v)).subtype y = ↑y

Tactic:
simp

Goal state after:
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
v : ι → M
hli : LinearIndependent R v
i : ι
⊢ ↑((Basis.span hli) i) = v i

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_7
M : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
h : span R (range v) = span R (range (-v))
i✝ : ι
⊢ ↑((Basis.span ⋯) i✝) =
    ↑(((Basis.span hli).map (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (span R (range v)) (span R (range (-v))) h)) i✝)

Tactic:
simp

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁶ : Semiring R✝
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R✝ M
inst✝³ : AddCommMonoid M'
inst✝² : Module R✝ M'
b✝ : Basis ι✝ R✝ M
v : ι✝ → M
x✝ y✝ : M
b : Basis ι✝ R✝ M
ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
x y : R
⊢ single default (x + y) = single default x + single default y

Tactic:
simp

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁶ : Semiring R✝
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R✝ M
inst✝³ : AddCommMonoid M'
inst✝² : Module R✝ M'
b✝ : Basis ι✝ R✝ M
v : ι✝ → M
x✝ y : M
b : Basis ι✝ R✝ M
ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
c x : R
⊢ single default (c • x) = (RingHom.id R) c • single default x

Tactic:
simp

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁶ : Semiring R✝
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R✝ M
inst✝³ : AddCommMonoid M'
inst✝² : Module R✝ M'
b✝ : Basis ι✝ R✝ M
v : ι✝ → M
x✝ y : M
b : Basis ι✝ R✝ M
ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
x : R
⊢ (fun f ↦ f default) ((fun x ↦ single default x) x) = x

Tactic:
simp

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁶ : Semiring R✝
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R✝ M
inst✝³ : AddCommMonoid M'
inst✝² : Module R✝ M'
b✝ : Basis ι✝ R✝ M
v : ι✝ → M
x y : M
b : Basis ι✝ R✝ M
ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
f : ι →₀ R
⊢ ((fun x ↦ single default x) ((fun f ↦ f default) f)) default = f default

Tactic:
simp

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

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
x✝ : ι
⊢ (Basis.singleton ι R) x✝ = 1 x✝

Tactic:
simp

Goal state after:
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
⊢ ∀ (r : R) (m : M), b.repr (r • m) = r • b.repr m

Tactic:
simp

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✝ : R
⊢ x✝ • v i = (⇑(Finsupp.linearCombination R v) ∘ Finsupp.single i) x✝

Tactic:
simp

Goal state after:
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
inst✝² : Fintype ι
b : Basis ι R M
inst✝¹ : Fintype R
inst✝ : Fintype M
⊢ card (ι → R) = card R ^ card ι

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
x : ℕ∞
h : x ≠ 0
z : ℕ∞
y_z : ⊤ ≤ z
⊢ (fun y ↦ x ^ y) ⊤ ≤ (fun y ↦ x ^ y) z

pp: case coe
x : ℕ∞
h : x ≠ 0
z : ℕ∞
a✝ : ℕ
y_z : ↑a✝ ≤ z
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) z

Tactic:
· rw [top_le_iff.1 y_z]

Goal state after:
case coe
x : ℕ∞
h : x ≠ 0
z : ℕ∞
a✝ : ℕ
y_z : ↑a✝ ≤ z
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y z : ℕ∞
x_0 : x < 1
⊢ x ^ (y + z) = x ^ y * x ^ z

pp: case inr.inl
y z : ℕ∞
⊢ 1 ^ (y + z) = 1 ^ y * 1 ^ z

pp: case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
· rw [Order.lt_one_iff.1 x_0]
    rcases eq_zero_or_pos y with rfl | y_0
    · simp only [zero_add, epow_zero, one_mul]
    · rw [zero_epow y_0.ne.symm, zero_mul]
      exact zero_epow (add_pos_of_pos_of_nonneg y_0 bot_le).ne.symm

Goal state after:
case inr.inl
y z : ℕ∞
⊢ 1 ^ (y + z) = 1 ^ y * 1 ^ z

case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr.inr.inl
x z : ℕ∞
x_2 : 1 < x
⊢ (x * 1) ^ ⊤ = x ^ ⊤ * 1 ^ ⊤

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ ∏ i, cons x f i = x * ∏ i, f i

Tactic:
by
  simp_rw [prod_univ_succ, cons_zero, cons_succ]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 1 → M
⊢ ∏ i, f i = f 0

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
p a : M
⊢ 0 • p + a = 0 • p + a

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a p : M
n : ℕ
⊢ 0 • p + (n • p + a) = n • p + a

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
⊢ ∏ _i, x = x ^ n

Tactic:
simp

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
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
t : Finset ↑s
⊢ ↑(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t) ⊆ s

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
h : 0 < n + 1
x : M
p : Fin n → M
⊢ ∏ j, ⟨0, h⟩.insertNth x p j = x * ∏ j, p j

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p : G
z : ℤ
⊢ -z • p = 0 - z • p

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
z : ℤ
⊢ -z • p = a - (a + z • p)

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
z : ℤ
⊢ -z • p = a - (z • p + a)

Tactic:
simp

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

Goal state before:
pp: case e_a
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ∀ (x y : Fin n), x ∈ univ ∧ y ∈ Iic x ↔ x ∈ Ici y ∧ y ∈ univ

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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) % (0 - 1) = 1 - 1

Tactic:
simp

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

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

Tactic:
simp

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
⊢ (0 - 1) % (1 - 1) = 1 - 1

Tactic:
simp

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

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

Tactic:
simp

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
⊢ (0 - 1) % (0 - 1) = 1 - 1

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inr.inl
b c : ℕ
ha0 : succ 0 > 0
⊢ (succ 0 ^ c - 1) % (succ 0 ^ b - 1) = succ 0 ^ (c % b) - 1

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inl
a c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
⊢ (a ^ c - 1) % (a ^ 0 - 1) = a ^ (c % 0) - 1

Tactic:
simp

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

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: a c n : ℕ
⊢ (a + c * n).Coprime c ↔ a.Coprime c

Tactic:
simp

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

Goal state before:
pp: b c n : ℕ
⊢ (c * n + b).Coprime c ↔ b.Coprime c

Tactic:
simp

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

Goal state before:
pp: a b n : ℕ
⊢ a.Coprime (b + a * n) ↔ a.Coprime b

Tactic:
simp

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

Goal state before:
pp: a c n : ℕ
⊢ a.Coprime (a * n + c) ↔ a.Coprime c

Tactic:
simp

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

Goal state before:
pp: ⊢ ¬Coprime 0 0

Tactic:
simp

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
a₁✝ : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)
⊢ ∀ ⦃a₂ : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)⦄, (fun x ↦ ⟨x.1, ⋯⟩) a₁✝ = (fun x ↦ ⟨x.1, ⋯⟩) a₂ → a₁✝ = a₂

Tactic:
simp

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

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

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

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:
· rwa [succAbove_of_castSucc_lt, succAbove_of_castSucc_lt, partialProd_right_inv,
    contractNth_apply_of_lt]
    · assumption
    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
      exact le_of_lt h

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

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.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 : ∃ y ∈ Finsupp.supported R R (univ \ {i}), (Finsupp.linearCombination R v) y = a • v i
⊢ a = 0

Tactic:
rcases ha with ⟨l, hl, e⟩

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : l ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
⊢ a = 0
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 : ι
⊢ ∃ a, f a = i

Tactic:
let repr : (span R (range (v ∘ f)) : Type _) → ι' →₀ R := (hv.comp f f.injective).repr

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
⊢ ∃ a, f a = i