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
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ ∀ (a : M) (b : M'), a ∈ p ⊔ p' → b ∈ q₁ ⊔ q₁' → (a, b) ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ ∀ (a : M) (b : M'), a ∈ p ⊔ p' → b ∈ q₁ ⊔ q₁' → (a, b) ∈ p.prod q₁ ⊔ p'.prod q₁'
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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
N : Submodule R M
f : ↥N →ₛₗ[σ₁₂] M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
⊢ sSup (comap N.subtype '' s) = ⊤

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
N : Submodule R M
f : ↥N →ₛₗ[σ₁₂] M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
⊢ sSup (comap N.subtype '' s) = ⊤
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
⊢ x ∈ (s ⊔ t) ⊓ p ↔ x ∈ s ⊔ t ⊓ p

Tactic:
;

Goal state after:
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
⊢ x ∈ (s ⊔ t) ⊓ p ↔ x ∈ s ⊔ t ⊓ p
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
⊢ p ⊔ s ⊓ t = s ⊓ (t ⊔ p)

Tactic:
inf_comm,

Goal state after:
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
⊢ p ⊔ t ⊓ s = s ⊓ (t ⊔ p)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
⊢ (p ⊔ t) ⊓ s = s ⊓ (t ⊔ p)

Tactic:
inf_comm,

Goal state after:
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
⊢ s ⊓ (p ⊔ t) = s ⊓ (t ⊔ p)
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
s : Finset ι
inst✝ : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
x : ι
hx : x ∈ s.val
hy : f x ∈ Multiset.map (fun i ↦ f i) s.val
⊢ a ∣ f x

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_4
s : Finset ι
inst✝ : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
x : ι
hx : x ∈ s.val
hy : f x ∈ Multiset.map (fun i ↦ f i) s.val
⊢ a ∣ f x
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
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
y : M
hy : y ∈ ↑p
z : M₂
hz : z ∈ q
eq : z = f (x - y)
⊢ x ∈ p

Tactic:
;

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
q : Submodule R₂ M₂
le : comap f q ≤ p
x : M
h : x ∈ comap f (map f p ⊔ q)
y : M
hy : y ∈ ↑p
z : M₂
hz : z ∈ q
eq : z = f (x - y)
⊢ x ∈ p
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

Tactic:
piecewise_eq_of_notMem _ _ _ h,

Goal state after:
case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = g x
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 q : Submodule R M
hpq : Disjoint p q
hker : f.ker ≤ q
⊢ Disjoint (map f p) (map f q)

Tactic:
by
  rw [disjoint_iff, map_inf_eq_map_inf_comap, comap_map_eq, eq_bot_iff, map_le_iff_le_comap,
    comap_bot, sup_eq_left.mpr hker, hpq.eq_bot]
  exact bot_le

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
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
hv : a ∈ s
⊢ False

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
hv : a ∈ s
⊢ False
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
this✝ : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
this : ¬(mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
this✝ : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
this : ¬(mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}
⊢ False
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 = ∏ i, ∑ j ∈ s, f j

Tactic:
;

Goal state after:
κ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
⊢ (∑ a ∈ s, f a) ^ n = ∏ i, ∑ j ∈ s, f j
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 = ⊤
⊢ f.ker ≤ ⨆ i ∈ s, comap f (p i)

Tactic:
;

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
this : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
⊢ f.ker ≤ ⨆ i ∈ s, comap f (p i)
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),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ a a_1 h ∈ {False}) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ a a_1 h ∈ {False}) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
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, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a

Tactic:
;

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.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) = ⨆ i ∈ s, comap f.rangeRestrict (comap f.range.subtype (p i))

Tactic:
;

Goal state after:
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) = ⨆ i ∈ s, comap f.rangeRestrict (comap f.range.subtype (p i))
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
x : α
⊢ f x = g x

Tactic:
;

Goal state after:
α : 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
x : α
⊢ f x = g x
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
x : α
⊢ f x = g x

Tactic:
;

Goal state after:
α : 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
x : α
⊢ f x = g x
Module: Mathlib.Data.Finsupp.Defs

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

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
h : Subsingleton M
⊢ Subsingleton (α →₀ M)
Module: Mathlib.Data.Finsupp.Defs

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

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ f.support = ∅ ↔ f = 0
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
⊢ onFinsetSupport s f = {a ∈ s | ¬f a = 0}

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ onFinsetSupport s f = {a ∈ s | ¬f a = 0}
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
⊢ {a ∈ s | f a ≠ 0} = {a ∈ s | ¬f a = 0}

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ {a ∈ s | f a ≠ 0} = {a ∈ s | ¬f a = 0}
Module: Mathlib.Data.Finsupp.Defs

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

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (onFinset f.support ⇑f ⋯) a✝ = f a✝
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
a✝ : α
⊢ a✝ ∈ (ofSupportFinite f hf).support ↔ a✝ ∈ hf.toFinset

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α → M
hf : (Function.support f).Finite
a✝ : α
⊢ a✝ ∈ (ofSupportFinite f hf).support ↔ a✝ ∈ hf.toFinset
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 : α
⊢ g a = 0 → (f ∘ ⇑g) a = 0

Tactic:
;

Goal state after:
α : 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 : α
⊢ g a = 0 → (f ∘ ⇑g) a = 0
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
  obtain (⟨h, -⟩ | ⟨-, h⟩) := Prod.mk_lt_mk.mp <| strictMono_inf_prod_sup (z := LinearMap.ker f) hab
  · simpa [inf_comm] using Or.inr h
  · apply Or.inl <| map_lt_map_of_le_of_sup_lt_sup hab.le h

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 (R ∙ x) s ↔ ∀ (r : R), r • x ∈ s → r • x = 0

Tactic:
;

Goal state after:
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 (R ∙ x) s ↔ ∀ (r : R), r • x ∈ s → r • x = 0
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
a✝ : ι
⊢ (mapRange ⇑e.symm ⋯ (mapRange (⇑e) hf x)) a✝ = x a✝

Tactic:
;

Goal state after:
α : 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
a✝ : ι
⊢ (mapRange ⇑e.symm ⋯ (mapRange (⇑e) hf x)) a✝ = x a✝
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
a✝ : ι
⊢ (mapRange (⇑e) hf (mapRange ⇑e.symm ⋯ x)) a✝ = x a✝

Tactic:
;

Goal state after:
α : 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
a✝ : ι
⊢ (mapRange (⇑e) hf (mapRange ⇑e.symm ⋯ x)) a✝ = x a✝
Module: Mathlib.Data.Finsupp.Defs

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

Tactic:
;

Goal state after:
ι : Type u_3
M : Type u_4
inst✝ : Zero M
x✝ : ι →₀ M
a✝ : ι
⊢ ((equiv (Equiv.refl M) ⋯) x✝) a✝ = ((Equiv.refl (ι →₀ M)) x✝) a✝
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
f₂ : N ≃ O
hf₂ : f₂ 0 = 0
x✝ : ι →₀ M
a✝ : ι
⊢ ((equiv (e.trans f₂) ⋯) x✝) a✝ = (((equiv e hf).trans (equiv f₂ hf₂)) x✝) a✝

Tactic:
;

Goal state after:
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
f₂ : N ≃ O
hf₂ : f₂ 0 = 0
x✝ : ι →₀ M
a✝ : ι
⊢ ((equiv (e.trans f₂) ⋯) x✝) a✝ = (((equiv e hf).trans (equiv f₂ hf₂)) x✝) a✝
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
f : α ↪ β
v : α →₀ M
b : β
this : DecidableEq β
x : α
⊢ x ∈ {x | x ∈ v.support.val ∧ f x = b} → ∀ ⦃y : α⦄, y ∈ {x | x ∈ v.support.val ∧ f x = b} → x = y

Tactic:
;

Goal state after:
α : 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
f : α ↪ β
v : α →₀ M
b : β
this : DecidableEq β
x : α
⊢ x ∈ {x | x ∈ v.support.val ∧ f x = b} → ∀ ⦃y : α⦄, y ∈ {x | x ∈ v.support.val ∧ f x = b} → x = y
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
x✝ : α →₀ M
a✝ : α
⊢ (embDomain (Embedding.refl α) x✝) a✝ = (id x✝) a✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
x✝ : α →₀ M
a✝ : α
⊢ (embDomain (Embedding.refl α) x✝) a✝ = (id x✝) a✝
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 y : M
⊢ (toSpanSingleton R M (x + y)) 1 = (toSpanSingleton R M x + toSpanSingleton R M y) 1

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (toSpanSingleton R M (x + y)) 1 = (toSpanSingleton R M x + toSpanSingleton R M y) 1
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
S : Type u_8
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass R S M
r : S
x : M
⊢ (toSpanSingleton R M (r • x)) 1 = (r • toSpanSingleton R M x) 1

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_8
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass R S M
r : S
x : M
⊢ (toSpanSingleton R M (r • x)) 1 = (r • toSpanSingleton R M x) 1
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →ₗ[R] M₂
x : M
⊢ (f ∘ₗ toSpanSingleton R M x) 1 = (toSpanSingleton R M₂ (f x)) 1

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →ₗ[R] M₂
x : M
⊢ (f ∘ₗ toSpanSingleton R M x) 1 = (toSpanSingleton R M₂ (f 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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ s ⊆ ↑(f.eqLocus g) ↔ Set.EqOn (⇑f) (⇑g) s

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ s ⊆ ↑(f.eqLocus g) ↔ Set.EqOn (⇑f) (⇑g) s
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n < k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
rw [← mem_range] at hnk

Goal state after:
case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : Zero M
x✝ : ι →₀ M
a✝ : ι
⊢ ((zeroHom (ZeroHom.id M)) x✝) a✝ = ((ZeroHom.id (ι →₀ M)) x✝) a✝

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : Zero M
x✝ : ι →₀ M
a✝ : ι
⊢ ((zeroHom (ZeroHom.id M)) x✝) a✝ = ((ZeroHom.id (ι →₀ M)) x✝) a✝
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : ZeroHom N O
f₂ : ZeroHom M N
x✝ : ι →₀ M
a✝ : ι
⊢ ((zeroHom (f.comp f₂)) x✝) a✝ = (((zeroHom f).comp (zeroHom f₂)) x✝) a✝

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : ZeroHom N O
f₂ : ZeroHom M N
x✝ : ι →₀ M
a✝ : ι
⊢ ((zeroHom (f.comp f₂)) x✝) a✝ = (((zeroHom f).comp (zeroHom f₂)) x✝) a✝
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
b : M
x✝ : α
⊢ (single a b) x✝ = Pi.single a b x✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
b : M
x✝ : α
⊢ (single a b) x✝ = Pi.single a b x✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f

Tactic:
;

Goal state after:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: M : Type u_8
inst✝ : AddZeroClass M
d : M
⊢ (AddEquiv.finsuppUnique.symm d) default = (single () d) default

Tactic:
;

Goal state after:
M : Type u_8
inst✝ : AddZeroClass M
d : M
⊢ (AddEquiv.finsuppUnique.symm d) default = (single () d) default
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
a : α
inst✝ : Subsingleton α
f : α →₀ M
b : α
⊢ (single a ((fun f ↦ f a) f)) b = f b

Tactic:
;

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
a : α
inst✝ : Subsingleton α
f : α →₀ M
b : α
⊢ (single a ((fun f ↦ f a) f)) b = f b
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
f✝ : α →₀ M
a✝ : α
b✝ : M
i : α
f : α →₀ M
a : α
b : M
this : DecidableEq α
⊢ Finset α

Tactic:
;

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
f✝ : α →₀ M
a✝ : α
b✝ : M
i : α
f : α →₀ M
a : α
b : M
this : DecidableEq α
⊢ Finset α
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : 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

Tactic:
;

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