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

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

Tactic:
intro m hm

Goal state after:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
⊢ m ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
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 : ι
hi : i ∈ image g s
⊢ i ∉ t → Disjoint (f i) (t.sup f)

Tactic:
hit

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
hit : i ∉ t
⊢ Disjoint (f i) (t.sup f)
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ⇑e ⁻¹' Ioo a b = Ioo (e.symm a) (e.symm b)

Tactic:
simp [← Ioi_inter_Iio]

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
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := ⋯
u : Finset ι := ⋯
⊢ Disjoint (f b) ((t.sup fun i ↦ (g i).sup f) ⊔ u.sup f)

Tactic:
symm

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 ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := ⋯
u : Finset ι := ⋯
⊢ Disjoint ((t.sup fun i ↦ (g i).sup f) ⊔ u.sup f) (f b)
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 : Finset α
ht : ↑t ⊆ range s
ht' : k ≤ t.sup id
f : ↥t → ι
hf : ∀ (x : ↥t), s (f x) = ↑x
b : α
hb : b ∈ t
⊢ id b ≤ (Finset.image f Finset.univ).sup s

Tactic:
← show s (f ⟨b, hb⟩) = id b from hf _

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
f : ↥t → ι
hf : ∀ (x : ↥t), s (f x) = ↑x
b : α
hb : b ∈ t
⊢ s (f ⟨b, hb⟩) ≤ (Finset.image f Finset.univ).sup s
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) ⟨a, b⟩) (⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) ((s.erase a).sup f)

Tactic:
Finset.sup_eq_iSup

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) ⟨a, b⟩) (⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) (⨆ a_1 ∈ s.erase a, f a_1)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ t.sup id ≤ sSup s

Tactic:
rw [Finset.sup_id_eq_sSup]
    exact sSup_le_sSup ht₁

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

Goal state before:
pp: 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 : S
hx : x ∈ s
⊢ x • y ∈ s • t

Tactic:
exact ⟨x, hx, y, hy, rfl⟩

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

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

Tactic:
split_ifs with h
  · exact prod_congr rfl fun i hi => by simp [h i hi]
  · push Not at h
    rcases h with ⟨i, hi, hq⟩
    exact prod_eq_zero hi (by simp [hq])

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

Goal state before:
pp: ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∏ x ∈ univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun a x_1 ↦ x a

Tactic:
by
  apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i) <;> simp

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

Goal state before:
pp: ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single i m)
⊢ p f

Tactic:
cases nonempty_fintype ι
  rw [← Finset.univ_sum_single f]
  exact Finset.sum_induction _ _ add zero (by simp [single])

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

Goal state before:
pp: α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = ↑l
⊢ x ∈ ↑(powersetAux l).revzip

Tactic:
have _ := Classical.decEq α

Goal state after:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = ↑l
x✝ : DecidableEq α
⊢ x ∈ ↑(powersetAux l).revzip
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
⊢ b = sSup {a | IsAtom a ∧ a ≤ b}

Tactic:
symm

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
⊢ sSup {a | IsAtom a ∧ a ≤ b} = b
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i

Tactic:
by
  classical
  calc
    ∏ i ∈ s, (f i + g i) =
        ∏ i ∈ s, ∑ p ∈ ({True, False} : Finset Prop), if p then f i else g i := by simp
    _ = ∑ p ∈ (s.pi fun _ => {True, False} : Finset (∀ a ∈ s, Prop)),
          ∏ a ∈ s.attach, if p a.1 a.2 then f a.1 else g a.1 := prod_sum _ _ _
    _ = ∑ t ∈ s.powerset, (∏ a ∈ t, f a) * ∏ a ∈ s \ t, g a :=
      sum_bij'
        (fun f _ ↦ {a ∈ s | ∃ h : a ∈ s, f a h})
        (fun t _ a _ => a ∈ t)
        (by simp)
        (by simp [Classical.em])
        (by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
        (by simp_rw [Finset.ext_iff, mem_filter, mem_powerset]; tauto)
        (fun a _ ↦ by
          simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
            Subtype.map_coe, id_eq, prod_attach]
          congr 2 with x
          simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
          tauto)

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 : Surjective e
⊢ Surjective (mapRange e he₀)

Tactic:
rw [← Set.range_eq_univ, range_mapRange, he.range_eq]
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
⊢ embDomain (Embedding.refl α) = id

Tactic:
by
  ext; simp [embDomain_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a = a' then b else 0

Tactic:
classical
  simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]

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

Goal state before:
pp: case pos
α : 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
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
mulIndicator_of_mem ha,

Goal state after:
case pos
α : 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
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
⊢ (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]

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

Goal state before:
pp: case c0
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
⊢ 0 < (map f s).prod

pp: case b0
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
⊢ 0 ≤ g a

Tactic:
· apply prod_pos
      grind

Goal state after:
case b0
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
⊢ 0 ≤ g a
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

pp: case neg
α : 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]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)

Goal state after:
case neg
α : 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
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
s t : Set α
h : Codisjoint s t
⊢ supported M R s ⊔ supported M R t = ⊤

Tactic:
eq_top_iff,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Codisjoint s t
⊢ ⊤ ≤ supported M R s ⊔ supported M R t
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)
⊢ f 1 = ∏ᶠ (i : α), f (g i)

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:
f.map_one,

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 = ∏ᶠ (i : α), f (g i)

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.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)

Tactic:
apply span_eq_of_le

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 α
⊢ v '' s ⊆ ↑(map (linearCombination R v) (supported R R s))

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 α
⊢ map (linearCombination R v) (supported R R s) ≤ span R (v '' s)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ (Fintype.linearCombination R v).range = span R (Set.range v)

Tactic:
rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
      LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]

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 : Set M
x : M
⊢ (∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x) → x ∈ span R s

Tactic:
rintro ⟨n, t, hts, -, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
n : M → R
t : Finset M
hts : ↑t ⊆ s
⊢ ∑ a ∈ t, n a • a ∈ span R s
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
m : M
s : Set M
| m ∈ span R s

Tactic:
← Set.image_id s

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
| m ∈ span R (_root_.id '' s)
Module: Mathlib.Algebra.Group.Fin.Basic

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

Tactic:
by simp only [lt_def, not_lt, val_fin_le, le_sub_one_iff, le_zero_iff]

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

Goal state before:
pp: N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ ∏ c ∈ Finite.toFinset ⋯, f c a = ∏ c ∈ Finite.toFinset ⋯, f c a

Tactic:
symm

Goal state after:
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ ∏ c ∈ Finite.toFinset ⋯, f c a = ∏ c ∈ Finite.toFinset ⋯, f c a
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
⊢ (finCongr ⋯) (finAddFlip ⟨n, ⋯⟩) = 0

Tactic:
finAddFlip_apply_mk_right le_rfl

Goal state after:
n : ℕ
⊢ (finCongr ⋯) ⟨n - n, ⋯⟩ = 0
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ (if h_1 : ↑⟨n, h⟩ < n then cast ⋯ (v (⟨n, h⟩.castLT h_1)) else cast ⋯ a) = cases a v ⟨0, ⋯⟩

Tactic:
dif_neg (lt_irrefl _)

Goal state after:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ cast ⋯ a = cases a v ⟨0, ⋯⟩
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∑ i ∈ f.support ∪ g.support, f i • v i = ∑ i ∈ f.support ∪ g.support, g i • v i

Tactic:
← sum_subset subset_union_left,

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∑ x ∈ f.support, f x • v x = ∑ i ∈ f.support ∪ g.support, g i • v i

case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∀ x ∈ f.support ∪ g.support, x ∉ f.support → f x • v x = 0
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y z : ℕ∞
x_0 : x < 1
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
rcases eq_zero_or_pos y with rfl | y_0

Goal state after:
case inl.inl
x z : ℕ∞
x_0 : x < 1
⊢ 0 ^ (0 + z) = 0 ^ 0 * 0 ^ z

case inl.inr
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y z : ℕ∞
y_0 : y = 0
⊢ x ^ (y * z) = (x ^ y) ^ z

pp: case inr
x y z : ℕ∞
y_0 : y ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
· simp [y_0]

Goal state after:
case inr
x y z : ℕ∞
y_0 : y ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ (d + 1) [MOD n]

Tactic:
Nat.pow_succ

Goal state after:
case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∑ i_1, ↑(Pi.single i j i_1) * m ^ ↑i_1 = ↑j * m ^ ↑i

Tactic:
Fintype.sum_eq_single i,

Goal state after:
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ↑(Pi.single i j i) * m ^ ↑i = ↑j * m ^ ↑i

m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∀ (x : Fin n), x ≠ i → ↑(Pi.single i j x) * m ^ ↑x = 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x +
      x *
        ∑ i,
          (↑a / x / ∏ i_1, Fin.cons x xs (Fin.castLE ⋯ i_1.succ)) % xs i *
            ∏ i_1, Fin.cons x xs (Fin.castLE ⋯ i_1.succ) =
    ↑a

Tactic:
convert! Nat.mod_add_div _ _

Goal state after:
case e'_2.e'_6
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ∑ i, (↑a / x / ∏ i_1, Fin.cons x xs (Fin.castLE ⋯ i_1.succ)) % xs i * ∏ i_1, Fin.cons x xs (Fin.castLE ⋯ i_1.succ) =
    ↑a / x
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∑ i_1, ↑(Pi.single i j i_1) * ∏ j, n (Fin.castLE ⋯ j) = ↑j * ∏ j, n (Fin.castLE ⋯ j)

Tactic:
Fintype.sum_eq_single i,

Goal state after:
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ↑(Pi.single i j i) * ∏ j, n (Fin.castLE ⋯ j) = ↑j * ∏ j, n (Fin.castLE ⋯ j)

m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j, n (Fin.castLE ⋯ j) = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case neg.isTrue
a b c : ℕ
h : ¬c = 0
h✝ : c ≤ a % c + b % c
⊢ 1 ≤ 1

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case neg.isFalse
a b c : ℕ
h : ¬c = 0
h✝ : ¬c ≤ a % c + b % c
⊢ 0 ≤ 1

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case neg
a b c : ℕ
h : ¬c = 0
⊢ (if c ≤ a % c + b % c then 1 else 0) ≤ 1

Tactic:
split <;> decide

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n : ℕ
⊢ ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n : ℕ
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
hn : n % 2 = 1
⊢ 2 ∣ 4

Tactic:
decide

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

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
g h : G
L : List G
⊢ g * (h⁻¹ * ∏ i, L[i] ^ (-1) ^ ↑i) =
    (g :: h :: L)[0] ^ (-1) ^ ↑0 *
      ((g :: h :: L)[Fin.succ 0] ^ (-1) ^ ↑(Fin.succ 0) * ∏ i, (g :: h :: L)[i.succ.succ] ^ (-1) ^ ↑i.succ.succ)

Tactic:
simp [pow_add]

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
i : G →* L
his : i ∈ s
⊢ ∃ y, i y ≠ a y

Tactic:
by_contra! hia

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
i : G →* L
his : i ∈ s
hia : ∀ (y : G), i y = a y
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard ≠ 0
⊢ ¬s = ∅

Tactic:
← encard_eq_zero

Goal state after:
α : Type u_1
s : Set α
h : s.encard ≠ 0
⊢ ¬s.encard = 0
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_4
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
cases finite_or_infinite α

Goal state after:
case inl
α : Type u_4
h✝ : Finite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

case inr
α : Type u_4
h✝ : Infinite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_4
h✝ : Finite α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
simp only [this, *, Nat.card_eq_fintype_card, dif_pos]

Goal state after: