mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x✝¹ x✝ : M
⊢ x✝¹ ~ᵤ x✝ ↔ x✝¹ = x✝

Tactic:
associated_iff_eq

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x✝¹ x✝ : M
⊢ x✝¹ = x✝ ↔ x✝¹ = x✝
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
x : ↥f.range
⊢ f ((ofInjective f h).symm x) = ↑x

Tactic:
obtain ⟨-, ⟨y, rfl⟩⟩ := x

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
y : M
⊢ f ((ofInjective f h).symm ⟨f y, ⋯⟩) = ↑⟨f y, ⋯⟩
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case mp.smul₁
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
t : R
n : M
mem : n ∈ {r} • N
h : ∃ m ∈ N, n = r • m
⊢ ∃ m ∈ N, t • n = r • m

Tactic:
rcases h with ⟨n, hn, rfl⟩

Goal state after:
case mp.smul₁
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
t : R
n : M
hn : n ∈ N
mem : r • n ∈ {r} • N
⊢ ∃ m ∈ N, t • r • n = r • m
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
h : ↑x ⊔ b ≤ ↑y ⊔ b
⊢ a ⊓ b ⊔ ↑x ≤ ↑y

Tactic:
inf_sup_assoc_of_le _ x.prop.2,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
h : ↑x ⊔ b ≤ ↑y ⊔ b
⊢ a ⊓ (b ⊔ ↑x) ≤ ↑y
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R (insert 0 s) ≤ span R s

Tactic:
span_le,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ insert 0 s ⊆ ↑(span R s)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
s : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
t : Set N
p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : y ∈ span R t), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : x ∈ span R s), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : x ∈ span R s) (hy : y ∈ span R s) (hz : z ∈ span R t),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : x ∈ span R s) (hy : y ∈ span R t) (hz : z ∈ span R t),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : a ∈ span R s
hb : b ∈ span R t
⊢ p a b ha hb

Tactic:
induction hb using span_induction with
  | mem z hz => induction ha using span_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
  | zero => exact zero_right a ha
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | smul _ _ _ h => exact smul_right _ _ _ _ _ h

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
⊢ ∃ b', b ⊓ b' = a ∧ b ⊔ b' = c

Tactic:
by
  obtain ⟨d, hdisjoint, hcodisjoint⟩ := exists_isCompl b
  refine ⟨(d ⊔ a) ⊓ c, ?_, ?_⟩
  · simpa [← inf_assoc, ← inf_sup_assoc_of_le _ hb, hdisjoint.eq_bot] using hb.trans hc
  · simp [← sup_inf_assoc_of_le _ hc, ← sup_assoc, hcodisjoint.eq_top]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ IsCoatom a ↔ ↑a ⋖ b

Tactic:
← covBy_top_iff

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ a ⋖ ⊤ ↔ ↑a ⋖ b
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝¹ : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α✝¹
α✝ : Type u_4
a✝ b : α✝
inst✝³ : Preorder α✝
α : Type u_5
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsStronglyAtomic α
a : α
⊢ ⊥ < a → ∃ a_2, IsAtom a_2 ∧ a_2 ≤ a

Tactic:
refine fun hlt ↦ ?_

Goal state after:
ι : Sort u_1
α✝¹ : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α✝¹
α✝ : Type u_4
a✝ b : α✝
inst✝³ : Preorder α✝
α : Type u_5
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsStronglyAtomic α
a : α
hlt : ⊥ < a
⊢ ∃ a_1, IsAtom a_1 ∧ a_1 ≤ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
⊢ ⟨c, hc⟩ < ⟨x, ⋯⟩

Tactic:
by simpa
        using! hcx.lt

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

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_9
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ R ∙ r • x ≤ R ∙ x

Tactic:
span_le,

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_9
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ {r • x} ⊆ ↑(R ∙ x)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
p : Submodule R M
⊢ R ∙ m ≤ p ↔ m ∈ p

Tactic:
span_le,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
p : Submodule R M
⊢ {m} ⊆ ↑p ↔ m ∈ p
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T

Tactic:
refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx

Goal state after:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T

case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ 0 ∈ span R ↑T

case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (x y : M),
    x ∈ span R S →
      y ∈ span R S → (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T

case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (a : R), ∀ x ∈ span R S, (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ ⨆ i, f i.down ∈ s

Tactic:
← Finset.sup'_univ_eq_ciSup

Goal state after:
case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ (univ.sup' ⋯ fun i ↦ f i.down) ∈ s
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ {i, j}.SupIndep f ↔ Disjoint (f i) (f j)

Tactic:
suffices Disjoint (f i) (f j) → Disjoint (f j) ((Finset.erase {i, j} j).sup f) by
    simpa [supIndep_iff_disjoint_erase, hij]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ Disjoint (f i) (f j) → Disjoint (f j) (({i, j}.erase j).sup f)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
⊢ ∀ (u : α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → IsLUB s u → k ≤ u → ∃ x ∈ s, k ≤ x

Tactic:
u

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
⊢ s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → IsLUB s u → k ≤ u → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})

Tactic:
iSupIndep_def'

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ (∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))) ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})
Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas

Goal state before:
pp: case h
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i ∈ s, f i = ∏ x, ⋯.choose * ⋯.choose

Tactic:
← Finset.prod_coe_sort

Goal state after:
case h
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i, f ↑i = ∏ x, ⋯.choose * ⋯.choose
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₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
⊢ span R (⇑f ⁻¹' s) ≤ comap f (span R₂ s)

Tactic:
span_le,

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₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
⊢ ⇑f ⁻¹' s ⊆ ↑(comap f (span R₂ s))
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr.smul
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ : M
a : R
x : M
hx : x ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
⊢ a • f ⟨x, hx⟩ = a • g ⟨x, hx⟩

Tactic:
rw [hx']

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

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
| fun x ↦ (φ x) (mulSingle i m x)

Tactic:
j

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
j : ι
| (φ j) (mulSingle i m j)
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: case inl
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
ha : 0 = a
⊢ a * l.prod = 0

pp: case inr
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
hl : 0 ∈ l
⊢ a * l.prod = 0

Tactic:
exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (prod_eq_zero hl)]

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

Goal state before:
pp: case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) ≤ -span R s

Tactic:
span_le,

Goal state after:
case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -s ⊆ ↑(-span R s)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R s ≤ -span R (-s)

Tactic:
span_le,

Goal state after:
case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ s ⊆ ↑(-span R (-s))
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₂
hf : Surjective ⇑f
p : Submodule R M
le : f.ker ≤ p
hp : IsCoatom p
⊢ IsCoatom (comap f (map f p))

Tactic:
by rwa [comap_map_eq_self le]

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:
induction s using Quotient.inductionOn
  simp only [quot_mk_to_coe, cons_coe]
  grind

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
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
⊢ Codisjoint s (K ∙ x)

Tactic:
← covBy_top_iff

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
⊢ Codisjoint s (K ∙ 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✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p : Submodule R M
⊢ map f p = ⊤ ↔ p ⊔ f.ker = ⊤

Tactic:
← top_le_iff,

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✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p : Submodule R M
⊢ ⊤ ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
a b : R
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s

Tactic:
rw [← prod_const, prod_add]
  refine Finset.sum_congr rfl fun t ht => ?_
  rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]

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

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

