mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case mp.smul₀
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
inst✝ : SMulCommClass R S M
r : S
x : M
r✝ : S
n✝ : M
mem₁✝ : r✝ ∈ {r}
mem₂✝ : n✝ ∈ N
⊢ ∃ m ∈ N, r✝ • n✝ = r • m

Tactic:
| smul₀ =>

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
x : α
⊢ x ∈ {x | c.IsClosed x} ↔ x ∈ range ⇑c

Tactic:
exact ⟨fun hx ↦ ⟨x, hx.closure_eq⟩, by rintro ⟨y, rfl⟩; exact c.isClosed_closure _⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
ht : t ⊆ image g s
i : ι
⊢ i ∈ image g s → i ∉ t → Disjoint (f i) (t.sup f)

Tactic:
hi

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
ht : t ⊆ image g s
i : ι
hi : i ∈ image g s
⊢ i ∉ t → Disjoint (f i) (t.sup f)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (map g s).SupIndep f

Tactic:
rw [map_eq_image]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (image (⇑g) s).SupIndep f
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
s : Set α
⊢ (s ≠ ⊥ ∧ ∀ (b : Set α), b ≠ ⊥ → b ⊆ s → s ⊆ b) → ∃ x, s = {x}

Tactic:
bot_eq_empty,

Goal state after:
α : Type u_2
s : Set α
⊢ (s ≠ ∅ ∧ ∀ (b : Set α), b ≠ ∅ → b ⊆ s → s ⊆ b) → ∃ x, s = {x}
Module: Mathlib.Order.CompactlyGenerated.Basic

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

Tactic:
replace hs : x ⊓ sSup s = ⊥ := by
      have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
      simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot

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 = ⊥
⊢ False
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
this : ⇑q.subtype '' ↑(inclusion h₁).range = ↑p
⊢ span S (⇑q.subtype '' range ⇑(inclusion h₁)) = q

Tactic:
refine this ▸ le_antisymm ?_ h₂
    simpa using span_mono (R := S) h₁

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
⊢ iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

Tactic:
by
  refine ⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  classical
  rw [← Finset.sup_erase_bot]
  set t := s.erase ⊥
  replace hf : InjOn f (f ⁻¹' t) := fun i hi j _ hij ↦ by
    refine hf ?_ ?_ hij <;> aesop (add norm simp [t])
  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⟩
  rw [← this, Finset.sup_image]
  specialize h (insert i (t.preimage _ hf))
  rw [Finset.supIndep_iff_disjoint_erase] at h
  exact h i (Finset.mem_insert_self i _)

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

Goal state before:
pp: R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h : ∀ (b : R), b ∈ l → Commute a b
⊢ Commute a l.sum

Tactic:
induction l with

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

Goal state before:
pp: R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h : ∀ (b : R), b ∈ l → Commute a b
⊢ Commute a l.sum

Tactic:
induction l with
  | nil => exact Commute.zero_right _
  | cons x xs ih =>
    rw [List.sum_cons]
    exact (h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

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

Goal state before:
pp: R : Type u_5
inst✝ : NonUnitalSemiring R
a : R
l : List R
h : ∀ (x : R), x ∈ l → a ∣ x
⊢ a ∣ l.sum

Tactic:
induction l with

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
x : M
⊢ IsCompactElement (R ∙ x)

Tactic:
by
  rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]
  intro d hemp hdir hsup
  have : x ∈ (sSup d) := (SetLike.le_def.mp hsup) (mem_span_singleton_self x)
  obtain ⟨y, ⟨hyd, hxy⟩⟩ := (mem_sSup_of_directed hemp hdir).mp this
  exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff] ⟩⟩

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map (fun x ↦ (s - x, a ::ₘ x)) s.powerset + map (fun x ↦ (a ::ₘ (s - x), x)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (s - x, a ::ₘ x)) s.powerset

Tactic:
rw [add_comm]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map (fun x ↦ (a ::ₘ (s - x), x)) s.powerset + map (fun x ↦ (s - x, a ::ₘ x)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (s - x, a ::ₘ x)) s.powerset
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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
i : ι
⊢ i ∈ s → map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i

Tactic:
hi

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
i : ι
hi : i ∈ s
⊢ map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case insert
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ f a b * ∏ x ∈ s.attach, f (↑x) (g ↑x ⋯) =
    f (↑⟨a, ⋯⟩) (Pi.cons s a b g ↑⟨a, ⋯⟩ ⋯) * ∏ x ∈ s.attach, f (↑⟨↑x, ⋯⟩) (Pi.cons s a b g ↑⟨↑x, ⋯⟩ ⋯)

Tactic:
simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj✝ : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
⊢ {i} ⊆ mulSupport f → False

Tactic:
hi

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj✝ : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
hi : {i} ⊆ mulSupport f
⊢ False
Module: Mathlib.Data.List.Find

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Bool
l : List α
h : ∀ (x : α), x ∈ l → p₁ x = p₂ x
⊢ find? p₁ l = find? p₂ l

Tactic:
induction l with

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = none ↔ ∀ (a : α), a ∈ s → ¬p a
hp : {x_1 | x_1 ∈ x ::ₘ s ∧ p x_1}.Subsingleton
⊢ find? p (x ::ₘ s) hp = none ↔ ∀ (a : α), a ∈ x ::ₘ s → ¬p a

Tactic:
rw [find?_cons]
    dsimp [Set.Subsingleton] at hp
    grind

Goal state after:
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 b h
  rw [Finsupp.ext_iff] at h ⊢
  simpa only [mapRange_apply, he.eq_iff] using h

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

Goal state before:
pp: case e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ 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
ha' : a ∉ s
⊢ f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j +
      (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) =
    (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
        ∏ j ∈ insert a s with a < j, f j +
      ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j

Tactic:
rw [add_comm]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ i ∈ (indicator s f).support → i ∈ s

Tactic:
hi

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : i ∈ (indicator s f).support
⊢ i ∈ s
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
h : f a = 0
b : M
⊢ f.update a b = single a b + f

Tactic:
by
  rw [update_eq_single_add_erase, erase_of_notMem_support (by simpa)]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b)

Tactic:
trans

Goal state after:
α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ?m.24

α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ ?m.24 = ∑ b ∈ s, single a (f b)

α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ α →₀ M
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
⊢ i ∉ s →
    ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
      (∑ i ∈ insert i s, g i).support = (insert i s).biUnion fun i ↦ (g i).support

Tactic:
hi

Goal state after:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
⊢ ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
    (∑ i ∈ insert i s, g i).support = (insert i s).biUnion fun i ↦ (g i).support
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : PartialOrder S
abv : AbsoluteValue R S
inst✝ : AddLeftMono S
l : List R
⊢ abv l.sum ≤ (List.map (⇑abv) l).sum

Tactic:
induction l with

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

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
a✝ : i ∈ s
⊢ i ∉ (indicator s f).support → single i ((indicator s f) i) = 0

Tactic:
hi

Goal state after:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
a✝ : i ∈ s
hi : i ∉ (indicator s f).support
⊢ single i ((indicator s f) i) = 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

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

Tactic:
subst H; exact nhf hf

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h₂.h0
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
⊢ i ∈ s → 0 ≤ f i

Tactic:
hi

Goal state after:
case h₂.h0
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
⊢ 0 ≤ f i
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
⊢ i ∈ s → f i ≤ g i

Tactic:
hi

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
⊢ f i ≤ g i
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' ↑(single b m).support)
⊢ comapDomain f (single b m) hf = 0

Tactic:
classical
  ext a
  simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]
  rintro rfl
  simp at hb

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

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst = i) ↔
    ∃ x, x ∈ { support := l.support.preimage (Sigma.mk i) ⋯, toFun := fun a ↦ l ⟨i, a⟩, mem_support_toFun := ⋯ }.support

Tactic:
simp only [Finset.mem_preimage, exists_and_right, exists_eq_right, mem_support_iff,
    Sigma.exists, Ne]

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✝³ : 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

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
⊢ f ∘ₗ f.splittingOfFinsuppSurjective s = id

Tactic:
by
  ext x
  dsimp [splittingOfFinsuppSurjective]
  congr
  rw [sum_single_index, one_smul]
  · exact (s (Finsupp.single x 1)).choose_spec
  · rw [zero_smul]

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
inst✝ : Nontrivial M
s t : Set α
⊢ Codisjoint (supported M R s) (supported M R t) ↔ Codisjoint s t

Tactic:
by
  refine ⟨fun h ↦ codisjoint_iff.mpr (eq_top_iff.mpr fun a ↦ ?_), codisjoint_supported_supported⟩
  obtain ⟨x, hx⟩ := exists_ne (0 : M)
  rw [codisjoint_iff, ← supported_union, eq_top_iff'] at h
  simpa [Finsupp.mem_supported, Finsupp.support_single _ hx] using h (Finsupp.single a x)

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
rw [← finprod_one]
  congr
  simp [eq_iff_true_of_subsingleton]

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 α
⊢ map (lmapDomain M R f) (supported M R s) = supported M R (f '' s)

Tactic:
by
  classical
  cases isEmpty_or_nonempty α
  · simp [s.eq_empty_of_isEmpty]
  refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_
  intro l hl
  refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
  · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
    exact Function.invFunOn_mem (by simpa using hl hc)
  · rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)

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

Goal state before:
pp: case h₁
α : 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 α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
⊢ i ∈ s ∧ v i = x → x ∈ ↑(map (linearCombination R v) (supported R R s))

Tactic:
hi

Goal state after:
case h₁
α : 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 α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x✝ : Fin m × Fin n
x : Fin m
y : Fin n
H : 0 < n
⊢ ↑y / n + ↑x = 0 + ↑x

Tactic:
Nat.div_eq_of_lt y.2

Goal state after:
m n : ℕ
x✝ : Fin m × Fin n
x : Fin m
y : Fin n
H : 0 < n
⊢ 0 + ↑x = 0 + ↑x
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) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
vecAlt0_vecAppend

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

Goal state before:
pp: n : ℕ
⊢ -↑n = 1

Tactic:
simp only [natCast_eq_last, neg_last]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Tactic:
have h'' : n = i := by
      simp only [not_lt] at h'
      exact (Nat.eq_of_le_of_lt_succ h' h).symm
    subst h''
    rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]
    rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Tactic:
by
  have h₁ : ∀ a, ∏ᶠ _ : a ∈ hf.toFinset, f a = f a := by simp
  have h₂ : ∏ᶠ a, f a = ∏ᶠ (a) (_ : a ∈ hf.toFinset), f a := by simp
  simp_rw [h₂, finprod_mem_finset_product, h₁]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy : (linearCombination R ⇑b) x = (linearCombination R ⇑b) y
⊢ b.repr ((linearCombination R ⇑b) y) = y

Tactic:
b.repr_linearCombination y

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy : (linearCombination R ⇑b) x = (linearCombination R ⇑b) y
⊢ y = y
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b : Basis ι R M
inst✝² : Semiring R₂
inst✝¹ : Module R₂ M'
inst✝ : SMulCommClass R R₂ M'
v : ι → M'
hv : LinearIndependent R v
x✝¹ x✝ : M
hab : ((b.constr R₂) v) x✝¹ = ((b.constr R₂) v) x✝
⊢ (linearCombination R v) (b.repr x✝¹) = (linearCombination R v) (b.repr x✝)

Tactic:
simpa [constr_def] using hab

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

Goal state before:
pp: y : ℕ∞
h : y ≠ 0
⊢ 0 ^ y = 0

Tactic:
by
  induction y with
  | top => exact zero_epow_top
  | coe y => rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]

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

Goal state before:
pp: case coe.coe
x : ℕ∞
h : x ≠ 0
a✝¹ a✝ : ℕ
y_z : ↑a✝¹ ≤ ↑a✝
⊢ (fun y ↦ x ^ y) ↑a✝¹ ≤ (fun y ↦ x ^ y) ↑a✝

Tactic:
exact pow_right_mono₀ (Order.one_le_iff_ne_zero.2 h) (Nat.cast_le.1 y_z)

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ Ioo (castAdd m a) (castAdd m b), f i = ∏ i ∈ Ioo a b, f (castAdd m i)

Tactic:
by
  simp [← map_castAddEmb_Ioo]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b c : G
⊢ c + a ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]

Tactic:
rw [add_comm]

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

Goal state before:
pp: a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ (c - b) * (a ^ b - 1) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1

Tactic:
mul_mod,

Goal state after:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ (c - b) % (a ^ b - 1) * ((a ^ b - 1) % (a ^ b - 1)) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) %
      (a ^ b - 1) =
    a ^ ((c - b) % b) - 1