mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
⊢ Prod.mk <$> x✝¹ <*> x✝ = (fun b a ↦ (a, b)) <$> x✝ <*> x✝¹

Tactic:
simp! [map, Seq.seq]

Goal state after:
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
⊢ mk ((fun x1 x2 ↦ x1 <*> x2) <$> mk ((fun x ↦ Prod.mk <$> x) <$> x✝¹) <*> x✝) =
    mk ((fun x1 x2 ↦ x1 <*> x2) <$> mk ((fun x ↦ (fun b a ↦ (a, b)) <$> x) <$> x✝) <*> x✝¹)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
⊢ v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'

Tactic:
rw [Ne, eq_cons_iff a v v', not_and_or]

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

Goal state before:
pp: case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
i' : Fin (n + 1)
⊢ (scanl f (f b v.head) v.tail).get i'.succ =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i'.succ.castSucc) ((v.head ::ᵥ v.tail).get i'.succ)

Tactic:
simp only [hn, Fin.castSucc_succ, get_cons_succ]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ↑(filterNe a (fill a m.fst m.snd)).snd = ↑m.snd

Tactic:
by
      rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]
      rw [filter_add, filter_eq_self.2, add_eq_left, eq_zero_iff_forall_notMem]
      · intro b hb
        rw [mem_filter, Sym.mem_coe, mem_replicate] at hb
        exact hb.2 hb.1.2.symm
      · exact fun a ha ha' => h <| ha'.symm ▸ ha

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
⊢ ¬Countable α ↔ Uncountable α

Tactic:
not_countable_iff

Goal state after:
α : Type u
⊢ Uncountable α ↔ Uncountable α
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
⊢ Injective h

Tactic:
refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
⊢ InjOn g' sᶜ

case refine_2
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
⊢ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g' y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case refine_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : x' = y'
⊢ g x' = g y'

Tactic:
rw [hxy]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case inl
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b

Tactic:
exact zero_le

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ sum f

Tactic:
rw [← Quotient.out_eq (f i)]
  exact ⟨⟨fun a => ⟨i, a.down⟩, fun a b h => by simpa using h⟩⟩

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
P : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : Monoid N✝
inst✝³ : Monoid P
M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
φ : M →* N
ψ : N →* N
inst✝ : IsId ψ
⊢ ψ.comp φ = φ

Tactic:
by simp only [IsId.eq_id, MonoidHom.id_comp]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ #((i : PEmpty.{u + 1}) → Quotient.out (f i)) = 1

Tactic:
mk_eq_one

Goal state after:
case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ 1 = 1
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
← mul_and_mul_iff

Goal state after:
R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
h : #α = ℵ₀
⊢ Nonempty (Denumerable α)

Tactic:
obtain ⟨f⟩ := Quotient.exact h
    exact ⟨Denumerable.mk' <| f.trans Equiv.ulift⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ⊢ #(List PEmpty.{u_1 + 1}) = 1

Tactic:
mk_eq_one

Goal state after:
⊢ 1 = 1
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
⊢ f = g

Tactic:
by
  apply DFunLike.ext
  intro m
  exact DFunLike.congr_fun h m

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M
inst✝¹ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst✝ : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
⊢ f ≠ 0

Tactic:
have ⟨y, ne⟩ := exists_ne (0 : M₂)

Goal state after:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M
inst✝¹ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst✝ : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
y : M₂
ne : y ≠ 0
⊢ f ≠ 0
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hy : y ∈ p
⊢ x - y ∈ p ↔ x ∈ p

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hy : y ∈ p
⊢ x + -y ∈ p ↔ x ∈ p
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
⊢ x - y ∈ p ↔ y ∈ p

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
⊢ x + -y ∈ p ↔ y ∈ p
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ↑(⨅ i, p i) = ⋂ i, ↑(p i)

Tactic:
rw [iInf, coe_sInf]; simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ (codRestrict p f hf).ker = f.ker

Tactic:
rw [ker, comap_codRestrict, Submodule.map_bot]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ comap f ⊥ = f.ker
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f : R →+* S
⊢ Subsemiring.map g f.rangeS = (g.comp f).rangeS

Tactic:
simpa only [rangeS_eq_map] using (⊤ : Subsemiring R).map_map g f

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x✝ x : R
hx✝ : x ∈ closure s
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ -x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
| neg x _ hx =>

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
this : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
⊢ (List.map List.prod [t]).sum = x

Tactic:
by
          rw [List.map_singleton, List.sum_singleton, ht2]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀✝ : ?m.1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ ∀ (x y : ↥(Associates M₀)⁰),
    (Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x ∈ M₀⁰) (fun x ↦ x ∈ (Quotient (Associated.setoid M₀))⁰) ⋯
            ⋯).toFun
        (x * y) =
      (Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x ∈ M₀⁰) (fun x ↦ x ∈ (Quotient (Associated.setoid M₀))⁰) ⋯
              ⋯).toFun
          x *
        (Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x ∈ M₀⁰) (fun x ↦ x ∈ (Quotient (Associated.setoid M₀))⁰) ⋯
              ⋯).toFun
          y

Tactic:
simp [Quotient.forall, Associates.mk_mul_mk]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: 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
⊢ ∅ • N = ⊥

Tactic:
ext
  fconstructor
  · intro hx
    rw [mem_set_smul_def, Submodule.mem_sInf] at hx
    exact hx ⊥ (fun r _ hr ↦ hr.elim)
  · rintro rfl; exact Submodule.zero_mem _

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

Goal state before:
pp: case smul
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y : M
_h : y ∈ span R s
hy : y ∈ closure (univ • s)
⊢ r₁ • y ∈ closure (univ • s)

Tactic:
clear _h

Goal state after:
case smul
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y : M
hy : y ∈ closure (univ • s)
⊢ r₁ • y ∈ closure (univ • s)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case pos
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
h : m = 0
⊢ m ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

Tactic:
rw [h]
      simp

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

Goal state before:
pp: case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j ∈ span R (range (update v j (v j + r • v i)))

Tactic:
nth_rw 2 [← add_sub_cancel_right (v j) (r • v i)]
    exact sub_mem (subset_span ⟨j, update_self ..⟩)
      (smul_mem _ _ (subset_span ⟨i, update_of_ne hij ..⟩))

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ span R (range (update v j (v j - r • v i))) = span R (range v)

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ span R (range (update v j (v j + -(r • v i)))) = span R (range v)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.sup g).SupIndep f

Tactic:
by
  rw [sup_eq_biUnion]
  exact hs.biUnion hg

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ sSupIndep s ↔ iSupIndep Subtype.val

Tactic:
by
  simp_rw [iSupIndep, sSupIndep, SetCoe.forall, sSup_eq_iSup]
  refine forall₂_congr fun a ha => ?_
  simp [iSup_subtype, iSup_and]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, s.sup (id ∘ f) ≤ x

Tactic:
rw [← Finset.sup_image]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, (Finset.image f s).sup id ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
⊢ IsCompactElement (s.sup f)

Tactic:
by
  classical
    simp_rw [isCompactElement_iff_le_of_directed_sSup_le] at ⊢ h
    intro d hemp hdir hsup
    rw [← Function.id_comp f]
    rw [← Finset.sup_image]
    apply Finset.sup_le_of_le_directed d hemp hdir
    rintro x hx
    obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
    specialize h p hps
    specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
    simpa only [exists_prop]

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

Goal state before:
pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ¬∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Tactic:
push Not at h
    rcases h with ⟨i, hi, hq⟩
    exact prod_eq_zero hi (by simp [hq])

Goal state after:
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 : M
⊢ (∃ y ∈ s, ∃ z, (z ∈ t ∧ z ∈ p) ∧ y + z = x) → (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p

Tactic:
rintro ⟨y, hy, z, ⟨hz, hz'⟩, hyzx⟩

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 ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p
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
⊢ s ⊆ ↑(span R s)

Tactic:
exact subset_span

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
⊢ -s ⊆ ↑(span R (-s))

Tactic:
exact subset_span

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

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

Tactic:
simpa using hx

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
hp : ∃! x, x ∈ s ∧ p x
a : α
⊢ a ∈ s ∧ p a ↔ some (choose p s hp) = some a

Tactic:
simp only [Option.some.injEq, choose_eq_iff]

Goal state after:
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
N : Submodule R M
x : M
hx : x ∈ N
y : ↥N
⊢ y ∈ (R ∙ x).submoduleOf N ↔ y ∈ R ∙ ⟨x, hx⟩

Tactic:
submoduleOf,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
x : M
hx : x ∈ N
y : ↥N
⊢ y ∈ comap N.subtype (R ∙ x) ↔ y ∈ R ∙ ⟨x, hx⟩
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
⊢ (embDomain f (single a m)) b = (single (f a) m) b

Tactic:
by_cases h : b ∈ Set.range f <;> grind

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

Goal state before:
pp: ι : Type u_1
G : Type u_6
inst✝¹ : AddGroup G
inst✝ : DecidableEq ι
f g : ι →₀ G
⊢ (f - g).support ⊆ f.support ∪ g.support

Tactic:
sub_eq_add_neg,

Goal state after:
ι : Type u_1
G : Type u_6
inst✝¹ : AddGroup G
inst✝ : DecidableEq ι
f g : ι →₀ G
⊢ (f + -g).support ⊆ f.support ∪ g.support
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f) none = y

Tactic:
by
  classical
  simp [optionElim]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
x : α
⊢ (optionElim y f) (Option.some x) = f x

Tactic:
by
  classical
  simp [optionElim]

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

Goal state before:
pp: α : Type u_1
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
h1 : ¬(d a = 0 ∧ ((erase a d).sum fun x n ↦ n) = 1) → d a = 1 ∧ ((erase a d).sum fun x n ↦ n) = 0
ha : d a ≠ 0 a
⊢ d a = 1 ∧ ∀ (i : α), i ≠ a → d i = 0

Tactic:
simp_all +contextual [sum, support_erase, sum_eq_zero_iff, mem_erase, erase_ne]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : One R
inst✝ : AddGroup R
f : ι → R
⊢ mulSupport (1 - f) = support f

Tactic:
sub_eq_add_neg,

Goal state after:
ι : Type u_1
R : Type u_5
inst✝¹ : One R
inst✝ : AddGroup R
f : ι → R
⊢ mulSupport (1 + -f) = support f
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
obtain ⟨y, hy⟩ := h.exists_abv_gt_one

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : 1 < v y
⊢ ∃ x, x ≠ 0 ∧ v x < 1
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
hf : 0 ∈ f.support
⊢ False

Tactic:
exact nhf hf

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

Goal state before:
pp: case ha
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
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)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ 0 ≤ f a

pp: case hbc
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
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)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f s.prod ≤ (map f s).prod

Tactic:
exacts [h0 _, hs hps]

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

Goal state before:

Tactic:
∏ x ∈ S', f x
        ≤ ∏ x ∈ S.erase d ∪ {d'}, f x := Finset.prod_le_prod_of_subset' hS'
      _ = (∏ x ∈ S.erase d, f x) * f d' := by
          rw [Finset.prod_union (Finset.disjoint_singleton_right.mpr
            (fun h ↦ hd'S (Finset.mem_of_mem_erase h))), Finset.prod_singleton]
      _ < (∏ x ∈ S.erase d, f x) * f d := mul_lt_mul_right hlt _
      _ = ∏ x ∈ S, f x := Finset.prod_erase_mul S f hd_mem

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
⊢ l x = 0 x

Tactic:
by_cases xs : x ∈ s

Goal state after:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
⊢ l x = 0 x

case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
xs : x ∉ s
⊢ l x = 0 x