mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ sSupIndep {a, b} ↔ Disjoint a b

Tactic:
by
  constructor
  · intro h
    exact h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab
  · rintro h c ((rfl : c = a) | (rfl : c = b))
    · convert! h using 1
      simp [hab, sSup_singleton]
    · convert! h.symm using 1
      simp [hab, sSup_singleton]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
⊢ Disjoint x (sSup y)

Tactic:
have := (hs.mono <| insert_subset_iff.mpr ⟨hx, hy⟩) (mem_insert x _)

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup (insert x y \ {x}))
⊢ Disjoint x (sSup y)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
have dir_US : DirectedOn (· ≤ ·) S := by
        rintro x ⟨c, hc⟩ y ⟨d, hd⟩
        use x ⊔ y
        constructor
        · use c ∪ d
          constructor
          · simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
          · simp only [hc.right, hd.right, Finset.sup_union]
        simp only [and_self_iff, le_sup_left, le_sup_right]

Goal state after:
case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
hst : Disjoint (↑s) t
⊢ Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
classical
  induction s using Finset.induction_on generalizing t with
  | empty => simp
  | insert j s₀ hj ih =>
    have hjt : j ∉ t := by aesop
    replace hst : Disjoint ↑s₀ (insert j t) := by aesop
    replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
    have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
    rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]
    exact disjoint_sup_right_of_disjoint_sup_right ih this

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ sSup s ∈ s

Tactic:
ht₂

Goal state after:
case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ ⊥ ∈ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s

Tactic:
ht₂

Goal state after:
case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ t.sup id ∈ s
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 : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
⊢ Disjoint (f i) (t.sup id)

Tactic:
have : (Finset.erase (insert i (t.preimage _ hf)) i).image f = t := by
    ext a
    simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq,
      Finset.erase_insert_eq_erase, Finset.mem_image, t]
    refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
    obtain ⟨j, hj, rfl⟩ := hs has
    exact ⟨j, ⟨hj, ha, has⟩, rfl⟩

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (t.sup id)
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))

Tactic:
rintro x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩

Goal state after:
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 : M
i : ι
hix : x ∈ p i
⊢ r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: M : Type u_3
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
l : List M
⊢ (map Neg.neg l).prod = (-1) ^ l.length * l.prod

Tactic:
by
  induction l <;> simp [*, pow_succ, ((Commute.neg_one_left _).pow_left _).left_comm]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
⊢ ∀ z ∈ S, z ≤ sSup S

Tactic:
intro

Goal state after:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
z✝ : α
⊢ z✝ ∈ S → z✝ ≤ 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
h : f.ker ≤ p
⊢ comap f (map f p) = p

Tactic:
rw [Submodule.comap_map_eq, sup_of_le_left h]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
by_cases ht : x ∈ t

Goal state after:
case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
ht : x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
ht : ¬x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
by_cases ht : x ∈ t

Goal state after:
case pos
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
ht : x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

case neg
α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
ht : ¬x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case h
α : 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 : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ ¬a = x

Tactic:
exact Ne.symm xa

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
h : Subsingleton M
⊢ Subsingleton (α →₀ M)

Tactic:
infer_instance

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

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

Tactic:
by
  refine subset_trans Finsupp.support_add <| union_subset_iff.mpr ⟨?_, ?_⟩ <;>
  exact subset_trans Finsupp.support_single_subset (by simp)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f g : ι →₀ M
h : Disjoint f.support g.support
⊢ AddCommute f g

Tactic:
by
  classical simp_all [addCommute_iff_inter, Finset.disjoint_iff_inter_eq_empty]

Goal state after:
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
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

Tactic:
· rw [mulIndicator_of_notMem hx]
    simp only [mem_iUnion, not_exists] at hx
    simp [hx, ← h1]

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

Goal state before:
pp: case hf
α : 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
i : ι
⊢ 1 ≤ f i

Tactic:
intro

Goal state after:
case hf
α : 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
i : ι
i✝ : α
⊢ 1 i✝ ≤ f i i✝
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s : Set ι
i : ι
inst✝ : Nontrivial M₀
⊢ s.indicator 1 i = 1 ↔ i ∈ s

Tactic:
classical simp [indicator_apply, imp_false]

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

Goal state before:
pp: case refine_1
α : 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✝ : α ≃ β
f : α →₀ M
x : α
⊢ (equivMapDomain f✝.symm (equivMapDomain f✝ f)) x = f x

Tactic:
simp only [equivMapDomain_apply, Equiv.symm_symm, Equiv.symm_apply_apply,
      Equiv.apply_symm_apply]

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

Goal state before:
pp: case refine_2
α : 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✝ : α ≃ β
f : β →₀ M
x : β
⊢ (equivMapDomain f✝ (equivMapDomain f✝.symm f)) x = f x

Tactic:
simp only [equivMapDomain_apply, Equiv.symm_symm, Equiv.symm_apply_apply,
      Equiv.apply_symm_apply]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β), single (g a) 0 = 0

Tactic:
intro

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ single (g a✝) 0 = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = single (g a) b₁ + single (g a) b₂

Tactic:
intro

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ ∀ (b₁ b₂ : M), single (g a✝) (b₁ + b₂) = single (g a✝) b₁ + single (g a✝) b₂
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a

Tactic:
rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (x a + ∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 0) = x a
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
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
by_cases hs0 : s = ∅

Goal state after:
case pos
α : 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 = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

case neg
α : 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 = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
a : Subtype P
m : M
⊢ (single a m).extendDomain = single (↑a) m

Tactic:
by
  ext a'
  obtain rfl | ha := eq_or_ne a' a.val <;>
    simp [*, a.prop, single, Pi.single, Function.update, Subtype.ext_iff]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : CommMonoid N
inst✝¹ : MulDistribMulAction M N
ι : Sort u_4
inst✝ : Finite ι
f : ι → N
r : M
⊢ r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x

Tactic:
cases nonempty_fintype (PLift ι)

Goal state after:
case intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : CommMonoid N
inst✝¹ : MulDistribMulAction M N
ι : Sort u_4
inst✝ : Finite ι
f : ι → N
r : M
val✝ : Fintype (PLift ι)
⊢ r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : MulOneClass N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
l : List N
m : M
⊢ m ^ l.length • l.prod = (map (fun x ↦ m • x) l).prod

Tactic:
induction l with
  | nil => simp
  | cons head tail ih => simp [← ih, smul_mul_smul_comm, pow_succ']

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

Goal state before:
pp: α : Type u_1
M : Type u_5
R : Type u_11
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ ¬b • g a = 0 → ¬g a = 0

Tactic:
exact mt fun h => h.symm ▸ smul_zero _

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

Goal state before:
pp: ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
f : ι → R
x : M
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x

Tactic:
by
  rcases eq_or_ne x 0 with (rfl | hx)
  · simp
  · exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ val '' Iio i = Iio ↑i

Tactic:
rw [← preimage_val_Iio_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact Iio_subset_Iio i.is_lt.le

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m '' Ici i = Ici (natAdd m i)

Tactic:
← preimage_natAdd_Ici_natAdd,

Goal state after:
n m : ℕ
i : Fin n
⊢ natAdd m '' natAdd ?m ⁻¹' Ici (natAdd ?m i) = Ici (natAdd m i)

case m
n m : ℕ
i : Fin n
⊢ ℕ
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case add
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
f₁ f₂ : β →₀ R
h₁ : ((f₁.sum fun i a ↦ a • B i).sum fun i a ↦ a • A i) = f₁.sum fun i a ↦ a • (B i).sum fun i a ↦ a • A i
h₂ : ((f₂.sum fun i a ↦ a • B i).sum fun i a ↦ a • A i) = f₂.sum fun i a ↦ a • (B i).sum fun i a ↦ a • A i
⊢ (((f₁ + f₂).sum fun i a ↦ a • B i).sum fun i a ↦ a • A i) = (f₁ + f₂).sum fun i a ↦ a • (B i).sum fun i a ↦ a • A i

Tactic:
simp [sum_add_index, h₁, h₂, add_smul]

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∃ c, ∑ i ∈ s, c i • v i = x

Tactic:
refine ⟨fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0, ?_⟩
    rw [← hc, ← Finset.sum_coe_sort (s := s)]
    simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
x : M
⊢ x ∈ span R ↑s → ∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x

Tactic:
rw [mem_span_iff_exists_finset_subset]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
x : M
⊢ (∃ f t, ↑t ⊆ ↑s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x) →
    ∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
x✝ : j ∈ Finset.univ
⊢ (b.repr (b' j)) i * (b'.repr x) j = (b'.repr x) j * (b.repr (b' j)) i

Tactic:
mul_comm

Goal state after:
ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
x✝ : j ∈ Finset.univ
⊢ (b'.repr x) j * (b.repr (b' j)) i = (b'.repr x) j * (b.repr (b' j)) i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ (∃ n f g, ∑ i, f i • ↑(g i) = m) → m ∈ span R s

Tactic:
· rintro ⟨n, f, g, rfl⟩
    exact Submodule.sum_mem _ (fun i _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span (g i).2))

Goal state after:
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
⊢ ↑j < #{i | p i} ↔ p j

Tactic:
have h1 (k : Fin n) (hk : ¬ p k) : #{i | p i} ≤ k := by
    rw [← Fin.card_Iio]
    exact card_le_card (by grind)
  refine ⟨by grind, fun h ↦ ?_⟩
  by_contra! hc
  let q : Fin n → Prop := (· < #{i | p i})
  have : univ.filter q = univ.filter p :=
    eq_of_subset_of_card_le (by grind) (by rw [card_filter_val_lt]; grind)
  have : j ∈ univ.filter p := by grind
  grind

Goal state after:
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
⊢ ↑j < #{i | p i} ↔ p j

Tactic:
by
  have h1 (k : Fin n) (hk : ¬ p k) : #{i | p i} ≤ k := by
    rw [← Fin.card_Iio]
    exact card_le_card (by grind)
  refine ⟨by grind, fun h ↦ ?_⟩
  by_contra! hc
  let q : Fin n → Prop := (· < #{i | p i})
  have : univ.filter q = univ.filter p :=
    eq_of_subset_of_card_le (by grind) (by rw [card_filter_val_lt]; grind)
  have : j ∈ univ.filter p := by grind
  grind

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = vecAlt1 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
rw [vecAlt1_vecAppend]

Goal state after:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = (vecCons x u ∘ fun n_1 ↦ n_1 + n_1 + 1) i
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
by
  cases n
  · simp [fin_one_eq_zero k]
  simp only [le_def]
  rw [← lt_sub_one_iff, le_iff_lt_or_eq, val_fin_lt, val_inj, lt_sub_one_iff, or_iff_left_iff_imp,
    eq_comm, sub_eq_iff_eq_add]
  simp

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
rcases lt_trichotomy y 1 with y_0 | rfl | y_2
      · simp only [Order.lt_one_iff.1 y_0, mul_zero, zero_epow_top]
      · simp
      · rw [epow_top x_2, epow_top y_2, mul_top top_ne_zero]
        exact epow_top (one_lt_mul x_2.le y_2)

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 8 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Tactic:
rw [prod_univ_castSucc, prod_univ_seven]
  rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : Fin n → M
⊢ ∏ j, ⟨i + 1, h⟩.insertNth x (cons hd tl) j = x * ∏ j, cons hd tl j

Tactic:
have i_lt := Nat.lt_of_succ_lt_succ h

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : Fin n → M
i_lt : i < n + 1
⊢ ∏ j, ⟨i + 1, h⟩.insertNth x (cons hd tl) j = x * ∏ j, cons hd tl j
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ Injective fun x ↦ ⟨x.1, ⋯⟩

Tactic:
intro

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
a₁✝ : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)
⊢ ∀ ⦃a₂ : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)⦄, (fun x ↦ ⟨x.1, ⋯⟩) a₁✝ = (fun x ↦ ⟨x.1, ⋯⟩) a₂ → a₁✝ = a₂
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m / ↑d ∣ (↑b - ↑a) * ↑c / ↑(m.gcd c)

Tactic:
mul_comm

Goal state after:
case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m / ↑d ∣ ↑c * (↑b - ↑a) / ↑(m.gcd c)