mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
S : Submodule R M
⊢ (f.domRestrict S).range = f.range ↔ Codisjoint S f.ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Defs

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : One M
⊢ HasFiniteMulSupport fun x ↦ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ ~ l₂
hp : {x | x ∈ l₁ ∧ p x = true}.Subsingleton
⊢ find? p l₁ = find? p l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Bool
l : List α
h : ∀ (x : α), x ∈ l → p₁ x = p₂ x
⊢ find? p₁ l = find? p₂ l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
⊢ ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
inst✝¹ : DecidableEq ι
κ : ι → Type u_5
inst✝ : Fintype ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
⊢ ∏ i, ∑ j ∈ t i, f i j = ∑ x ∈ piFinset t, ∏ i, f i (x i)

Tactic:
by

Goal state after:
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₂
S : Submodule R M
hf : Surjective ⇑f
⊢ Surjective ⇑(f.domRestrict S) ↔ Codisjoint S f.ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
s : Finset κ
g : ι → κ → R
⊢ ∑ f ∈ piFinset fun x ↦ s, ∏ i, g i (f i) = ∏ i, ∑ j ∈ s, g i j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ Eq.ndrec (motive := fun x ↦ {x_1 | x_1 ∈ x ∧ p x_1}.Subsingleton → Option α)
      (fun x ↦ List.find? (fun b ↦ decide (p b)) l₁) ⋯ =
    fun x ↦ List.find? (fun b ↦ decide (p b)) l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
hp : {x | x ∈ s ∧ p x}.Subsingleton
⊢ find? p s hp = some a → p a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
⊢ {x | x ∈ 0 ∧ p x}.Subsingleton

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
hp : {x | x ∈ a ::ₘ s ∧ p x}.Subsingleton
h : ¬p a
⊢ {x | x ∈ s ∧ p x}.Subsingleton

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
hp : {x | x ∈ a ::ₘ s ∧ p x}.Subsingleton
⊢ find? p (a ::ₘ s) hp = if h : p a then some a else find? p s ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
hp : {x | x ∈ s + t ∧ p x}.Subsingleton
⊢ {x | x ∈ s ∧ p x} ⊆ {x | x ∈ s + t ∧ p x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
hp : {x | x ∈ s + t ∧ p x}.Subsingleton
⊢ {x | x ∈ t ∧ p x} ⊆ {x | x ∈ s + t ∧ p x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
hp : {x | x ∈ s + t ∧ p x}.Subsingleton
⊢ find? p (s + t) hp = (find? p s ⋯).or (find? p t ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: κ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
⊢ (∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i ↦ s, ∏ i, f (p i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, ∑ p ∈ {True, False}, if p then f i else g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.pi fun x ↦ {True, False}, {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h} ∈ s.powerset

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.powerset, (fun a_1 x ↦ a_1 ∈ a) ∈ s.pi fun x ↦ {True, False}

Tactic:
by

Goal state after:
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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
this : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
by

Goal state after:
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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
suffices (⨆ i ∈ s, (p i).comap f) ⊔ LinearMap.ker f = ⊤ by
    rw [← this, left_eq_sup]; exact le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)

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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
⊢ (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.pi fun x ↦ {True, False}, (fun a_1 x ↦ a_1 ∈ {a_2 ∈ s | ∃ (h : a_2 ∈ s), a a_2 h}) = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.powerset, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a

Tactic:
mem_powerset

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ⊆ s, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
hp : {x | x ∈ s ∧ p x}.Subsingleton
⊢ find? p s hp = some a ↔ a ∈ s ∧ p a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
⊢ ∃ s, sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.powerset, {a_1 ∈ s | ∃ (h : a_1 ∈ s), (fun a_2 x ↦ a_2 ∈ a) a_1 h} = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ sSup {a | a ≤ ⊤ ∧ IsAtom a} = ⊤

Tactic:
by

Goal state after:
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 τ₁₂
ι : Type u_8
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ ∃ s, sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
by

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}.Subsingleton
⊢ find? p s hp = none ↔ ∀ (a : α), a ∈ s → ¬p a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x ↦ {True, False}
⊢ (∏ a_1 ∈ s.attach, if a ↑a_1 ⋯ then f ↑a_1 else g ↑a_1) =
    (∏ a ∈ s with ∃ (h : a ∈ s), a a h, f a) * ∏ a ∈ s \ {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h}, g a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b : α
h : sSup {a | a ≤ b ∧ IsAtom a} = b
s : Set α
s_ind : sSupIndep s
left✝ : Disjoint ⊥ (sSup s)
s_atoms : ⊥ ⊔ sSup s = b ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
⊢ sSup s = b ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝² : DecidablePred p
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
s : Multiset α
hp₁ : {x | x ∈ s ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ s → (p₁ x ↔ p₂ x)
⊢ {x | x ∈ s ∧ p₂ x}.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
⊢ sSup {a | a ≤ ⊤ ∧ IsAtom a} = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ sSup {a | IsAtom a} = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
a✝ : List α
hp₁ : {x | x ∈ ⟦a✝⟧ ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ ⟦a✝⟧ → (p₁ x ↔ p₂ x)
x : α
hx : x ∈ a✝
⊢ x ∈ ⟦a✝⟧

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
a✝ : List α
hp₁ : {x | x ∈ ⟦a✝⟧ ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ ⟦a✝⟧ → (p₁ x ↔ p₂ x)
x : α
hx : x ∈ a✝
⊢ decide (p₁ x) = decide (p₂ x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
s : Multiset α
hp₁ : {x | x ∈ s ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ s → (p₁ x ↔ p₂ x)
⊢ find? p₁ s hp₁ = find? p₂ s ⋯

Tactic:
by

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

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α ↔ IsAtomistic α

Tactic:
by

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

Goal state before:
pp: M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst✝⁴ : Semiring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
this : ⨆ i ∈ s, comap f.range.subtype (p i) = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
by

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
⊢ find? p s ⋯ = some (choose p s hp)

Tactic:
by

Goal state after:
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, (f i + 1) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Tactic:
by

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

Goal state before:
pp: M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst✝⁴ : Semiring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i ∈ ∅, (f i + g i) = ∏ i ∈ ∅, f i + ∑ i ∈ ∅, (g i * ∏ j ∈ ∅ with j < i, (f j + g j)) * ∏ j ∈ ∅ with i < j, f j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝ : Zero M
⊢ Injective toFun

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : IsEmpty α
f g : α →₀ M
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : Subsingleton M
f g : α →₀ M
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
h : Nontrivial (α →₀ M)
⊢ Nontrivial M

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ ⇑f = 0 ↔ f = 0

Tactic:
by

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
⊢ g a = 0

Tactic:
by

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
⊢ f a = g a

Tactic:
by

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 : α
⊢ f a = g a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ f.support.Nonempty ↔ f ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ #f.support = 0 ↔ f = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ HasFiniteSupport ⇑f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ ↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : Unique α
f g : α →₀ M
h : f default = g default
a : α
⊢ f a = g a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ (a : α), a ∈ onFinsetSupport s f ↔ f a ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support = {a ∈ s | f a ≠ 0}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝ : Zero M
f : α →₀ M
⊢ ∀ (a : α), f a ≠ 0 → a ∈ f.support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ onFinset f.support ⇑f ⋯ = f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
⊢ a ∈ (onFinset s f hf).support ↔ f a ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α → M
hf : (Function.support f).Finite
⊢ (ofSupportFinite f hf).support = hf.toFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ (f ∘ ⇑g) a ≠ 0 → a ∈ g.support

Tactic:
by

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

Goal state after:
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
a : α →₀ M
f : M → N
hf : Injective f
h : f 0 = 0
⊢ mapRange f h a = 0 ↔ a = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e₁ : N → O
e₂ : M → N
he₁ : e₁ 0 = 0
he₂ : e₂ 0 = 0
f : α →₀ M
⊢ (e₁ ∘ e₂) 0 = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
⊢ (mapRange e he0 f).support = f.support

Tactic:
by

Goal state after:
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✝⁶ : Ring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p < p'
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'

Tactic:
by

Goal state after:
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
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ ∀ (a : α), (if a ∈ g.support then f a else 0) ≠ 0 → a ∈ g.support

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Submodule R M
x : M
⊢ Disjoint s (R ∙ x) ↔ ∀ (r : R), r • x ∈ s → r • x = 0

Tactic:
by

Goal state after:
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
e : M → N
he₀ : e 0 = 0
⊢ Set.range (mapRange e he₀) = {g | ∀ (i : α), g i ∈ Set.range e}

Tactic:
by

Goal state after:
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
e : M → N
he₀ : e 0 = 0
he : Injective e
⊢ Injective (mapRange e he₀)

Tactic:
by

Goal state after:
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
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ Surjective (mapRange e he₀)

Tactic:
← Set.range_eq_univ,

Goal state after:
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ Set.range (mapRange e he₀) = Set.univ
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
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ Surjective (mapRange e he₀)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
⊢ e.symm 0 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
x : ι →₀ M
⊢ mapRange ⇑e.symm ⋯ (mapRange (⇑e) hf x) = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
x : ι →₀ N
⊢ mapRange (⇑e) hf (mapRange ⇑e.symm ⋯ x) = x

Tactic:
by

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

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
y : V
hyq : y ∈ q
hyp : y ∉ s
⊢ ∃ c, ∃ z ∈ s, c • x + z = y

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
M : Type u_4
inst✝ : Zero M
⊢ equiv (Equiv.refl M) ⋯ = Equiv.refl (ι →₀ M)

Tactic:
by

Goal state after: