mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa [U] using @this x

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s

Tactic:
ext x
  refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
  rintro - ⟨H, rfl⟩
  rintro - ⟨J, rfl⟩
  refine (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_
  refine (Submonoid.mem_closure.mp hy) H.toSubmonoid fun z hz => ?_
  exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubring R := NonUnitalSubring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa [U] using @this x

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝² : A →ₐ[R] A
x✝¹ x✝ : Aˣ
⊢ ↑(x✝² • (x✝¹ * x✝)) = ↑(x✝² • x✝¹ * x✝² • x✝)

Tactic:
exact map_mul _ _ _

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa [U] using @this x

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa [U] using @this x

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (hd.prod + (List.map List.prod tl).sum)

Tactic:
exact ha this (ih HL.2)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
⊢ b * a ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
mul_comm c

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case left
M : Type u_1
inst✝ : CommMonoidWithZero M
b : Associates M
hlt : 0 < b
⊢ False

Tactic:
apply not_lt_of_ge _ hlt

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
b : Associates M
hlt : 0 < b
⊢ b ≤ 0
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inl
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
· obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

Goal state after:
case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inl
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
· obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

Goal state after:
case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ comap q.subtype p.subtype.range = comap q.subtype p

Tactic:
range_subtype

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ comap q.subtype p = comap q.subtype p
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ b → a ⋖ a ⊔ b

Tactic:
by
  rw [sup_comm, inf_comm]
  exact covBy_sup_of_inf_covBy_left

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

Goal state before:
pp: M : Type u_9
inst✝ : AddCommGroup M
s : AddSubgroup M
⊢ (span ℤ ↑s).toAddSubgroup = s

Tactic:
rw [span_int_eq_addSubgroupClosure, s.closure_eq]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a b : α
ha : IsCoatom a
hab : a ≤ b
⊢ b = ⊤ → b ≠ a

Tactic:
by rintro rfl; exact ha.ne_top.symm

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
⊢ (fun A ↦ {a | ↑a ≤ A}) ((fun S ↦ sSup (Subtype.val '' S)) S) = S

Tactic:
by
    have h : ∀ a ∈ Subtype.val '' S, IsAtom a := by
      rintro a ⟨a', ha', rfl⟩
      exact a'.prop
    rw [← Subtype.val_injective.image_injective.eq_iff, eq_setOfPred_le_sSup_and_isAtom h]
    ext a
    simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≠ ⊤

Tactic:
obtain ⟨a, b, h⟩ := exists_pair_ne α
  rcases eq_bot_or_eq_top a with (rfl | rfl) <;> rcases eq_bot_or_eq_top b with (rfl | rfl) <;>
    first | simpa | simpa using h.symm

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, ∃ z ∈ span R s, x = a • y + z) → ∃ a, x + a • y ∈ span R s

Tactic:
rintro ⟨a, z, hz, rfl⟩
    exact ⟨-a, by simp [hz, add_assoc]⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (⋯.IicOrderIsoIci ⟨a, ay⟩) ⟨b, xb⟩
⊢ IsCoatom ⟨b, xb⟩

Tactic:
← hb.isAtom_iff_isCoatom,

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (⋯.IicOrderIsoIci ⟨a, ay⟩) ⟨b, xb⟩
⊢ IsAtom (⋯.IicOrderIsoIci ⟨a, ay⟩)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)

Tactic:
fin_cases i <;> simpa

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

Goal state before:
pp: case mpr
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ t.sup Subtype.val
⊢ ∀ b ∈ t, ↑b ≤ (Finset.image Subtype.val t).sup id

Tactic:
exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)

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

Goal state after:
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
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
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i

Tactic:
iSup,

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ a ⊓ sSup (range fun i ↦ f i) = ⨆ i, a ⊓ f i
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:
iSup,

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ sSup (range fun i ↦ f i) ⊓ a = ⨆ i, f i ⊓ a
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i x₁ : ι
hx₁ : ¬f x₁ = ⊥
x₂ : ι
hx₂ : ¬f x₂ = ⊥
hfeq : f x₁ = f x₂
hneq : ¬x₁ = x₂
⊢ False

Tactic:
specialize h ({x₁, x₂} : Finset ι)

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i x₁ : ι
hx₁ : ¬f x₁ = ⊥
x₂ : ι
h : {x₁, x₂}.SupIndep f
hx₂ : ¬f x₂ = ⊥
hfeq : f x₁ = f x₂
hneq : ¬x₁ = x₂
⊢ False
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
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:
· rw [smul_zero]
      exact AddSubmonoid.zero_mem _

Goal state after:
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.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ map Prod.fst (antidiagonal ⟦l⟧) = powerset ⟦l⟧

Tactic:
by simp [powersetAux']

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ map Prod.snd (antidiagonal ⟦l⟧) = powerset ⟦l⟧

Tactic:
by simp [powersetAux']

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s✝ : Multiset ι
f g : ι → R
a : ι
s : Multiset ι
ih : (map (fun i ↦ f i + g i) s).prod = (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
⊢ (map (fun i ↦ (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal).sum +
      (map (fun i ↦ (map f i.1).prod * (g a * (map g i.2).prod)) s.antidiagonal).sum =
    (map (fun x ↦ (map f x.1).prod * (g a * (map g x.2).prod)) s.antidiagonal).sum +
      (map (fun i ↦ (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal).sum

Tactic:
exact add_comm _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ (f ∘ ⇑g) a ≠ 0 → a ∈ g.support

Tactic:
rw [mem_support_iff, not_imp_not]; exact fun H => (congr_arg f H).trans hf

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j

Tactic:
by
  refine Finset.induction_on_max s (by simp) ?_
  clear s
  intro a s ha ihs
  have ha' : a ∉ s := fun ha' => lt_irrefl a (ha a ha')
  rw [prod_insert ha', prod_insert ha', sum_insert ha', filter_insert, if_neg (lt_irrefl a),
    filter_true_of_mem ha, ihs, add_mul, mul_add, mul_add, add_assoc]
  congr 1
  rw [add_comm]
  congr 1
  · rw [filter_false_of_mem, prod_empty, mul_one]
    exact (forall_mem_insert _ _ _).2 ⟨lt_irrefl a, fun i hi => (ha i hi).not_gt⟩
  · rw [mul_sum]
    refine sum_congr rfl fun i hi => ?_
    rw [filter_insert, if_neg (ha i hi).not_gt, filter_insert, if_pos (ha i hi), prod_insert,
      mul_left_comm]
    exact mt (fun ha => (mem_filter.1 ha).1) ha'

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
i : ι
inst✝ : Subsingleton ι
m : M
j : ι
⊢ ((uniqueAddEquiv i).symm m) j = m

Tactic:
by simp [Subsingleton.elim j i]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
⊢ ∀ (s : Finset ι) (f : ι →₀ M), f.support = s → motive f

Tactic:
refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)

Goal state after:
case refine_1
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s : Finset ι
f : ι →₀ M
h : f.support = ∅
⊢ motive f

case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ motive f
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 : α
hx : ∃ x_1, x ∉ s x_1
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Tactic:
rcases hx with ⟨j, hj⟩

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
⊢ 1 = ⨅ i, (s i).mulIndicator f x
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: α : 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
⊢ (∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
hpsa

Goal state after:
α : 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
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
⊢ {x ∈ ∅ | p x} = ∅

Tactic:
Finset.filter_empty

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
⊢ ∅ = ∅
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ 0 < #({a_1 ∈ s | g a_1 = a})

Tactic:
card_pos

Goal state after:
ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ {a_1 ∈ s | g a_1 = a}.Nonempty
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α × β →₀ M
⊢ ∀ (a : α),
    a ∈ image Prod.fst f.support ↔
      { support := filterMap (fun x ↦ if x.1 = a then some x.2 else none) f.support ⋯, toFun := fun b ↦ f (a, b),
          mem_support_toFun := ⋯ } ≠
        0

Tactic:
simp [DFunLike.ext_iff]

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✝¹ : LinearOrder M
f g : ι → M
s : Finset ι
inst✝ : MulLeftMono M
Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i
⊢ ∃ i ∈ s, f i < g i

Tactic:
contrapose! Hlt with Hle
  exact prod_le_prod' Hle

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : 1 ≤ f
⊢ 1 < ∏ i, f i ↔ 1 < f

Tactic:
obtain rfl | hf := hf.eq_or_lt

Goal state after:
case inl
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
hf : 1 ≤ 1
⊢ 1 < ∏ i, 1 i ↔ 1 < 1

case inr
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf✝ : 1 ≤ f
hf : 1 < f
⊢ 1 < ∏ i, f i ↔ 1 < f
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : f ≤ 1
⊢ ∏ i, f i < 1 ↔ f < 1

Tactic:
obtain rfl | hf := hf.eq_or_lt

Goal state after:
case inl
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
hf : 1 ≤ 1
⊢ ∏ i, 1 i < 1 ↔ 1 < 1

case inr
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf✝ : f ≤ 1
hf : f < 1
⊢ ∏ i, f i < 1 ↔ f < 1
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ ∑ x ∈ m.toFinset, (count x m - 1) ≤ 1 ↔ ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
Finset.sum_le_one_iff

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ (∀ (x y : α), x ∈ m.toFinset → y ∈ m.toFinset → count x m - 1 ≠ 0 → count y m - 1 ≠ 0 → x = y ∧ count x m - 1 = 1) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
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
s : δ → Set α
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)

Tactic:
have := Classical.decPred fun x => x ∈ ⋃ i, s i

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
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
s : δ → Set α
this✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
this : (supported M R (⋃ i, s i)).subtype.range ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)

Tactic:
range_subtype

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
this : supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
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 α'
l : α →₀ M
hl : f '' ↑l.support ⊆ s
⊢ ↑(mapDomain f l).support ⊆ s

Tactic:
← Finset.coe_image

Goal state after:
α : 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 α'
l : α →₀ M
hl : ↑(Finset.image f l.support) ⊆ s
⊢ ↑(mapDomain f l).support ⊆ s
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∈ s
⊢ z c • v c ∈ span R (v '' s)

pp: case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∉ s
⊢ z c • v c ∈ span R (v '' s)

Tactic:
· exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))

Goal state after:
case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∉ s
⊢ z c • v c ∈ span R (v '' s)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
v : α → M
s : Set α
⊢ span R (v '' s) ≤ map (linearCombination R v) (supported R R s).subtype.range

Tactic:
range_subtype

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ span R (v '' s) ≤ map (linearCombination R v) (supported R R s)