mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case mp
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
f : F
⊢ ⇑f = 1 → f = 1

Tactic:
intro h

Goal state after:
case mp
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
f : F
h : ⇑f = 1
⊢ f = 1
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case mpr
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
f : F
⊢ f = 1 → ⇑f = 1

Tactic:
intro h

Goal state after:
case mpr
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
f : F
h : f = 1
⊢ ⇑f = 1
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case mp
F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
f : F'
⊢ ⇑f = id → f = 1

Tactic:
intro h

Goal state after:
case mp
F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
f : F'
h : ⇑f = id
⊢ f = 1
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case mpr
F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
f : F'
⊢ f = 1 → ⇑f = id

Tactic:
intro h

Goal state after:
case mpr
F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
f : F'
h : f = 1
⊢ ⇑f = id
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr
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
V : Submodule R M
f g : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
⊢ (∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩) → f = g

Tactic:
intro h

Goal state after:
case mpr
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
V : Submodule R M
f g : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
⊢ f = g
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
rw [iSup, h.directedOn_range.sSup_inf_eq, iSup_range]

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

Goal state before:
pp: case e'_1.mpr
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
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype → f = g

Tactic:
intro h

Goal state after:
case e'_1.mpr
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
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
h : f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype
⊢ f = g
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case refine_4.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ ∀ x ∈ ⋃ i, ↑(p i), r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

pp: case refine_4.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • 0 ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

pp: case refine_4.refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ ∀ (x y : M),
    x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
      y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
        r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
          r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) → r • (x + y) ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
· rintro x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩
      apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)
      exact smul_mem _ r hix

Goal state after:
case refine_4.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • 0 ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

case refine_4.refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ ∀ (x y : M),
    x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
      y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
        r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) →
          r • y ∈ AddSubmonoid.closure (⋃ i, ↑(p i)) → r • (x + y) ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: case mpr
α : 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
⊢ (∀ (i : α), ∃ y, e y = g i) → ∃ y, mapRange e he₀ y = g

Tactic:
intro h

Goal state after:
case mpr
α : 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
h : ∀ (i : α), ∃ y, e y = g i
⊢ ∃ y, mapRange e he₀ y = g
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ f.support ∪ {a} = cons a f.support ha

pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint f.support (single a b).support

Tactic:
union_comm,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ {a} ∪ f.support = cons a f.support ha

ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint f.support (single a b).support
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : ¬s = a
⊢ (f + f') s = f s + f' s

Tactic:
add_apply

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : ¬s = a
⊢ f s + f' s = f s + f' s
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ optionElim y f ≠ 0 → f ≠ 0 ∨ y ≠ 0

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : optionElim y f ≠ 0
⊢ f ≠ 0 ∨ y ≠ 0
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ f ≠ 0 ∨ y ≠ 0 → optionElim y f ≠ 0

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : f ≠ 0 ∨ y ≠ 0
⊢ optionElim y f ≠ 0
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case pos
α : 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 : ι
hi : a ∈ s i
⊢ ⨆ i, f i a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
iSup_apply

Goal state after:
case pos
α : 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 : ι
hi : a ∈ s i
⊢ ⨆ i, f i a ≤ ⨆ i, (s i).mulIndicator (f i) a
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
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ ∀ x ∈ f.support.erase y, g x ((erase y f) x) = g x (f x)

Tactic:
intro h

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
h : α
⊢ h ∈ f.support.erase y → g h ((erase y f) h) = g h (f h)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_1
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
⊢ ∃ a, d = single a 1

pp: case refine_2
α : Type u_1
d : α →₀ ℕ
⊢ (∃ a, d = single a 1) → (d.sum fun x n ↦ n) = 1

Tactic:
· have hd0 : d ≠ 0 := (by simp [·] at h1)
    obtain ⟨a, ha⟩ := ne_iff.mp hd0
    obtain ⟨hda, hda'⟩ : d a = 1 ∧ ∀ i ≠ a, d i = 0 := by
      rw [← add_sum_erase' _ a _ (fun _ ↦ rfl), Nat.add_eq_one_iff, or_iff_not_imp_left] at h1
      simp_all +contextual [sum, support_erase, sum_eq_zero_iff, mem_erase, erase_ne]
    use a
    ext b
    by_cases hb : b = a
    · rw [hb, single_eq_same, hda]
    · simpa only [single_eq_of_ne hb] using hda' b hb

Goal state after:
case refine_2
α : Type u_1
d : α →₀ ℕ
⊢ (∃ a, d = single a 1) → (d.sum fun x n ↦ n) = 1
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
x : Option α
⊢ (optionElim (i + j) (a + b)) x = (optionElim i a + optionElim j b) x

Tactic:
cases x

Goal state after:
case none
α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
⊢ (optionElim (i + j) (a + b)) none = (optionElim i a + optionElim j b) none

case some
α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
val✝ : α
⊢ (optionElim (i + j) (a + b)) (Option.some val✝) = (optionElim i a + optionElim j b) (Option.some val✝)
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 → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (∏ x ∈ f1.support, g x ((f1 + f2) x)) * ∏ x ∈ f2.support, g x ((f1 + f2) x) =
    (∏ x ∈ f1.support, g x (f1 x + f2 x)) * ∏ x ∈ f2.support, g x (f1 x + f2 x)

Tactic:
add_apply

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

Goal state before:
pp: α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : Multiset α
n : α
h : ∀ (x : α), x ∈ l → x ≤ n
⊢ fold max ⊥ l ≤ n

Tactic:
induction l using Quotient.inductionOn

Goal state after:
case h
α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
n : α
a✝ : List α
h : ∀ (x : α), x ∈ ⟦a✝⟧ → x ≤ n
⊢ fold max ⊥ ⟦a✝⟧ ≤ n
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0

Tactic:
graph,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ map { toFun := fun a ↦ (a, f a), inj' := ⋯ } f.support ↔ f a = m ∧ m ≠ 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
c : α × M
f : α →₀ M
⊢ c ∈ f.graph ↔ f c.1 = c.2 ∧ c.2 ≠ 0

Tactic:
by
  cases c
  exact mk_mem_graph_iff

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst f.graph = f.support

Tactic:
graph,

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst (map { toFun := fun a ↦ (a, f a), inj' := ⋯ } f.support) = f.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∈ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

Tactic:
rcases h with ⟨a, rfl⟩
    rw [mapDomain_apply f.injective, embDomain_apply_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ v₁ a = v₂ a

Tactic:
by_cases h : a ∈ v₁.support ∪ v₂.support
    · rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq] <;>
        · apply Set.union_subset hv₁ hv₂
          exact mod_cast h
    · simp_all

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 : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ (∀ (a : α), f a ∉ l.support) → ∀ (a : β), a ∉ l.support

Tactic:
intro h

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
⊢ ∀ (a : β), a ∉ l.support
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case pos
ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∈ S
⊢ ∏ x ∈ S', f x < ∏ x ∈ S, f x

pp: case neg
ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∉ S
⊢ ∏ x ∈ S', f x < ∏ x ∈ S, f x

Tactic:
· calc ∏ x ∈ S', f x
        ≤ ∏ x ∈ S.erase d, f x := Finset.prod_le_prod_of_subset' (fun x hx ↦
          Finset.mem_erase.mpr ⟨fun h ↦ hd_not (h ▸ hx),
            match Finset.mem_union.mp (hS' hx) with
            | .inl h => Finset.mem_of_mem_erase h
            | .inr h => Finset.mem_singleton.mp h ▸ hd'S⟩)
      _ < (∏ x ∈ S.erase d, f x) * f d :=
          lt_mul_of_one_lt_right' _ (one_le.trans_lt hlt)
      _ = ∏ x ∈ S, f x := Finset.prod_erase_mul S f hd_mem

Goal state after:
case neg
ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∉ S
⊢ ∏ x ∈ S', f x < ∏ x ∈ S, f x
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 ∈ insert i s, f j

Tactic:
prod_insert hs

Goal state after:
ι : 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 < f i * ∏ x ∈ s, f x
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
⊢ ∀ (x : α), 0 ≠ 0 → x ∈ s

Tactic:
intro h

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
h : α
⊢ 0 ≠ 0 → h ∈ s
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
⊢ single a 1 ∈ span R ((fun x ↦ single x 1) '' s) ↔ a ∈ s

Tactic:
by
  refine ⟨fun h => ?_, fun h => Submodule.subset_span <| Set.mem_image_of_mem _ h⟩
  rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
    Finsupp.support_single _ (one_ne_zero' R)] at h
  simpa using h

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ ⋯.toFinset
⊢ x ∈ s

Tactic:
Finite.mem_toFinset

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ 1 < ∏ᶠ (i : ι) (_ : i ∈ univ), f i

Tactic:
apply one_lt_finprod_cond <;> simpa

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

Goal state before:
pp: case neg
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : ¬HasFiniteMulSupport fun x ↦ 0
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1

Tactic:
rw [finprod_of_not_hasFiniteMulSupport H]

Goal state after:
case neg
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : ¬HasFiniteMulSupport fun x ↦ 0
⊢ 1 ≤ ∏ᶠ (x : α), 1
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
k : Fin n
hk : ¬p k
⊢ #{i | p i} ≤ ↑k

Tactic:
← Fin.card_Iio

Goal state after:
n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
k : Fin n
hk : ¬p k
⊢ #{i | p i} ≤ #(Iio k)
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
i : Fin (n + 1)
x : Option (Fin n)
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) x) = x

Tactic:
cases x

Goal state after:
case none
m n : ℕ
i : Fin (n + 1)
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) none) = none

case some
m n : ℕ
i : Fin (n + 1)
val✝ : Fin n
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) (some val✝)) = some val✝
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ 0 < a → Ioi (a - 1) = Ici a

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < a → Ioc (a - 1) b = Icc a b

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < a → Ioo (a - 1) b = Ico a b

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < b → Icc a (b - 1) = Ico a b

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < b → Ioc a (b - 1) = Ioo a b

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a

Tactic:
by
  rw [mul_finsum]
  congr
  ext a
  by_cases h : a ∈ s <;> simp_all

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
⊢ v i ≠ 0

Tactic:
intro h

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ False
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ ⊤ = (x ^ ↑a✝) ^ ⊤

Tactic:
epow_top

Goal state after:
case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ ⊤ = ⊤

case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ 1 < x ^ ↑a✝
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ k • p + (n • p + b) = n • p + (l • p + c)

Tactic:
← hbc,

Goal state after:
case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ k • p + (n • p + b) = n • p + (k • p + b)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ m n, m • f p + f a = n • f p + f b

Tactic:
use m, n

Goal state after:
case h
M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
m n : ℕ
h : m • p + a = n • p + b
⊢ m • f p + f a = n • f p + f b
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∃ m, m • p = b - a) → ∃ m n, m • p + a = n • p + b

Tactic:
· rintro ⟨m, h⟩
    use m.toNat, (-m).toNat
    rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
⊢ a * m + b * n ≠ m * n

Tactic:
intro h

Goal state after:
m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
⊢ False
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case mpr
a b n : ℕ
⊢ a % n = b % n → a ≡ b [PMOD n]

Tactic:
intro h

Goal state after:
case mpr
a b n : ℕ
h : a % n = b % n
⊢ a ≡ b [PMOD n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
w : (Finsupp.linearCombination R v) f = v x
p : ∀ x ∈ Finsupp.supported R R ↑f.support, (Finsupp.linearCombination R v) x ≠ (Finsupp.linearCombination R v) f
⊢ False

Tactic:
exact p f (f.mem_supported_support R) rfl

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
⊢ a - c ≡ b - d [MOD n]

Tactic:
obtain hac | hca := lt_or_ge a c

Goal state after:
case inl
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hac : a < c
⊢ a - c ≡ b - d [MOD n]

case inr
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hca : c ≤ a
⊢ a - c ≡ b - d [MOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
⊢ b * n + a ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
rw [add_comm, add_mul_modulus_modEq_iff]

Goal state after: