mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case zero
ι : Type u_1
M : Type u_2
m : ℕ
f : Fin 0 → Fin m
⊢ ∑ i, ↑(f i) * m ^ ↑i < m ^ 0

Tactic:
simp

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

Goal state before:
pp: ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
x✝ : ι
⊢ (Subtype.val ∘ fun i ↦ ⟨v i, ⋯⟩) x✝ = v x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m n : ℕ
f : Fin n → Fin m
⊢ ∑ i, ↑(f i) * m ^ ↑i < m ^ n

Tactic:
by
      induction n with
      | zero => simp
      | succ n ih =>
        cases m
        · exact isEmptyElim (f <| Fin.last _)
        simp_rw [Fin.sum_univ_castSucc, Fin.val_castSucc, Fin.val_last]
        refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _
          (Fin.is_le _)).trans_eq ?_
        rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']

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

Goal state before:
pp: n a : ℕ
⊢ n + a ≡ a [MOD n]

Tactic:
simp

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

Goal state before:
pp: n a : ℕ
⊢ a + n ≡ a [MOD n]

Tactic:
simp

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

Goal state before:
pp: m a b d : ℕ
hdm : d ∣ m
h : a ≡ b [MOD d]
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]

Tactic:
exact ⟨h.symm.trans, h.trans⟩

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

Goal state before:
pp: case zero
ι : Type u_1
M : Type u_2
n : Fin 0 → ℕ
f : (i : Fin 0) → Fin (n i)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i

Tactic:
simp

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

Goal state before:
pp: case pos
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ (a % c + b % c) % c + c = a % c + b % c

pp: case neg
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c

Tactic:
· have h2 : (a % c + b % c) / c < 2 :=
        Nat.div_lt_of_lt_mul
          (by
            rw [mul_two]
            exact
              add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
                (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)))
      have h0 : 0 < (a % c + b % c) / c := Nat.div_pos h (Nat.pos_of_ne_zero hc0)
      rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]

Goal state after:
case neg
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
hc0 : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
simp [hc0]

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 (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr 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:
simp

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

Goal state before:
pp: case zero
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
⊢ (take 0 (ofFn f)).prod = ∏ j with ↑j < 0, f j

Tactic:
simp

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite β
f : α → β
hf : Injective f
⊢ lift.{u, v} #β < ℵ₀

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
this : lift.{u, v} #β ≤ lift.{v, u} #α
⊢ lift.{v, u} #α < ℵ₀

Tactic:
simp

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
A : take i (ofFn f) = take i.succ (ofFn f)
⊢ ∀ (j : Fin n), (↑j < i.succ) = (↑j < i)

Tactic:
intro j

Goal state after:
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
A : take i (ofFn f) = take i.succ (ofFn f)
j : Fin n
⊢ (↑j < i.succ) = (↑j < i)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
g : G
⊢ g = [g][0] ^ (-1) ^ ↑0 * ∏ i, [g][i.succ] ^ (-1) ^ ↑i.succ

Tactic:
simp

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.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
⊢ ∑ i, (-1) ^ ↑i • d i = d 0 + ∑ i, (-1) ^ (↑i + 1) • d i.castSucc.succ + (-1) ^ (n + 1) • d (last (n + 1))

Tactic:
rw [Fin.sum_univ_succ, Fin.sum_univ_castSucc]

Goal state after:
α : 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.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
⊢ (-1) ^ ↑0 • d 0 + (∑ i, (-1) ^ ↑i.castSucc.succ • d i.castSucc.succ + (-1) ^ ↑(last n).succ • d (last n).succ) =
    d 0 + ∑ i, (-1) ^ (↑i + 1) • d i.castSucc.succ + (-1) ^ (n + 1) • d (last (n + 1))
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case empty
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
⊢ ∀ (g : (G →* L) → L), ∑ i ∈ ∅, g i • ⇑i = 0 → ∀ i ∈ ∅, g i = 0

Tactic:
simp

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

Goal state before:
pp: c : Cardinal.{u_3}
n : ℕ
⊢ toENat c ≤ ↑n ↔ c ≤ ↑n

Tactic:
simp

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

Goal state before:
pp: c : Cardinal.{u_3}
n : ℕ
⊢ toENat c = ↑n ↔ c = ↑n

Tactic:
simp

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

Goal state before:
pp: case inr.inl.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Finite β
this✝ : Fintype α := Fintype.ofFinite α
this : Fintype β := Fintype.ofFinite β
⊢ card (α → β) = card β ^ card α

Tactic:
simp

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
i : G →* L
his : i ∈ s
x y : G
⊢ 0 (x * y) - a x * 0 y = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
s : { s // LinearIndepOn R id s }
le : ↑(n + 1) ≤ #↑↑s
t : Finset ↑↑s
ht : n + 1 = t.card
⊢ ↑(Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t) ⊆ ↑s

Tactic:
simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ (Finset.map { toFun := v, inj' := ⋯ } Finset.univ).card = n

Tactic:
simp

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 : Cardinal.{v}
⊢ w < 1 → ∃ i, w < #↑↑i

Tactic:
hw

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}
hw : w < 1
⊢ ∃ i, w < #↑↑i
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toNat (Module.rank R ↥⊤) = toNat (Module.rank R M)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ↑⋯.toFinset.card = ↑s.card

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
⊢ s.encard = ⊤

Tactic:
by
  have := h.to_subtype
  rw [encard, ENat.card_eq_top_of_infinite]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
⊢ a ∉ {x | x ≠ a}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case empty
α : Type u_1
s : Set α
⊢ ∅.encard < ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≠ ⊤ ↔ s.Finite

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard < 1 ↔ s = ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 1
⊢ 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 2
⊢ 2 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 3
⊢ 3 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 4
⊢ 4 ≠ 0

Tactic:
simp

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
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ ∀ x ∉ univ \ {i}, (Finsupp.single i (l i) - l) x = 0

Tactic:
intro j

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
j : ι
⊢ j ∉ univ \ {i} → (Finsupp.single i (l i) - l) j = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hk : 0 ≤ s.encard
⊢ ∅.encard = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : ↑n.succ ≤ s.encard
⊢ ↑n ≤ ↑n.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' ∅).encard ≤ ∅.encard

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
h' : IsEmpty α
⊢ InjOn f s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
t : Set β
hs : ∅.Finite
hle : ∅.encard ≤ t.encard
⊢ ∃ f, ∅ ⊆ f ⁻¹' t ∧ InjOn f ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case pos
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
I : Finset η
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
j : η
hnotMem : j ∉ I
h1 : ∀ i ∉ insert j I, x i = 1
h2 : ∀ i ∈ insert j I, Pi.mulSingle i (x i) ∈ H
⊢ x j = (Function.update x j 1 * Pi.mulSingle j (x j)) j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
⊢ ∀ i_1 ∉ I, Function.update x i 1 i_1 = 1

Tactic:
intro j

Goal state after:
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
⊢ j ∉ I → Function.update x i 1 j = 1
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
⊢ ∀ i_1 ∈ I, Pi.mulSingle i_1 (Function.update x i 1 i_1) ∈ H

Tactic:
intro j

Goal state after:
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
⊢ j ∈ I → Pi.mulSingle j (Function.update x i 1 j) ∈ H
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case pos
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
I : Finset η
x : (i : η) → f i
j : η
hj hnotMem : j ∉ I
h1 : ∀ i ∉ insert j I, x i = 1
h2 : ∀ i ∈ insert j I, Pi.mulSingle i (x i) ∈ H
⊢ Function.update x j 1 j = 1

Tactic:
simp

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

Goal state before:
pp: case refine_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
i : Fin m.succ
⊢ (Subtype.val ∘ Fin.cons ⟨x, x_mem⟩ fun i ↦ ⟨↑(v i), ⋯⟩) 0 = Fin.cons x (Subtype.val ∘ v) 0

Tactic:
simp

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

Goal state before:
pp: case refine_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
i : Fin m.succ
⊢ ∀ (i : Fin m), (Subtype.val ∘ Fin.cons ⟨x, x_mem⟩ fun i ↦ ⟨↑(v i), ⋯⟩) i.succ = Fin.cons x (Subtype.val ∘ v) i.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝⁴ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝³ : SetLike S ((i : η) → f i)
inst✝² : SubmonoidClass S ((i : η) → f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ ∀ i ∉ Finset.univ, x i = 1

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥⊥ = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case pos
α : Type u_1
a : α
s : Set α
h : s.Finite
h✝ : a ∈ s
⊢ s.ncard ≤ s.ncard

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case neg
α : Type u_1
a : α
s : Set α
h : s.Finite
h✝ : a ∉ s
⊢ s.ncard ≤ s.ncard + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ {a}.Finite

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.encard ≤ ↑s.ncard
ht : t.Finite
⊢ t.encard ≤ s.encard

Tactic:
(ht.subset h).cast_ncard_eq

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.encard ≤ s.encard
ht : t.Finite
⊢ t.encard ≤ s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
P : α → Prop
h : {x | x ∈ s ∧ P x}.ncard = s.ncard
ha : a ∈ s
hs : s.Finite
⊢ {x | x ∈ s ∧ P x} ⊆ s

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ 1 • s ↔ x ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ op 1 • s ↔ x ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Set α
x a : α
h : a⁻¹ * x ∈ s
⊢ (fun x ↦ a • x) (a⁻¹ * x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Set α
x a : α
h : x * a⁻¹ ∈ s
⊢ (fun x ↦ op a • x) (x * a⁻¹) = x

Tactic:
simp

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

Goal state before:
pp: M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
x : ↥A
i x✝ : ι
⊢ (mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ ↑(addSubgroupOfClosure A b h).repr) ((addSubgroupOfClosure A b h) x✝) =
    ((↑ℤ ↑b.repr).domRestrict (AddSubgroup.toIntSubmodule A)) ((addSubgroupOfClosure A b h) x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
x✝ : (fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₂ ≤ (fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₁
a : α
ha : a ∈ t₂
le1 : ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).1 ≤ ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).1
le2 : ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).2 ⊆ ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).2
a' : α
h' : a' ∈ ↑t₁
eq : ↑a' = ↑a
⊢ a = a' * s.subtype ⟨a'⁻¹ * a, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
x✝ : ↑(g • ↑s)
x : α
property✝ : x ∈ g • ↑s
⊢ ↑((fun x ↦ ⟨g * ↑x, ⋯⟩) ((fun x ↦ ⟨g⁻¹ * ↑x, ⋯⟩) ⟨x, property✝⟩)) = ↑⟨x, property✝⟩

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α
x✝ : ↥s
g : α
property✝ : g ∈ s
⊢ ↑((fun x ↦ ⟨g✝⁻¹ * ↑x, ⋯⟩) ((fun x ↦ ⟨g✝ * ↑x, ⋯⟩) ⟨g, property✝⟩)) = ↑⟨g, property✝⟩

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
x✝ : ↑(op g • ↑s)
x : α
property✝ : x ∈ op g • ↑s
⊢ ↑((fun x ↦ ⟨↑x * g, ⋯⟩) ((fun x ↦ ⟨↑x * g⁻¹, ⋯⟩) ⟨x, property✝⟩)) = ↑⟨x, property✝⟩

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α
x✝ : ↥s
g : α
property✝ : g ∈ s
⊢ ↑((fun x ↦ ⟨↑x * g✝⁻¹, ⋯⟩) ((fun x ↦ ⟨↑x * g✝, ⋯⟩) ⟨g, property✝⟩)) = ↑⟨g, property✝⟩

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = Quotient.mk'' (Quotient.out L) }

Tactic:
simp

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = L }
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_3
s : Set α
⊢ univ.ncard = s.ncard

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h₁ : {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe
t : Finset α
⊢ t ∈ SetLike.coe ⁻¹' {t | t ⊆ ↑s ∧ t.ncard = n} ↔ t ∈ ↑(Finset.powersetCard n s)

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : ↑(mk ⁻¹' t)
a : α
property✝ : a ∈ mk ⁻¹' t
⊢ Quotient.out ↑((fun a ↦ (⟨(Quotient.out ↑↑a)⁻¹ * ↑a, ⋯⟩, ⟨↑↑a, ⋯⟩)) ⟨a, property✝⟩).2 *
      ↑((fun a ↦ (⟨(Quotient.out ↑↑a)⁻¹ * ↑a, ⋯⟩, ⟨↑↑a, ⋯⟩)) ⟨a, property✝⟩).1 =
    a

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝ : Group α
a✝ : α
⊢ ↑(Quotient.lift id ⋯ ⟦a✝⟧) = ⟦a✝⟧

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
x : α
⊢ Quotient.lift id ⋯ ↑x = x

Tactic:
simp

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) 0 = vecCons (x • y) (x • v) 0

Tactic:
simp

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (x • vecCons y v) i.succ = vecCons (x • y) (x • v) i.succ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v + vecCons y w = vecCons (x + y) (v + w)

Tactic:
simp

Goal state after: