mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ∀ (s : Set (Submodule R M)), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → R ∙ x ≤ sSup s → ∃ x_1 ∈ s, R ∙ x ≤ x_1

Tactic:
intro d hemp hdir hsup

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
⊢ ∃ x_1 ∈ d, R ∙ x ≤ x_1
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
h : f.ker ≤ p
⊢ comap f (map f p) = p

Tactic:
Submodule.comap_map_eq,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
h : f.ker ≤ p
⊢ p ⊔ f.ker = p
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Tactic:
simp only [add_comm (1 : R), prod_add, prod_const_one, mul_one]

Goal state after:
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
hp : ∃! x, x ∈ s ∧ p x
a : α
⊢ find? p s ⋯ = some a ↔ some (choose p s hp) = some a

Tactic:
refine find?_eq_some_iff _ |>.trans ?_

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
hp : ∃! x, x ∈ s ∧ p x
a : α
⊢ a ∈ s ∧ p a ↔ some (choose p s hp) = some a
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
hp : ∃! x, x ∈ s ∧ p x
⊢ find? p s ⋯ = some (choose p s hp)

Tactic:
by
  ext a
  refine find?_eq_some_iff _ |>.trans ?_
  simp only [Option.some.injEq, choose_eq_iff]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
⊢ f a = g a

Tactic:
have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
hg : g a = 0
⊢ f a = g a
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
f : M → N
hf : f 0 = 0
x✝ : α
⊢ (mapRange f hf 0) x✝ = 0 x✝

Tactic:
by simp only [hf, zero_apply, mapRange_apply]

Goal state after:
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : Nonempty α
inst✝ : Nontrivial M
inhabited_h : Inhabited α
⊢ Nontrivial (α →₀ M)

Tactic:
rcases exists_ne (0 : M) with ⟨x, hx⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : Nonempty α
inst✝ : Nontrivial M
inhabited_h : Inhabited α
x : M
hx : x ≠ 0
⊢ Nontrivial (α →₀ M)
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
⊢ Nontrivial (α →₀ M) → Nonempty α ∧ Nontrivial M

Tactic:
rintro ⟨f, g, hfg⟩
    obtain ⟨a, ha⟩ := ne_iff.mp hfg
    exact ⟨⟨a⟩, _, _, ha⟩

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
⊢ erase a (f + f') = erase a f + erase a f'

Tactic:
ext s

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
⊢ (erase a (f + f')) s = (erase a f + erase a f') s
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case mpr.inl
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : f ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
| inl h =>

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support
⊢ (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun i ↦ (g i).support

Tactic:
rw [Finsupp.support_add_eq, hs]

Goal state after:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support
⊢ Disjoint (g i).support (∑ i ∈ s, g i).support
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
i : ι
hi : i ∈ s
⊢ ∃ i ∈ s, f i < g i

Tactic:
exact ⟨i, hi, hfg i hi⟩

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ (a : R), a ∈ a✝ → 1 ≤ a
⊢ 1 ≤ a✝.prod

Tactic:
apply List.one_le_prod h

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
⊢ 0 ∈ {p | ↑p.support ⊆ s}

Tactic:
simp only [subset_def, Finset.mem_coe, Set.mem_ofPred_eq, mem_support_iff, zero_apply]

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
⊢ ∀ (x : α), 0 ≠ 0 → x ∈ s
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_7
s : ι → Set α
x : α →₀ M
⊢ x ∈ supported M R (⋂ i, s i) ↔ x ∈ ⨅ i, supported M R (s i)

Tactic:
by simp [mem_supported, subset_iInter_iff]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
⊢ ↥(supported M R s) ≃ₗ[R] ↑s →₀ M

Tactic:
let F : supported M R s ≃ (s →₀ M) := restrictSupportEquiv s M
  refine F.toLinearEquiv ?_
  have :
    (F : supported M R s → ↥s →₀ M) =
      (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M).comp (Submodule.subtype (supported M R s)) :=
    rfl
  rw [this]
  exact LinearMap.isLinear _

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
s : Set α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = s.mulIndicator f a

Tactic:
by
  convert! finprod_eq_if (M := M) (p := a ∈ s) (x := f a)

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
⊢ ⇑(b.repr (∑ i, c i • b i)) = c

Tactic:
simp_rw [← b.equivFun_symm_apply, ← b.equivFun_apply, b.equivFun.apply_symm_apply]

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

Goal state before:
pp: ι : 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✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexRange.repr (b i)) (((Equiv.refl M).subtypeEquiv ⋯).symm ⟨bi, hbi⟩) = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩

Tactic:
reindexRange_repr_self

Goal state after:
ι : 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✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (single ⟨b i, ⋯⟩ 1) (((Equiv.refl M).subtypeEquiv ⋯).symm ⟨bi, hbi⟩) = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩
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
w : Set M
x : ↥(span R w)
⊢ (linearCombination R Subtype.val) (repr R w x) = ↑x

Tactic:
by
  rw [Span.repr_def]
  exact ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose_spec

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

Goal state before:
pp: n : ℕ
⊢ ↑(Iio (last n)) = ↑(map castSuccEmb univ)

Tactic:
ext; simp [lt_def]

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

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

Tactic:
ext i
  cases Fin.fin_one_eq_zero i
  rfl

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ g '' s ∩ mulSupport f = g '' ↑hs.toFinset ∩ mulSupport f

Tactic:
hs.coe_toFinset,

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g)) ∩ mulSupport f
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x✝ : Fin m × Fin n
x : Fin m
y : Fin n
H : 0 < n
⊢ ↑y / n + ↑x = 0 + ↑x

Tactic:
rw [Nat.div_eq_of_lt y.2]

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

Goal state before:
pp: α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 ⋯ u)

Tactic:
ext i
  simp_rw [vecAlt1]
  rcases i with ⟨⟨⟩ | i, hi⟩
  · rfl
  · simp [vecAlt1, Nat.add_right_comm, ← Nat.add_assoc]

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 : ι
hi : v i ∈ span R (range v)
⊢ (Basis.span hli).repr ⟨v i, hi⟩ = single i 1

Tactic:
rw [← LinearEquiv.eq_symm_apply]

Goal state after:
ι : 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 : ι
hi : v i ∈ span R (range v)
⊢ ⟨v i, hi⟩ = (Basis.span hli).repr.symm (single i 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
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
⊢ x ∈ range ⇑b

Tactic:
by_contra q

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
⊢ False
Module: Mathlib.Data.ENat.Pow

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

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:
· rw [Order.lt_one_iff.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]

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

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.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ m n, m • p + b = n • p + a

Tactic:
exact ⟨n, m, h.symm⟩

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ∏ i, ∏ j, f i j = (∏ i, ∏ j with i ≤ j.castSucc, f i j) * ∏ i, ∏ j with j.castSucc < i, f i j

Tactic:
simp only [← Finset.prod_mul_distrib, ← not_le, Finset.prod_filter_mul_prod_filter_not]

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
h' : v x ∈ span R (v '' {x})
⊢ v x ∉ span R (v '' s)

Tactic:
intro w

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
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ False
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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
⊢ (Finsupp.linearCombination R v) f ≠ v x

Tactic:
intro w

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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
w : (Finsupp.linearCombination R v) f = v x
⊢ False
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
← sub_eq_zero

Goal state after:
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ Int.ofNat b - Int.ofNat a = 0
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ ↑(Nat.card α) = #α

Tactic:
Nat.card,

Goal state after:
α : Type u_1
inst✝ : Finite α
⊢ ↑(toNat #α) = #α
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case neg
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j with ↑j < i + 1, f j

Tactic:
· have A : (ofFn f).take i = (ofFn f).take i.succ := by
        rw [← length_ofFn (f := f)] at h
        have : length (ofFn f) ≤ i := not_lt.mp h
        rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
      have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) := by
        intro j
        have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
        simp [this, lt_trans this (Nat.lt_succ_self _)]
      simp [← A, B, IH]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f

Tactic:
and_congr_left_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Surjective f → (Injective f ↔ Nat.card α = Nat.card β)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
⊢ Nat.card ↑(f ⁻¹' s) = Nat.card ↑s

Tactic:
by
  rw [← Nat.card_image_of_injOn hf, image_preimage_eq_iff.2 hsf]

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Fintype.card α = 1

Tactic:
Fintype.card_ofSubsingleton a

Goal state after:
α : Type u_1
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case insert
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), ∑ i ∈ insert a s, g i • ⇑i = 0 → ∀ i ∈ insert a s, g i = 0

Tactic:
intro g

Goal state after:
case insert
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
⊢ ∑ i ∈ insert a s, g i • ⇑i = 0 → ∀ i ∈ insert a s, g i = 0
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
i : G →* L
his : i ∈ s
x : G
⊢ (g i • ⇑i) x = (g i • ⇑a) x

Tactic:
← sub_eq_zero

Goal state after:
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
i : G →* L
his : i ∈ s
x : G
⊢ (g i • ⇑i) x - (g i • ⇑a) x = 0
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝ : Fintype α
⊢ Nat.card ((a : α) → β a) = ∏ a, Nat.card (β a)

Tactic:
Nat.card,

Goal state after:
α : Type u_1
β : α → Type u_3
inst✝ : Fintype α
⊢ toNat #((a : α) → β a) = ∏ a, toNat #(β a)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ card (ULift.{?u.15, u_3} α) ≤ card β

Tactic:
← card_ulift β

Goal state after:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ card (ULift.{?u.15, u_3} α) ≤ card (ULift.{?u.17, u_4} β)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
⊢ 1 < card α ↔ ↑1 < #α

Tactic:
rw [← natCast_lt_toENat]

Goal state after:
α : Type u_3
⊢ 1 < card α ↔ ↑1 < toENat #α
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 ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0

Tactic:
specialize h t₁ (fun i => if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) ?_
    · rw [← Finset.sum_subset ht₁t₂.le_compl_left]
      · convert! heq using 2 with i hi i hi <;> simp [hi]
      · intro i hi hi'
        simp [Finset.mem_compl.1 hi, hi']
    refine ⟨fun i hi => ?_, fun i hi => ?_⟩ <;> simpa [hi] using h i

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

Goal state before:
pp: case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ ∀ w < 1, ∃ i, w < #↑↑i

Tactic:
intro w

Goal state after:
case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
w : Cardinal.{v}
⊢ w < 1 → ∃ i, w < #↑↑i
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
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:
enter [2, 1, 1]

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✝⁴ : 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
| s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard + (s ∩ t).encard = t.encard ↔ (s \ t).encard = (t \ s).encard

Tactic:
← encard_sdiff_add_encard_inter t s,

Goal state after:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard + (s ∩ t).encard = (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard = (t \ s).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard + (s ∩ t).encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard

Tactic:
← encard_sdiff_add_encard_inter t s,

Goal state after:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard + (s ∩ t).encard ≤ (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard ≤ (t \ s).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard + (s ∩ t).encard < t.encard ↔ (s \ t).encard < (t \ s).encard

Tactic:
← encard_sdiff_add_encard_inter t s,

Goal state after:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard + (s ∩ t).encard < (t \ s).encard + (t ∩ s).encard ↔ (s \ t).encard < (t \ s).encard
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : Module R' M
inst✝³ : SMulWithZero R R'
inst✝² : IsScalarTower R R' M
inst✝¹ : FaithfulSMul R R'
inst✝ : IsScalarTower R R' R'
⊢ Module.rank R' M ≤ Module.rank R M

Tactic:
rw [Module.rank, Module.rank]

Goal state after:
R : Type u
R' : Type u'
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : Module R' M
inst✝³ : SMulWithZero R R'
inst✝² : IsScalarTower R R' M
inst✝¹ : FaithfulSMul R R'
inst✝ : IsScalarTower R R' R'
⊢ ⨆ ι, #↑↑ι ≤ ⨆ ι, #↑↑ι