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

Goal state before:
pp: case mp
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
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx✝ : y + z = x
hyzx : z = -y + x
⊢ z ∈ p

Tactic:
simpa using

Goal state after:
case mp
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
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx✝ : y + z = x
hyzx : z = -y + x
⊢ -y + x ∈ p
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr
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 y : M
hy : y ∈ s
z : M
hyzx : y + z = x
hz : z ∈ t
hz' : z ∈ p
⊢ x ∈ p

Tactic:
simpa using

Goal state after:
case mpr
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 y : M
hy : y ∈ s
z : M
hyzx : y + z = x
hz : z ∈ t
hz' : z ∈ p
⊢ y + z ∈ p
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : HasDistribNeg M
f : ι → M
⊢ ∏ x ∈ s, -f x = (-1) ^ #s * ∏ x ∈ s, f x

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : HasDistribNeg M
f : ι → M
⊢ ∏ x ∈ s, -f x = (-1) ^ #s * ∏ x ∈ s, f x
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_10
M : Type u_11
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q r : Submodule R M
h₁ : IsCompl q r
h₂ : q ≤ p
⊢ IsCompl (comap p.subtype q) (comap p.subtype r)

Tactic:
simpa using

Goal state after:
R : Type u_10
M : Type u_11
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q r : Submodule R M
h₁ : IsCompl q r
h₂ : q ≤ p
⊢ Disjoint (p ⊓ q) (p ⊓ r) ∧ p ⊓ q ⊔ p ⊓ r = p
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
x y : M
hy : y ∈ ↑p
e : f y = f x
⊢ x - y ∈ f.ker

Tactic:
simpa using

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
x y : M
hy : y ∈ ↑p
e : f y = f x
⊢ f x - f y = 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✝⁶ : 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
hz : f (x - y) ∈ q
⊢ x ∈ p

Tactic:
simpa using

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
hz : f (x - y) ∈ q
⊢ x ∈ p
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₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ p < map f q ⊔ p

Tactic:
simpa using

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₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ ¬q ≤ comap f p
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
i : α
j : γ
hj✝ : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
hi : {i} ⊆ mulSupport f
hs : ∀ ⦃i j : γ⦄, i ≠ j → ∀ ⦃x : Set α⦄, x ⊆ s i ∧ x ⊆ mulSupport f → x ⊆ s j ∧ x ⊆ mulSupport f → x ⊆ ⊥
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
i : α
j : γ
hj✝ : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
hi : {i} ⊆ mulSupport f
hs : ∀ ⦃i j : γ⦄, i ≠ j → ∀ ⦃x : Set α⦄, x ⊆ s i ∧ x ⊆ mulSupport f → x ⊆ s j ∧ x ⊆ mulSupport f → x ⊆ ⊥
⊢ False
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case insert
ι : 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
⊢ ⟨a, ⋯⟩ ∉ image (fun x ↦ ⟨↑x, ⋯⟩) s.attach

Tactic:
simpa using

Goal state after:
case insert
ι : 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
⊢ a ∉ s
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
hp₁ : {x | x ∈ ⟦l₁⟧ ∧ p x}.Subsingleton
hp₂ : {x | x ∈ ⟦l₂⟧ ∧ p x}.Subsingleton
x✝ : hp₁ ≍ hp₂
⊢ {x | x ∈ l₁ ∧ decide (p x) = true}.Subsingleton

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
hp₁ : {x | x ∈ ⟦l₁⟧ ∧ p x}.Subsingleton
hp₂ : {x | x ∈ ⟦l₂⟧ ∧ p x}.Subsingleton
x✝ : hp₁ ≍ hp₂
⊢ {x | x ∈ l₁ ∧ p x}.Subsingleton
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
l : List α
hp : {x | x ∈ ⟦l⟧ ∧ p x}.Subsingleton
⊢ List.find? (fun a ↦ decide (p a)) l = some a → p a

Tactic:
simpa using

Goal state after:
case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
l : List α
hp : {x | x ∈ ⟦l⟧ ∧ p x}.Subsingleton
⊢ List.find? (fun a ↦ decide (p a)) l = some a → p a
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:
simpa using

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ ∃ s, sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = ⊤ ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
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:
simpa using

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ sSup {a | IsAtom a} = ⊤
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:
simpa using

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

Goal state after:
α : 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✝
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case inl
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'
h : p ⊓ f.ker < p' ⊓ f.ker
⊢ map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'

Tactic:
simpa using

Goal state after:
case inl
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'
h : p ⊓ f.ker < p' ⊓ f.ker
⊢ map f p < map f p' ∨ p ⊓ f.ker < p' ⊓ f.ker
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
a b : α →₀ M
h : ∀ (a_1 : α), (mapRange e he₀ a) a_1 = (mapRange e he₀ b) a_1
⊢ ∀ (a_1 : α), a a_1 = b a_1

Tactic:
simpa using

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 : Injective e
a b : α →₀ M
h : ∀ (a_1 : α), (mapRange e he₀ a) a_1 = (mapRange e he₀ b) a_1
⊢ ∀ (a_1 : α), a a_1 = b a_1
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:
simpa using

Goal state after:
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
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
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ x ∈ q

Tactic:
q.add_mem_iff_left (hpq.le hz),

Goal state after:
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
c : K
z : V
hz : z ∈ s
hyq : c • x ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ x ∈ q
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
l₁ l₂ : α →₀ M
h : embDomain f l₁ = embDomain f l₂
a : α
⊢ l₁ a = l₂ a

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
l₁ l₂ : α →₀ M
h : embDomain f l₁ = embDomain f l₂
a : α
⊢ l₁ a = l₂ a
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
s : Submodule K V
x : V
⊢ Disjoint s (K ∙ x) ↔ x ∈ s → x = 0

Tactic:
simpa using

Goal state after:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
⊢ (∀ (r : K), ¬r = 0 → x ∈ s → x = 0) ↔ x ∈ s → x = 0
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
s : Submodule K V
x : V
hs : s ⋖ ⊤
hx : x ∉ s
⊢ Codisjoint s (K ∙ x)

Tactic:
simpa using

Goal state after:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hs : s ⋖ ⊤
hx : x ∉ s
⊢ s ⊔ K ∙ x = ⊤
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✝¹ x✝ : M
eq : toSpanSingleton R M x✝¹ = toSpanSingleton R M x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ x✝ : M
eq : toSpanSingleton R M x✝¹ = toSpanSingleton R M x✝
⊢ x✝¹ = x✝
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_5
R : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
⊢ ∏ a, (f a + g a) = ∑ t, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a

Tactic:
simpa using

Goal state after:
ι : Type u_5
R : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
⊢ ∏ a, (f a + g a) = ∑ x, (∏ a ∈ x, f a) * ∏ a ∈ univ \ x, g a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝¹ : CommMonoid β
f : ι → κ
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
⊢ Set.InjOn f ↑(s.preimage f hf)

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝¹ : CommMonoid β
f : ι → κ
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
⊢ ∀ ⦃x₁ : ι⦄, f x₁ ∈ s → ∀ ⦃x₂ : ι⦄, f x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂
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 α
this : DecidableEq M
⊢ Finset α

Tactic:
exact if b = 0 then f.support.erase a else insert a f.support

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case pos
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∈ s
⊢ s.mulIndicator f a ≤ y

Tactic:
simpa using

Goal state after:
case pos
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∈ s
⊢ f a ≤ y
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∉ s
⊢ s.mulIndicator f a ≤ y

Tactic:
simpa using

Goal state after:
case neg
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∉ s
⊢ 1 ≤ y
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ ⨅ i, (s i).mulIndicator f x ≤ 1

Tactic:
simpa using

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ ⨅ i, (s i).mulIndicator f x ≤ 1
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
⊢ ∃ i, a ∈ s i

Tactic:
simpa using

Goal state after:
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
⊢ ∃ i, a ∈ s i
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
hda : d a = 1
hda' : ∀ (i : α), i ≠ a → d i = 0
b : α
hb : ¬b = a
⊢ d b = (single a 1) b

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
hda : d a = 1
hda' : ∀ (i : α), i ≠ a → d i = 0
b : α
hb : ¬b = a
⊢ d b = 0
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
simpa using

Goal state after:
R : Type u_5
S : Type u_6
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
a b c : R
⊢ abv (a + -c) ≤ abv (a + -b) + abv (b + -c)
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsOrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ abv a ≤ abv (a - b) + abv b

Tactic:
simpa using

Goal state after:
R : Type u_5
S : Type u_6
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsOrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ abv a ≤ abv (a - b) + abv b
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv a - abv b ≤ abv (a + b)

Tactic:
simpa using

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv a ≤ abv (a + b) + abv b
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv (a - b) ≤ abv a + abv b

Tactic:
simpa using

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv (a - b) ≤ abv a + abv b
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: S : Type u_5
inst✝³ : Ring S
inst✝² : PartialOrder S
R : Type u_6
inst✝¹ : Ring R
abv : R → S
inst✝ : IsAbsoluteValue abv
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
simpa using

Goal state after:
S : Type u_5
inst✝³ : Ring S
inst✝² : PartialOrder S
R : Type u_6
inst✝¹ : Ring R
abv : R → S
inst✝ : IsAbsoluteValue abv
a b c : R
⊢ abv (a + -c) ≤ abv (a + -b) + abv (b + -c)
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
inst✝ : MulLeftMono α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
⊢ 1 ≤ prod ⟦l⟧

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
inst✝ : MulLeftMono α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
⊢ 1 ≤ l.prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
inst✝ : IsOrderedMonoid α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
x : α
hx : x ∈ ⟦l⟧
⊢ x ≤ prod ⟦l⟧

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
inst✝ : IsOrderedMonoid α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
x : α
hx : x ∈ ⟦l⟧
⊢ x ≤ l.prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
n : α
a✝ : List α
h : ∀ (x : α), x ∈ ⟦a✝⟧ → x ≤ n
⊢ prod ⟦a✝⟧ ≤ n ^ card ⟦a✝⟧

Tactic:
simpa using

Goal state after:
case h
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
n : α
a✝ : List α
h : ∀ (x : α), x ∈ ⟦a✝⟧ → x ≤ n
⊢ a✝.prod ≤ n ^ a✝.length
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
hs : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ l ≠ []

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
hs : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ ¬l = []
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
⊢ l ≠ ∅

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
⊢ ¬l = []
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝³ : CommMonoid α
m : Multiset α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : IsOrderedMonoid α
l : List α
⊢ prod ⟦l⟧ = 1 ↔ ∀ (x : α), x ∈ ⟦l⟧ → x = 1

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : CommMonoid α
m : Multiset α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : IsOrderedMonoid α
l : List α
⊢ l.prod = 1 ↔ ∀ (x : α), x ∈ l → x = 1
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
n : α
a✝ : List α
h : ∀ (x : α), x ∈ ⟦a✝⟧ → x ≤ n
⊢ fold max ⊥ ⟦a✝⟧ ≤ n

Tactic:
simpa using

Goal state after:
case h
α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
n : α
a✝ : List α
h : ∀ (x : α), x ∈ ⟦a✝⟧ → x ≤ n
⊢ List.foldr max ⊥ a✝ ≤ n
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 1 ≤ f i
⊢ 1 ≤ ∏ i ∈ s, f i

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 1 ≤ f i
⊢ 1 ≤ ∏ i ∈ s, f i
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

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

Tactic:
induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact mul_nonneg h.1 (hind h.2)

Goal state after: