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

Goal state before:
pp: case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ((Finset.image (fun x ↦ x i) s).biUnion fun a ↦ {c ∈ s | c i = a}).SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
refine Finset.SupIndep.biUnion ?_ (by grind)

Goal state after:
case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ (Finset.image (fun x ↦ x i) s).SupIndep fun i_1 ↦ {c ∈ s | c i = i_1}.sup fun k ↦ ⨅ i, f i (k i)
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 τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p ≤ p'
h : p ⊔ f.ker < p' ⊔ f.ker
⊢ map f p < map f p'

Tactic:
simp_rw [← comap_map_eq] at h
  exact lt_of_le_of_ne (map_mono hab) (ne_of_apply_ne _ h.ne)

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ (mulSupport f).mulIndicator (f * g) = f

Tactic:
refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport
  have : g x = 1 := notMem_mulSupport.1 (disjoint_left.1 h hx)
  rw [Pi.mul_apply, this, mul_one]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
⊢ s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g

Tactic:
by
  ext x
  by_cases h : x ∈ s
  · rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
      Set.mulIndicator_of_notMem (Set.notMem_compl_iff.2 h), mul_one]
  · rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ onFinsetSupport s f = {a ∈ s | ¬f a = 0}

Tactic:
rw [onFinsetSupport]

Goal state after:
α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ {a ∈ s | f a ≠ 0} = {a ∈ s | ¬f a = 0}
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
⊢ toSpanSingleton R M 0 = 0

Tactic:
ext
  simp

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

Goal state before:
pp: ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Goal state after:
case inl
ι : Type u_5
s : Finset ι
f : ι → ℕ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ (∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0

case inr
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
⊢ equivFunOnFinite.symm (equivFunOnFinite (single x m)) = single x m

Tactic:
Equiv.symm_apply_apply

Goal state after:
α : Type u_1
M : Type u_5
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
⊢ single x m = single x m
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i : α
f : α →₀ M
a : α
b : M
this : DecidableEq α
⊢ Finset α

Tactic:
haveI := Classical.decEq M

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i : α
f : α →₀ M
a : α
b : M
this✝ : DecidableEq α
this : DecidableEq M
⊢ Finset α
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ some 0 = 0

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
f g : Option α →₀ M
⊢ (f + g).some = f.some + g.some

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
m : M
⊢ (single none m).some = 0

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f).some = f

Tactic:
ext
  simp

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
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ i, s i
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Tactic:
simp only [mem_iInter, not_forall] at hx

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ x_1, x ∉ s x_1
⊢ 1 = ⨅ i, (s i).mulIndicator f x
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ i, s i
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x

Tactic:
· rw [mulIndicator_of_notMem hx]
    simp only [mem_iInter, not_forall] at hx
    rcases hx with ⟨j, hj⟩
    refine le_antisymm (by simp only [← h1, le_iInf_iff, bot_le, forall_const]) ?_
    simpa [mulIndicator_of_notMem hj] using (iInf_le (fun i ↦ (s i).mulIndicator f) j) x

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

Goal state before:
pp: α : Type u_1
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
h1 : (d a + (erase a d).sum fun x n ↦ n) = 1
ha : d a ≠ 0 a
⊢ d a = 1 ∧ ∀ (i : α), i ≠ a → d i = 0

Tactic:
Nat.add_eq_one_iff,

Goal state after:
α : Type u_1
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
h1 : d a = 0 ∧ ((erase a d).sum fun x n ↦ n) = 1 ∨ d a = 1 ∧ ((erase a d).sum fun x n ↦ n) = 0
ha : d a ≠ 0 a
⊢ d a = 1 ∧ ∀ (i : α), i ≠ a → d i = 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
⊢ d a = 1 ∧ ∀ (i : α), i ≠ a → d i = 0

Tactic:
rw [← add_sum_erase' _ a _ (fun _ ↦ rfl), Nat.add_eq_one_iff, or_iff_not_imp_left] at h1
      simp_all +contextual [sum, support_erase, sum_eq_zero_iff, mem_erase, erase_ne]

Goal state after:
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
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
apply prod_map_le_prod_map₀

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 : ι), i ∈ s → 0 ≤ f i

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
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
⊢ (addMonoidHom f).comp (mapRange.addMonoidHom g) = (mapRange.addMonoidHom g).comp (addMonoidHom f)

Tactic:
ext
  simp

Goal state after:
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 : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ v₁ a = v₂ a

Tactic:
rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
⊢ comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
⊢ (f.curry.sum fun a f ↦ f.sum (g a)) = f.sum fun p c ↦ g p.1 p.2 c

Tactic:
by
  rw [← sum_uncurry_index', uncurry_curry]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 =
    ∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j

Tactic:
simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring

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✝¹ : Zero γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
⊢ (fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) ((fun fg ↦ fg.1.sumElim fg.2) fg) = fg

Tactic:
ext <;> simp

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
αs : ι → Type u_12
inst✝² : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝¹ : Fintype η
ιs : η → Type u_14
inst✝ : Zero α
f : (j : η) × ιs j →₀ α
a✝ : (j : η) × ιs j
⊢ ((fun f ↦ onFinset (univ.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f.split) a✝ = f a✝

Tactic:
simp [split]

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
αs : ι → Type u_12
inst✝² : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝¹ : Fintype η
ιs : η → Type u_14
inst✝ : Zero α
f : (j : η) → ιs j →₀ α
x✝ : η
a✝ : ιs x✝
⊢ (((fun f ↦ onFinset (univ.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f).split x✝) a✝ = (f x✝) a✝

Tactic:
simp [split]

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

Goal state before:
pp: α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
⊢ (single a r) b • f a = (single a (r • f b)) b

Tactic:
by_cases h : a = b <;> simp [h]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
p q : α →₀ M
hp : p ∈ {p | ↑p.support ⊆ s}
hq : q ∈ {p | ↑p.support ⊆ s}
⊢ p + q ∈ {p | ↑p.support ⊆ s}

Tactic:
classical
    refine Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) ?_) (union_subset hp hq)
    rw [Finset.coe_union]

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

Goal state before:
pp: n : ℕ
s t : Finset ℕ
hs : ∀ m ∈ s, m < n
ht : ∀ m ∈ t, m < n
⊢ s.attachFin hs ⊆ t.attachFin ht ↔ s ⊆ t

Tactic:
by
  simp [← map_subset_map (f := Fin.valEmbedding)]

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α → α'
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = linearCombination R (v' ∘ f)

Tactic:
ext
  simp

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

Goal state before:
pp: m n : ℕ
i : Fin (m + n)
hi : m ≤ ↑i
⊢ ↑i - m < n

Tactic:
lia

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

Goal state before:
pp: n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
this : ↑i + m ≤ ↑j
⊢ ↑j - m < n

Tactic:
lia

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) '' Ioi i = Ioi (i.addNat m)

Tactic:
rw [← preimage_addNat_Ioi_addNat, image_preimage_eq_of_subset]

Goal state after:
n m : ℕ
i : Fin n
⊢ Ioi (i.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Iic i ↔ x✝ ∈ Ici i.rev

Tactic:
simp [rev_le_iff]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
by
  rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union hst hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport]

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Iic a) = Iic ↑a

Tactic:
by
  rw [← attachFin_Iic, map_valEmbedding_attachFin]

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

Goal state before:
pp: α✝ : Type u
m n o✝ : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
h : ¬↑i < m
⊢ ↑i - m < n

Tactic:
lia

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

Goal state before:
pp: α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
⊢ o = m + n

Tactic:
lia

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
⊢ (finSuccEquiv' i) m.castSucc = some m

Tactic:
← Fin.succAbove_of_castSucc_lt _ _ h,

Goal state after:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
⊢ (finSuccEquiv' i) (i.succAbove m) = some m
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
m n o : ℕ
hm : m = n + n
v : Fin m → α
k : Fin n
⊢ ↑k + ↑k < m

Tactic:
lia

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

Goal state before:
pp: n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isRight = decide (n ≤ i)

Tactic:
simp_rw [← not_lt, decide_not, ← isLeft_finSumNatEquiv_symm_apply]

Goal state after:
n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isRight = !((finSumNatEquiv n).symm i).isLeft
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k - m < n + m

Tactic:
lia

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

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n < n

Tactic:
lia

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

Goal state before:
pp: m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k - m < n

Tactic:
lia

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

Goal state before:
pp: case hst
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ Disjoint (s ∩ t) (s \ t)

Tactic:
rw [disjoint_iff_inf_le]
    exact fun x hx => hx.2.2 hx.1.2

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ 1 < n + 2

Tactic:
lia

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

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) < n + 1 + 1

Tactic:
lia

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

Goal state before:
pp: α : Type u
m n o : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n

Tactic:
lia

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

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
⊢ i < n

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)

Tactic:
by
  rw [Set.powerset_insert,
    finprod_mem_union (disjoint_powerset_insert has) hs.powerset (hs.powerset.image (insert a)),
    finprod_mem_image (powerset_insert_injOn has)]

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ ↑k - 1 < n

Tactic:
lia

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
t : Set β
f : α → β → M
ht : t.Finite
s : Finset α
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ ↑s), f i j

Tactic:
lift t to Finset β using ht

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ ↑t), f i j = ∏ᶠ (j : β) (_ : j ∈ ↑t) (i : α) (_ : i ∈ ↑s), f i j
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
x : α
hx : x ∈ mulSupport fun a ↦ ∏ b ∈ s, f a b
⊢ x ∈ ⋃ i ∈ ↑s, mulSupport fun a ↦ f a i

Tactic:
simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
x : α
hx : x ∈ mulSupport fun a ↦ ∏ b ∈ s, f a b
⊢ ∃ i ∈ s, ¬f x i = 1
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
ha : ↑a + 1 < n
⊢ ↑a < ↑a + 1

Tactic:
lia

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

Goal state before:
pp: n : ℕ
⊢ n < n + 1

Tactic:
lia

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

Goal state before:
pp: n : ℕ
α : Type u_1
v : Fin n → α
a : α
⊢ snoc v a = fun i ↦ cons a v ((finRotate (n + 1)) i)

Tactic:
ext ⟨i, h⟩
  by_cases h' : i < n
  · rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']
    rfl
  · 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.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
⊢ x = y

Tactic:
rw [← b.repr_linearCombination x, hxy, b.repr_linearCombination y]

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

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

Tactic:
by
  rw [prod_univ_castSucc, prod_univ_five]
  rfl

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

Goal state before:
pp: case mp.refine_1
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ 0 < ↑n

Tactic:
lia

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

Goal state before:
pp: case inl
b c : ℕ
⊢ (0 ^ c - 1) % (0 ^ b - 1) = 0 ^ (c % b) - 1

Tactic:
simp [zero_pow_eq]

Goal state after:
case inl
b c : ℕ
⊢ ((if c = 0 then 1 else 0) - 1) % ((if b = 0 then 1 else 0) - 1) = (if c % b = 0 then 1 else 0) - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ m.Coprime (n - m) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_sub_self_right h]

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

Goal state before:
pp: case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ ↑i < ↑a

Tactic:
lia

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

Goal state before:
pp: case refine_2.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ ↑i < ↑a + 1

Tactic:
lia

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

Goal state before:
pp: case refine_2.inr.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i = ↑a
⊢ ↑a ≤ ↑i

Tactic:
lia

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

Goal state before:
pp: case refine_2.inr.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i = ↑a
⊢ ↑i ≤ ↑a

Tactic:
lia

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

Goal state before:
pp: case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ ↑a ≤ ↑i

Tactic:
lia

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

Goal state before:
pp: case refine_2.inr.inr.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ ↑a + 1 ≤ ↑i

Tactic:
lia

Goal state after: