mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case hab
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ t

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ #(s ^ 0) ≤ #s ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ {x | x ∈ s.sort fun x1 x2 ↦ x1 ≤ x2} = ↑s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ ↑(image (⇑(s.orderEmbOfFin h)) univ) = ↑s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case convert_3
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
x : Fin k
⊢ (i.succAbove ∘ Fin.cast ?convert_7) x ∈ {i}ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Finset α
t : Finset β
⊢ s ×ˢ t ^ 0 = (s ^ 0) ×ˢ (t ^ 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
j : Fin k
⊢ (RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb) j = i.succAbove (Fin.cast ⋯ j)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
⊢ ∀ (a : Fin n), (a ∈ Finset.univ.sort fun a b ↦ a ≤ b) ↔ a ∈ List.finRange n

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Subsingleton M
⊢ ∀ (g : R), g * 0 = 0 * g

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (s ^ 0).Nonempty

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case ofNat
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.ofNat a✝ = {a ^ Int.ofNat a✝}

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case negSucc
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.negSucc a✝ = {a ^ Int.negSucc a✝}

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
a : α
⊢ ↑(image (fun b ↦ a * b) t) = ↑(t.preimage (fun b ↦ a⁻¹ * b) ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
b : α
⊢ ↑(image (fun x ↦ x * b) t) = ↑(t.preimage (fun x ↦ x * b⁻¹) ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
a : α
⊢ image (fun b ↦ a⁻¹ * b) t = t.preimage (fun b ↦ a * b) ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
b : α
⊢ image (fun x ↦ x * b⁻¹) t = t.preimage (fun x ↦ x * b) ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
x✝ : 1 ≠ 0
⊢ ∀ (f : F) (s : Finset α), image (⇑f) (s ^ 1) = image (⇑f) s ^ 1

Tactic:
simp

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

Goal state before:
pp: case refine_1.zero
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ (lmapDomain R R u) 0 ∈ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
i : α
⊢ (lmapDomain R R u) (single i 1) = single (u i) 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
a : α
S : Set (Sublattice α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Lattice α
a : α
f : ι → Sublattice α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i

Tactic:
simp

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i
s : Finset (Subtype (Membership.mem S))
hs : m ∈ ⨆ i ∈ s, ↑i
⊢ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ S) s) ⊆ S

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support = 0 ↔ p = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (monomial 0).toFun 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ C 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝¹ : (i : κ) → Lattice (π i)
inst✝ : Nonempty κ
⊢ (pi univ fun x ↦ ⊥) = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
⊢ (monomial 0) 1 = X ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ ↑(pi univ L) = ↑⊥ ↔ ∃ i, ↑(L i) = ↑⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ X ^ 0 * p = p * X ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * X ^ 0 = (monomial (n + 0)) r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ n ∈ { toFinsupp := toFinsupp✝ }.support ↔ { toFinsupp := toFinsupp✝ }.coeff n ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ n ∉ p.support ↔ p.coeff n = 0

Tactic:
simp

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

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2

Tactic:
specialize hu ⟨_, ⟨_, hd1, rfl⟩, _, hc3, rfl⟩ ⟨_, hd3, _, ⟨_, hc2, rfl⟩, rfl⟩

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * c3 * (d3 * c2⁻¹) = d1⁻¹ * c1 * (d2 * c2⁻¹) → d1⁻¹ * c3 = d1⁻¹ * c1 ∧ d3 * c2⁻¹ = d2 * c2⁻¹
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
m : M
⊢ (f.inv * ↑f) m = m

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
m : M
⊢ (↑f * f.inv) m = m

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : End R M
x✝ : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⟨p, hp⟩ ≤ ⟨⊤, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : End R M
x✝ : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⟨⊥, ⋯⟩ ≤ ⟨p, hp⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (erase n 0).toFinsupp = toFinsupp 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (erase n ((monomial n) a)).toFinsupp = toFinsupp 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint ↑⟨p, hp⟩ ↑⟨q, hq⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint ↑⟨p, hp⟩ ↑⟨q, hq⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl ↑⟨p, hp⟩ ↑⟨q, hq⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
x✝ : M
⊢ (↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ image (fun n_1 ↦ ((monomial n) c).coeff n_1) {n} = {c}

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ C ↑n = ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬X.coeff 1 = coeff 0 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝ : CommRing R
⊢ (Multiset.map (fun a ↦ X - C a) 0).prod = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝ : CommRing R
⊢ ∀ (a b : Multiset R),
    (Multiset.map (fun a ↦ X - C a) (a + b)).prod =
      (Multiset.map (fun a ↦ X - C a) a).prod * (Multiset.map (fun a ↦ X - C a) b).prod

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
a✝ : (i : ι) × φ i
i✝ : ι
⊢ (((linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd)) ∘ₗ Finsupp.lsingle a✝) 1) i✝ =
    ((((mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R)) ∘ₗ Finsupp.lsingle a✝)
        1)
      i✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: case neg
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ 0 i' = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Tactic:
Finsupp.zero_apply,

Goal state after:
case neg
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ 0 = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
ji : (j : η) × ιs j
⊢ (Pi.basis s).repr (single ji.fst ((s ji.fst) ji.snd)) = Finsupp.single ji 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
x✝ : (i : ι) × φ i
⊢ single x✝.fst (f x✝.fst x✝.snd) =
    (⇑↑(finsuppLequivDFinsupp R).symm ∘ fun ix ↦ DFinsupp.single ix.fst (f ix.fst ix.snd)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
⊢ single (u i) 1 = (lmapDomain R R u) (single i 1)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : f.range = ⊤
⊢ f.range = ⊤

Tactic:
hf

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : f.range = ⊤
⊢ ⊤ = ⊤
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝² x✝¹ : M
a✝¹ : ι
x✝ : M →ₗ[R] N
a✝ : ι
⊢ ((mapRange.linearMap (id.flip (x✝² + x✝¹)) ∘ₗ lsingle a✝¹) x✝) a✝ =
    (((mapRange.linearMap (id.flip x✝²) + mapRange.linearMap (id.flip x✝¹)) ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝² : R
x✝¹ : M
a✝¹ : ι
x✝ : M →ₗ[R] N
a✝ : ι
⊢ ((mapRange.linearMap (id.flip (x✝² • x✝¹)) ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((((RingHom.id R) x✝² • mapRange.linearMap (id.flip x✝¹)) ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Finite ι
x : M →ₗ[R] ι →₀ N
x✝ : M
a✝ : ι
⊢ (((finsuppLinearMap S) (equivFunOnFinite.symm fun i ↦ lapply i ∘ₗ x)) x✝) a✝ = (x x✝) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : ↥p
⊢ ↑x = (p.prodEquivOfIsCompl q h) (x, 0)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : ↥q
⊢ ↑x = (p.prodEquivOfIsCompl q h) (0, x)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ ↑t2
⊢ x ∈ ↑s

Tactic:
have : x ∈ span R t2 := subset_span hx

Goal state after:
case a.refine_2
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ ↑t2
this : x ∈ span R ↑t2
⊢ x ∈ ↑s
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
⊢ ∀ (x : E), ↑(p.prodEquivOfIsCompl q hpq).symm x = ((p.projectionOnto q hpq).prod (q.projectionOnto p ⋯)) x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ p ≤ (q.projectionOnto p ⋯).ker

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x✝ : ↥q
⊢ ↑((p.liftQ (q.projectionOnto p ⋯) ⋯ ∘ₗ p.mkQ ∘ₗ q.subtype) x✝) = ↑(LinearMap.id x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
a : ↥p
b : ↥q
right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = ↑a + ↑b → r = a ∧ s = b
⊢ (ofIsCompl hpq φ ψ) (↑a + ↑b) = (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯) (↑a + ↑b)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ₁ φ₂ : ↥p →ₗ[R] F
ψ₁ ψ₂ : ↥q →ₗ[R] F
⊢ ∀ (u : ↥p), (φ₁ + φ₂) u = (ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ₁ φ₂ : ↥p →ₗ[R] F
ψ₁ ψ₂ : ↥q →ₗ[R] F
⊢ ∀ (u : ↥q), (ψ₁ + ψ₂) u = (ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_7
inst✝⁴ : CommRing R
E : Type u_8
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_9
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
c : R
⊢ ∀ (u : ↥p), (c • φ) u = (c • ofIsCompl h φ ψ) ↑u

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_7
inst✝⁴ : CommRing R
E : Type u_8
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_9
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
c : R
⊢ ∀ (u : ↥q), (c • ψ) u = (c • ofIsCompl h φ ψ) ↑u

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
p q : Submodule R E
M : Type u_6
inst✝¹ : AddCommMonoid M
h : IsCompl p q
inst✝ : Module R M
f : M →ₗ[R] ↥p
x✝ : M
⊢ ↑((p.projectionOnto q h ∘ₗ p.subtype ∘ₗ f) x✝) = ↑(f x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
p : Submodule R E
M : Type u_6
inst✝¹ : AddCommMonoid M
h✝ : IsComplemented p
inst✝ : Module R M
q : Submodule R E
h : IsCompl p q
f : ↥p →ₗ[R] M
x✝ : ↥p
⊢ ((fun f ↦ f ∘ₗ p.subtype) (f ∘ₗ p.projectionOnto q h)) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
x : ↥p
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯) ↑x = φ x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
x : ↥q
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯) ↑x = ψ x

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℕ
h✝ : IsEmpty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i

Tactic:
simp

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

Goal state before:
pp: s : Set ℕ∞
⊢ (∃ a ∈ s, a < 1) ↔ 0 ∈ s

Tactic:
simp

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

Goal state before:
pp: ι : Sort u_1
⊢ ⨆ x, 0 = 0

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Sort u_2
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), 0 * f i ≤ d
⊢ 0 * ⨆ i, f i ≤ d

Tactic:
simp

Goal state after: