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

Goal state before:
pp: case zero
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
⊢ p a 0 ha ⋯

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ 0 ∈ closure (univ • s)

Tactic:
| zero =>

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

Goal state before:
pp: case smul.zero
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
⊢ r₁ • 0 ∈ closure (univ • s)

Tactic:
| zero =>

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 t : Set M
hst : Disjoint (span R s) (span R t)
⊢ Disjoint (s \ {0}) t

Tactic:
disjoint_iff_forall_ne

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set M
hst : Disjoint (span R s) (span R t)
⊢ ∀ ⦃a : M⦄, a ∈ s \ {0} → ∀ ⦃b : M⦄, b ∈ t → a ≠ b
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s : Set α
t : Set β
⊢ latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t

Tactic:
by
  simp_rw [← supClosure_infClosure]; simp

Goal state after:
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.biUnion g).SupIndep f

Tactic:
intro a

Goal state after:
α : 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
a : Finset ι
⊢ a ⊆ s.biUnion g → ∀ ⦃i : ι⦄, i ∈ s.biUnion g → i ∉ a → Disjoint (f i) (a.sup f)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case mem
R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute y x
y x✝ : A
h✝ : x✝ ∈ s
⊢ Commute x✝ x

Tactic:
| mem _ _ =>

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

Goal state before:
pp: case zero
R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute y x
y : A
⊢ Commute 0 x

Tactic:
| zero =>

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

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
⊢ ∃ t, k ≤ t.sup s

Tactic:
obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs

Goal state after:
case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ range s
ht' : k ≤ t.sup id
⊢ ∃ t, k ≤ t.sup s
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
⊢ Disjoint (f j) (⨆ x ∈ t ∪ ↑s₀, f x)

Tactic:
exact disjoint_biSup hf <| by aesop

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
⊢ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
intro a

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : ℕ →o α
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x = ⊥

Tactic:
← hs,

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x = x ⊓ sSup s
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ ∀ (x y_1 : S),
    x ∈ span R s → y_1 ∈ span R s → x • y ∈ span R (s • t) → y_1 • y ∈ span R (s • t) → (x + y_1) • y ∈ span R (s • t)

Tactic:
intro _ _ _ _

Goal state after:
case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝¹ : A
hp : x✝¹ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
x✝ y✝ : S
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
⊢ x✝ • y ∈ span R (s • t) → y✝ • y ∈ span R (s • t) → (x✝ + y✝) • y ∈ span R (s • t)
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
inst✝³ : FunLike F α α
inst✝² : Monoid F
inst✝¹ : IsOneApplyEqSelf F α
inst✝ : IsMulApplyEqComp F α
f : F
x : α
⊢ (f ^ 0) x = (⇑f)^[0] x

Tactic:
| zero =>

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

Goal state before:
pp: case mpr.zero
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
⊢ f ⟨0, ⋯⟩ = g ⟨0, ⋯⟩

Tactic:
| zero =>

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
S : Finset M
⊢ IsCompactElement (⨆ x ∈ ↑S, R ∙ x)

Tactic:
simp only [Finset.mem_coe]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ IsCompactElement (⨆ x ∈ S, R ∙ 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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
N : Submodule R M
f : ↥N →ₛₗ[σ₁₂] M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
⊢ ⨆ a ∈ s, comap N.subtype a = ⊤

Tactic:
← hs,

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₂
N : Submodule R M
f : ↥N →ₛₗ[σ₁₂] M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
⊢ ⨆ a ∈ s, comap (⨆ a ∈ s, a).subtype a = ⊤
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
⊢ ∀ b_1 ∈ {a | a ≤ c ∧ IsAtom a}, b_1 ≤ b ⊔ sSup s

Tactic:
intro a

Goal state after:
case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
⊢ a ∈ {a | a ≤ c ∧ IsAtom a} → a ≤ b ⊔ sSup 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₂
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ q = ⊤

Tactic:
by
    rw [← comap_map_sup_of_comap_le lt.le, hp.2 (map f q ⊔ p), comap_top]
    simpa only [right_lt_sup, map_le_iff_le_comap] using lt.not_ge

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 ι
f g : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ 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 →
        ∏ i ∈ insert a s, (f i + g i) =
          ∏ i ∈ insert a s, f i +
            ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j

Tactic:
intro a

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
⊢ ∀ (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ 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 →
        ∏ i ∈ insert a s, (f i + g i) =
          ∏ i ∈ insert a s, f i +
            ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
⊢ Injective (mapRange e he₀)

Tactic:
intro a

Goal state after:
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a : α →₀ M
⊢ ∀ ⦃a₂ : α →₀ M⦄, mapRange e he₀ a = mapRange e he₀ a₂ → a = a₂
Module: Mathlib.Data.Finsupp.Ext

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
⊢ f = g

Tactic:
by
  refine AddMonoidHom.eq_of_eqOn_denseM add_closure_setOfPred_eq_single ?_
  rintro _ ⟨x, y, rfl⟩
  apply H

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
⊢ Injective fun f ↦ indicator s f

Tactic:
intro a

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a : (i : ι) → i ∈ s → α
⊢ ∀ ⦃a₂ : (i : ι) → i ∈ s → α⦄, (fun f ↦ indicator s f) a = (fun f ↦ indicator s f) a₂ → a = a₂
Module: Mathlib.Algebra.Order.Group.Indicator

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

Tactic:
intro a

Goal state after:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ s.indicator f a ≤ {a | 0 ≤ f a}.indicator f a
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case zero
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
⊢ prod 0 b = b none (0 none) * (some 0).prod fun a ↦ b (Option.some a)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.sup fun x ↦ (f x).support

Tactic:
induction s using Finset.cons_induction_on with
  | empty => rfl
  | cons _ _ _ ih =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr.zero
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
h✝ : Nontrivial R
⊢ abv ↑0 ≤ ↑0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
⊢ prod 0 ≤ prod 0

Tactic:
| zero =>

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

Tactic:
intro a

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 α),
    ((∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod) →
      (∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ f a ≤ (map f (a ::ₘ s')).prod

Tactic:
rw [map_cons, prod_cons]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ f a ≤ f a * (map f s').prod
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 : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' ↑l.support)
⊢ ∀ (a : α), a ∈ l.support.preimage f hf ↔ l (f a) ≠ 0

Tactic:
intro a

Goal state after:
α : 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 : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' ↑l.support)
a : α
⊢ a ∈ l.support.preimage f hf ↔ l (f a) ≠ 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)) →
        (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)

Tactic:
intro a

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
a : ι
⊢ ∀ (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)) →
        (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hf : Injective f
⊢ Surjective fun l ↦ comapDomain f l ⋯

Tactic:
by
  intro l'
  use l'.embDomain ⟨f, hf⟩
  exact Finsupp.comapDomain_embDomain ..

Goal state after:
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✝ : AddCommMonoid M
e : α ≃ β
v : β →₀ M
⊢ equivMapDomain (e.symm.trans e) v = v

Tactic:
Equiv.symm_trans_self

Goal state after:
α : 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✝ : AddCommMonoid M
e : α ≃ β
v : β →₀ M
⊢ equivMapDomain (Equiv.refl β) v = v
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ≤ g i
⊢ ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i

Tactic:
classical
    revert h
    refine Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h),
      fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_
    specialize ih fun i ↦ H i ∘ Finset.mem_insert_of_mem
    rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]
    exact
      mul_eq_mul_iff_eq_and_eq (H a (s.mem_insert_self a))
        (Finset.prod_le_prod' fun i ↦ H i ∘ Finset.mem_insert_of_mem)

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

Goal state before:
pp: case zero
α : 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
⊢ 0 ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))

Tactic:
| zero =>

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
s : δ → Set α
⊢ supported M R (⋃ i, s i) = ⨆ i, supported M R (s i)

Tactic:
by
  refine le_antisymm ?_ (iSup_le fun i => supported_mono <| Set.subset_iUnion _ _)
  have := Classical.decPred fun x => x ∈ ⋃ i, s i
  suffices
    LinearMap.range ((Submodule.subtype _).comp (restrictDom M R (⋃ i, s i))) ≤
      ⨆ i, supported M R (s i) by
    rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
  rw [range_le_iff_comap, eq_top_iff]
  rintro l ⟨⟩
  induction l using Finsupp.induction with
  | zero => exact zero_mem _
  | single_add x a l _ _ ih =>
    refine add_mem ?_ ih
    by_cases h : ∃ i, x ∈ s i
    · simp only [mem_comap, coe_comp, coe_subtype, Function.comp_apply, restrictDom_apply,
        mem_iUnion, h, filter_single_of_pos]
      obtain ⟨i, hi⟩ := h
      exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)
    · simp [h]

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

Goal state before:
pp: case neg
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ 1 = if h : HasFiniteMulSupport ((fun i ↦ f (g i)) ∘ PLift.down) then ∏ i ∈ Finite.toFinset h, f (g i.down) else 1

pp: case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport ((fun i ↦ g i) ∘ PLift.down)

Tactic:
dif_neg

Goal state after:
case neg
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ 1 = 1

case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport ((fun i ↦ f (g i)) ∘ PLift.down)

case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport ((fun i ↦ g i) ∘ PLift.down)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case pos.h₀
α : 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
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ ∀ (b : α), l b ≠ 0 → b ≠ x → (single (f b) (l b)) (f x) = 0

Tactic:
intro y hy xy

Goal state after:
case pos.h₀
α : 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
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
y : α
hy : l y ≠ 0
xy : y ≠ x
⊢ (single (f y) (l y)) (f x) = 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ (if h : HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down) then ∏ i ∈ Finite.toFinset h, f i.down else 1) = 1

Tactic:
dif_neg

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ 1 = 1

case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ¬HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : HasFiniteMulSupport f
⊢ ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ (Finite.toFinset hf).erase a, f i

Tactic:
apply finprod_cond_eq_prod_of_cond_iff

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : HasFiniteMulSupport f
⊢ ∀ {x : α}, f x ≠ 1 → (x ≠ a ↔ x ∈ (Finite.toFinset hf).erase a)
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 : Option α → M
f : Option α →₀ R
⊢ (f.sum fun i a ↦ a • v i) = f none • v none + (linearCombination R (v ∘ Option.some)) f.some

Tactic:
sum_option_index_smul,

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 : Option α → M
f : Option α →₀ R
⊢ (f none • v none + f.some.sum fun a r ↦ r • v (Option.some a)) =
    f none • v none + (linearCombination R (v ∘ Option.some)) f.some
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case zero
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
⊢ ((sum 0 fun i a ↦ a • B i).sum fun i a ↦ a • A i) = sum 0 fun i a ↦ a • (B i).sum fun i a ↦ a • A i

Tactic:
| zero =>

Goal state after: