mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : M →ₗ[R] M'
i : ι
⊢ (b.constr S).symm f i = f (b i)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
⊢ x ∈ span R (Set.range fun x ↦ v ↑x) ↔ x ∈ span R (Set.range fun i ↦ v ↑i)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ (∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x) → x ∈ span R s

Tactic:
by
    rintro ⟨n, t, hts, -, rfl⟩; exact sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hts hx

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #(filter ((fun x ↦ p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ) + 1
    else #(filter ((fun x ↦ p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ)) =
    if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
k : Fin n
hk : ¬p k
⊢ {i | p i} ⊆ Iio k

Tactic:
grind

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
⊢ ↑j < #{i | p i} → p j

Tactic:
grind

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ filter q univ ⊆ filter p univ

Tactic:
grind

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ #(filter p univ) ≤ min n #{i | p i}

Tactic:
grind

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
this : filter q univ = filter p univ
⊢ j ∈ filter p univ

Tactic:
grind

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
this✝ : filter q univ = filter p univ
this : j ∈ filter p univ
⊢ False

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
f : ℕ → α
⊢ (univ.sup fun n_1 ↦ f ↑n_1) = univ.sup (f ∘ val)

Tactic:
Function.comp_def

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
f : ℕ → α
⊢ (univ.sup fun n_1 ↦ f ↑n_1) = univ.sup fun x ↦ f ↑x
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u_1
x : α
⊢ Fin.cons x ![] = ![x]

Tactic:
rfl

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

Goal state before:
pp: case refl
α : Type u_1
x : α
⊢ Fin.snoc ![] x 0 = ![x] 0

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
α : Type u_1
x y : α
p : Fin n → α
⊢ Fin.cons x (vecCons y p) = vecCons x (vecCons y p)

Tactic:
rfl

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

Goal state before:
pp: α : Type u
x : α
u : Fin 0 → α
⊢ vecCons x u 0 = x

Tactic:
rfl

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

Goal state before:
pp: case e_e
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(Fin.cast ho i) < m
⊢ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨↑i - m, ⋯⟩

Tactic:
rfl

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rw [Fin.val_mk] at h

Goal state after:
case pos
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case zero
α : Type u
v : Fin (0 + 1) → α
hi : 0 < 0 + 1
⊢ (if h : ↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 < 0 + 1 then v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩
    else v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨0, hi⟩ + ⟨0, hi⟩ + 1)

Tactic:
rfl

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = (vecCons x u ∘ fun n_1 ↦ n_1 + n_1) i

Tactic:
rfl

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = (vecCons x u ∘ fun n_1 ↦ n_1 + n_1 + 1) i

Tactic:
rfl

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

Goal state before:
pp: case zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨0, hi⟩

Tactic:
rfl

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

Goal state before:
pp: case zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨0, hi⟩

Tactic:
rfl

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
i : ℕ
h : i + 2 < n.succ.succ
⊢ ⟨i + 2, h⟩ = ⟨i, ⋯⟩.succ.succ

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ f x ≠ 1 ∧ ¬x = a

Tactic:
grind

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ k = ⟨↑k - 1, ⋯⟩.succ

Tactic:
grind

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨↑k - 1, ⋯⟩.succ
⊢ ⟨↑k - 1, ⋯⟩ ≠ i

Tactic:
grind

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨↑k - 1, ⋯⟩.succ
⊢ ⟨↑k - 1, ⋯⟩ ≠ j

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ -last n = 1

Tactic:
by simp [neg_eq_iff_add_eq_zero]

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

Goal state before:
pp: case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ cast ⋯ (v (⟨i, h⟩.castLT h')) = cases a v ⟨i + 1, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ cast ⋯ a = cases a v ⟨0, ⋯⟩

Tactic:
rfl

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
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α), {ab ∈ s | ab.1 = a}.prod f

Tactic:
finprod_eq_prod_of_mulSupport_subset _
      (s.mulSupport_of_fiberwise_prod_subset_image f Prod.fst),

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ i ∈ Finset.image Prod.fst s, ∏ a ∈ s with a.1 = i, f a
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)
⊢ range (Subtype.val ∘ fun i ↦ ⟨v i, ⋯⟩) = range v

Tactic:
rfl

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

Goal state before:
pp: case top
x : ℕ∞
⊢ x ^ ⊤ = if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
rfl

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

Goal state before:
pp: case coe
x : ℕ∞
n : ℕ
⊢ x ^ ↑n = x ^ n

Tactic:
rfl

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

Goal state before:
pp: case top
y : ℕ∞
⊢ 1 ^ ⊤ = 1

Tactic:
rfl

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: case inr.inr.inr.inl
y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ 1 ^ (y * z) = (1 ^ y) ^ z

pp: case inr.inr.inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
· simp only [one_epow]

Goal state after:
case inr.inr.inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ x ^ (↑a✝ * ⊤) = (x ^ ↑a✝) ^ ⊤

Tactic:
mul_top y_0,

Goal state after:
case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ x ^ ⊤ = (x ^ ↑a✝) ^ ⊤
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
l : List M
⊢ ∏ i, l[↑i] = l.prod

Tactic:
by
  simp [Finset.prod_eq_multiset_prod]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
l : List ι
f : ι → M
⊢ ∏ i, f l[↑i] = (List.map f l).prod

Tactic:
by
  simp [Finset.prod_eq_multiset_prod]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 3 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (last 2) = f 0 * f 1 * f 2

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
⊢ a ≡ b [PMOD p] ↔ ∃ m n, m • p + a = n • p + b

Tactic:
rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 4 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (last 3) = f 0 * f 1 * f 2 * f 3

Tactic:
rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 5 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4

Tactic:
rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 6 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (last 5) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5

Tactic:
rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 7 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (last 6) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Tactic:
rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 8 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (castSucc 6) *
      f (last 7) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Tactic:
rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a : Fin n
⊢ ∏ i ≤ castLE h a, f i = ∏ i ≤ a, f (castLE h i)

Tactic:
by
  simp [← map_castLEEmb_Iic]

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

Goal state before:
pp: case mp.refine_1
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % ↑n < ↑n

pp: case mp.refine_2
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ a - b = (k / ↑n * ↑n + k % ↑n) • p

Tactic:
· refine Int.emod_lt_of_pos _ ?_
      lia

Goal state after:
case mp.refine_2
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ a - b = (k / ↑n * ↑n + k % ↑n) • p
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
f : Fin (n + 1) → M
j : Fin (n + 1)
⊢ f 0 * (List.take (↑j) (List.ofFn fun i ↦ f i.succ)).prod = f 0 * (List.take (↑j) (List.ofFn (tail f))).prod

Tactic:
rfl

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

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

Tactic:
rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]

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

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

Tactic:
rfl

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∈ span R (v '' {x})

Tactic:
Set.image_singleton

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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∈ R ∙ v x
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
rfl

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
hv : LinearIndepOn R v s
hi : i ∈ s
a : R
ha : a • v i ∈ span R (v '' (s \ {i}))
⊢ a • v ↑⟨i, hi⟩ ∈ span R ((fun x ↦ v ↑x) '' (univ \ {⟨i, hi⟩}))

Tactic:
by
    simpa [← comp_def, image_comp, image_sdiff Subtype.val_injective]

Goal state after:
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:
· show Int.gcd (m / d) (c / d) = 1
    simp only [d, ← Int.natCast_div, Int.gcd_natCast_natCast (m / d) (c / d),
      gcd_div hmd hcd, Nat.div_self (gcd_pos_of_pos_left c hm)]

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

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

Tactic:
rfl

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

Tactic:
rfl

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

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

Goal state before:
pp: case neg
iv : ℕ
ih : ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last iv))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i ↦ Fin (n (Fin.natAdd iv i))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) ⟨Sum.inr 0, j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j

Tactic:
rfl

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

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

Goal state before:
pp: case pos
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
A : {j | ↑j < i + 1} = insert ⟨i, h⟩ {j | ↑j < i}
⊢ (take i (ofFn f)).prod * (ofFn f)[i] = ∏ j with ↑j < i + 1, f j

Tactic:
grind

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

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

Tactic:
convert! Fintype.card_fin (n + 1) using 2

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 < (ofFn f).length
this : (ofFn f).length ≤ i
⊢ take i (ofFn f) = take i.succ (ofFn f)

Tactic:
rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]

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

Goal state before:
pp: α : Type u_3
inst✝ : AddCommGroup α
n : ℕ
d : Fin (n + 2) → α
r : Fin (n + 1) → α
h_first : d 0 = r 0
h_mid : ∀ (i : Fin n), d i.castSucc.succ = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
h₂ : -∑ x, (-1) ^ ↑x • (r x.castSucc + r x.succ) = -∑ x, (-1) ^ ↑x • r x.castSucc + -∑ x, (-1) ^ ↑x • r x.succ
h₃ : r 0 + -∑ x, (-1) ^ ↑x • r x.succ = ∑ x, (-1) ^ ↑x • r x.castSucc + (-1) ^ n • r (last n)
⊢ r 0 + (-∑ x, (-1) ^ ↑x • r x.castSucc + -∑ x, (-1) ^ ↑x • r x.succ) + -((-1) ^ n • r (last n)) = 0

Tactic:
grind

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ g a * a 1 = (g a • ⇑a) 1

Tactic:
rfl

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

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
le : ∀ (s : Finset M), s.card = n + 1 → ¬LinearIndepOn R id ↑s
⊢ Module.rank R M < ↑(n + 1)

Tactic:
rw [Module.rank, Nat.cast_add_one, lt_natCast_add_one_iff, ciSup_le_iff bddAbove_of_small]

Goal state after:
case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
le : ∀ (s : Finset M), s.card = n + 1 → ¬LinearIndepOn R id ↑s
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ ↑n
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ 0 1 = 0

Tactic:
rfl

Goal state after:
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
inst✝ : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
⊢ ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i =
    ∑ i ∈ s \ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i

Tactic:
conv =>
        enter [2, 1, 1]
        rw [← s.subtype_map_of_mem (fun x hx => hx), Finset.subtype_eq_univ.2 (fun x hx => hx)]
        change Finset.map (Embedding.subtype (· ∈ (s : Set ι))) _

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
inst✝ : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
⊢ ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i =
    ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) Finset.univ \ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t,
      (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ s.encard = 3

Tactic:
rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_singleton]

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ 1 + 1 + 1 = 3

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ y ∉ {z}

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ x ∉ {y, z}