Tactic:
ext; simp [single_apply, Pi.single_apply, eq_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
⊢ embDomain f (v + w) = embDomain f v + embDomain f w

Tactic:
by
    ext b
    by_cases h : b ∈ Set.range f
    · rcases h with ⟨a, rfl⟩
      simp
    · simp only [coe_add, Pi.add_apply, embDomain_of_notMem_range _ _ _ h, add_zero]

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ (single f₁ g₁).support ⊆ {f₁, f₂}

Tactic:
exact subset_trans Finsupp.support_single_subset (by simp)

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ (single f₂ g₂).support ⊆ {f₁, f₂}

Tactic:
exact subset_trans Finsupp.support_single_subset (by simp)

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

Goal state before:
pp: case pos
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∈ s
h✝ : a ∈ {a | 0 ≤ f a}
⊢ f a ≤ f a

pp: case neg
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∈ s
h✝ : a ∉ {a | 0 ≤ f a}
⊢ f a ≤ 0

pp: case pos
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∉ s
h✝ : a ∈ {a | 0 ≤ f a}
⊢ 0 ≤ f a

pp: case neg
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∉ s
h✝ : a ∉ {a | 0 ≤ f a}
⊢ 0 ≤ 0

Tactic:
exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd✝ : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
f1✝ f2✝ : α →₀ M
hd : Disjoint f1✝.support f2✝.support
x : α
hx : x ∈ f1✝.support
⊢ g x (f1✝ x + f2✝ x) = g x (f1✝ x)

Tactic:
simp only [notMem_support_iff.mp (disjoint_left.mp hd hx), add_zero]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
x✝¹ : ↥s
x✝ : x✝¹ ∈ s.attach
⊢ single (↑x✝¹) ((indicator s f) ↑x✝¹) = single (↑x✝¹) (f ↑x✝¹ ⋯)

Tactic:
indicator_of_mem

Goal state after:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
x✝¹ : ↥s
x✝ : x✝¹ ∈ s.attach
⊢ single (↑x✝¹) (f ↑x✝¹ ?hi) = single (↑x✝¹) (f ↑x✝¹ ⋯)

case hi
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
x✝¹ : ↥s
x✝ : x✝¹ ∈ s.attach
⊢ ↑x✝¹ ∈ s
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
x✝¹ : ↥s
x✝ : x✝¹ ∈ s.attach
⊢ h (↑x✝¹) ((indicator s f) ↑x✝¹) = h (↑x✝¹) (f ↑x✝¹ ⋯)

Tactic:
indicator_of_mem

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
x✝¹ : ↥s
x✝ : x✝¹ ∈ s.attach
⊢ h (↑x✝¹) (f ↑x✝¹ ?hi) = h (↑x✝¹) (f ↑x✝¹ ⋯)

case hi
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
x✝¹ : ↥s
x✝ : x✝¹ ∈ s.attach
⊢ ↑x✝¹ ∈ s
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 List.max_le_of_forall_le _ _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' ↑(single b m).support)
a : α
⊢ (comapDomain f (single b m) hf) a = 0 a

Tactic:
simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' ↑(single b m).support)
a : α
⊢ b = f a → m = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
h : a ∉ f.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
simp_rw [Multiset.sum_cons, mem_support_iff, add_apply, notMem_support_iff.1 h,
          zero_add] at ha
        rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩
        exact ⟨f', Multiset.mem_cons_of_mem h₀, h₁⟩

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ {x ∈ s | f x ≠ 1} ⊆ t

Tactic:
by simpa only [subset_iff, mem_filter, and_imp]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < ∏ j ∈ t, f j

Tactic:
classical calc
    ∏ j ∈ s, f j < ∏ j ∈ insert i s, f j := by
      rw [prod_insert hs]
      exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt
    _ ≤ ∏ j ∈ t, f j := by
      apply prod_le_prod_of_subset_of_one_le'
      · simp [Finset.insert_subset_iff, h, ht]
      · intro x hx h'x
        simp only [mem_insert, not_or] at h'x
        exact hle x hx h'x.2

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

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ i ∈ l.splitSupport ↔ l.split i ≠ 0

Tactic:
by
  classical rw [splitSupport, mem_image, Ne, ← support_eq_empty, ← Ne,
    ← Finset.nonempty_iff_ne_empty, split, comapDomain, Finset.Nonempty]
  simp only [Finset.mem_preimage, exists_and_right, exists_eq_right, mem_support_iff,
    Sigma.exists, Ne]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Tactic:
have H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i := fun i hi ↦ div_nonneg (sq_nonneg _) (hg' i hi)

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Tactic:
by
  have hg' : ∀ i ∈ s, 0 ≤ g i := fun i hi ↦ (hg i hi).le
  have H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i := fun i hi ↦ div_nonneg (sq_nonneg _) (hg' i hi)
  refine div_le_of_le_mul₀ (sum_nonneg hg') (sum_nonneg H)
    (sum_sq_le_sum_mul_sum_of_sq_le_mul _ H hg' fun i hi ↦ ?_)
  rw [div_mul_cancel₀]
  exact (hg i hi).ne'

Goal state after: