mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ ¬2 = 0

Tactic:
two_ne_zero,

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ ¬False
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * (a + b) = x✝¹ * (x✝ * (a + b))

Tactic:
rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
⊢ C x₁ hx₁

Tactic:
refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc

Goal state after:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
⊢ ∃ (x : x₁ ∈ ⨆ i, S i), C x₁ x
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
by ext <;> exact right_distrib ..

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R ≃+* S
K : NonUnitalSubsemiring R
x : S
⊢ x ∈ map (↑f) K ↔ f.symm x ∈ K

Tactic:
by
  convert! @Set.mem_image_equiv _ _ (↑K) f.toEquiv x

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ a

Tactic:
by
  rw [mul_comm] at h'
  exact hp.pow_dvd_of_dvd_mul_left n h h'

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ ⇑f '' ⇑f ⁻¹' {0} ⊆ ↑(map f s)

Tactic:
exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (s.map f).zero_mem)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ b = a * x) → ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b

Tactic:
· rintro ⟨x, ⟨hx, rfl⟩⟩
    use x

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬b ≤ a ∧ IsEmpty ↑(Ioo a (b ⊔ a)) → ¬b ≤ a ∧ IsEmpty ↑(Ioo (b ⊓ a) b)

Tactic:
(infIooOrderIsoIooSup b a).symm.toEquiv.isEmpty_congr

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬b ≤ a ∧ IsEmpty ↑(Ioo (b ⊓ a) b) → ¬b ≤ a ∧ IsEmpty ↑(Ioo (b ⊓ a) b)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set M
hst : Disjoint (span R s) (span R t)
⊢ Disjoint (s \ {0}) t

Tactic:
by
  rw [disjoint_iff_forall_ne]
  rintro v ⟨hvs, hv0 : v ≠ 0⟩ _ hvt rfl
  exact hv0 <| (disjoint_def.1 hst) v (subset_span hvs) (subset_span hvt)

Goal state after:
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) := ⋯
⊢ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m} ≤ p

Tactic:
rw [sSup_le_iff]
    rintro S ⟨_, ⟨_, ⟨_, rfl⟩⟩⟩
    rwa [span_singleton_le_iff_mem]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk i) (g i)
v : Finset ((x : ι) × β x) := t.biUnion fun j ↦ map (Function.Embedding.sigmaMk j) (g j)
⊢ Disjoint ((fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩) i) (t.sup fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩)

Tactic:
suffices Disjoint (u.sup f) (v.sup f) by simpa only [sup_map, sup_biUnion, u, v]

Goal state after:
case refine_1
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk i) (g i)
v : Finset ((x : ι) × β x) := t.biUnion fun j ↦ map (Function.Embedding.sigmaMk j) (g j)
⊢ Disjoint (u.sup f) (v.sup f)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, s.sup (id ∘ f) ≤ x

Tactic:
← Finset.sup_image

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, (Finset.image f s).sup id ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Tactic:
tfae_have 1 → 2 := @WellFoundedGT.isSupFiniteCompact α _

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b

Tactic:
by
  simp_rw [disjoint_iff, h.inf_sSup_eq, iSup_eq_bot]

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a

Tactic:
by
  simp_rw [disjoint_iff, h.iSup_inf_eq, iSup_eq_bot]

Goal state after:
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
⊢ ∀ i_1 ∈ Finset.image (fun x ↦ x i) s, ∀ (b : (i : ι) → κ i), b ∈ s ∧ b i = i_1 → ⨅ i, f i (b i) ≤ f i i_1

Tactic:
and_imp

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
⊢ ∀ i_1 ∈ Finset.image (fun x ↦ x i) s, ∀ b ∈ s, b i = i_1 → ⨅ i, f i (b i) ≤ f i i_1
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -span R s ≤ span R (-s)

Tactic:
· rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]
    exact subset_span

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

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

Tactic:
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]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ g.support
hf : f a = 0
⊢ g a = 0

Tactic:
notMem_support_iff

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : g a = 0
hf : f a = 0
⊢ g a = 0
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
f : M → N
hf : f 0 = 0
x✝ : α
⊢ (mapRange f hf 0) x✝ = 0 x✝

Tactic:
simp only [hf, zero_apply, mapRange_apply]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
⊢ ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ ↑s) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0

Tactic:
have : (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
      ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ i (hi : i ∉ s), g i = 0) := by grind

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔ (∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ i ∉ s, g i = 0
⊢ ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ ↑s) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

Tactic:
classical rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ (f.update a b) i = if i = a then b else f i

Tactic:
delta update Function.update

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ { support := if b = 0 then f.support.erase a else insert a f.support,
        toFun := fun a_1 ↦ if h : a_1 = a then ⋯ ▸ b else f a_1, mem_support_toFun := ⋯ }
      i =
    if i = a then b else f i
Module: Mathlib.Algebra.Order.Group.Indicator

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

Tactic:
simp_rw [indicator_apply]

Goal state after:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ (if a ∈ s then f a else 0) ≤ if a ∈ {a | 0 ≤ f a} then f a else 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_1
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
⊢ ∃ a, d = single a 1

Tactic:
have hd0 : d ≠ 0 := (by simp [·] at h1)
    obtain ⟨a, ha⟩ := ne_iff.mp hd0
    obtain ⟨hda, hda'⟩ : d a = 1 ∧ ∀ i ≠ a, d i = 0 := by
      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]
    use a
    ext b
    by_cases hb : b = a
    · rw [hb, single_eq_same, hda]
    · simpa only [single_eq_of_ne hb] using hda' b hb

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
ι : Type u_3
inst✝ : Finite α
f : ι → α → M
hf : ∀ (a : α), (mulSupport fun x ↦ f x a).Finite
i : ι
hi : f i ≠ 1
⊢ ∃ i_1, f i i_1 ≠ 1

Tactic:
exact ne_iff.mp hi

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ ∏ a ∈ f2.support \ f1.support ∪ f1.support, g2 a (f2 a)

Tactic:
prod_union sdiff_disjoint

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ (∏ x ∈ f2.support \ f1.support, g2 x (f2 x)) * ∏ x ∈ f1.support, g2 x (f2 x)
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
⊢ indicator s f = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)

Tactic:
rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach]
  · refine Finset.sum_congr rfl (fun _ _ => ?_)
    rw [indicator_of_mem]
  · intro i _ hi
    rw [notMem_support_iff.mp hi, single_zero]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : IsOrderedCancelMonoid α
inst✝ : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
hle : ∀ (i : ι), i ∈ s → f i ≤ g i
hlt : ∃ i, i ∈ s ∧ f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
by
  obtain ⟨l⟩ := s
  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  exact List.prod_lt_prod' f g hle hlt

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
b : β
hb : b ∉ Set.range ⇑f
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b

Tactic:
replace hg : g b = 0 := notMem_support_iff.mp <| mt (hg ·) hb
    rw [embDomain_of_notMem_range _ _ _ hb, hg]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ ∏ x ∈ f.support, g x (f x) = f.prod g

Tactic:
Finsupp.prod

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✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
gcongr with j hj j hj <;> simp_all

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
⊢ #s * n ≤ ∑ t ∈ B, #(s ∩ t)

Tactic:
apply (s.card_nsmul_le_sum _ _ h).trans
  simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
  exact sum_comm.le

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

Goal state before:
pp: α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
⊢ f.extendDomain = embDomain (Embedding.subtype P) f

Tactic:
ext a
  by_cases h : P a
  · refine Eq.trans ?_ (embDomain_apply_self (.subtype P) f (Subtype.mk a h)).symm
    simp [h]
  · rw [embDomain_of_notMem_range] <;> simp [*]

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
⊢ l.support = l.splitSupport.sigma fun i ↦ (l.split i).support

Tactic:
simp_rw [Finset.ext_iff, splitSupport, split, comapDomain, Sigma.forall, mem_sigma, mem_image,
    mem_preimage]
  tauto

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
this : ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)).range ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)

Tactic:
rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this

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

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

Tactic:
← preimage_natAdd_Ico_natAdd,

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

case m
n m : ℕ
i j : Fin n
⊢ ℕ
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
x✝¹ x✝ : M
⊢ (f x✝¹ + f x✝) i = f x✝¹ i + f x✝ i

Tactic:
Pi.add_apply

Goal state after:
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
x✝¹ x✝ : M
⊢ f x✝¹ i + f x✝ i = f x✝¹ i + f x✝ i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ rev ⁻¹' Iic i = Ici i.rev

Tactic:
ext; 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 α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
    finprod_mem_union_inter hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport, ←
    finprod_mem_inter_mulSupport f (s ∩ t)]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
⊢ (b.reindex e).sumCoords = b.sumCoords

Tactic:
by
  ext x
  simp only [coe_sumCoords, repr_reindex]
  exact Finsupp.sum_mapDomain_index (fun _ => rfl) fun _ _ _ => rfl

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) (i.succAbove m) = some m

Tactic:
finSuccEquiv'_succAbove

Goal state after:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
⊢ some m = some m
Module: Mathlib.Logic.Equiv.Fin.Basic

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

Tactic:
finSuccEquiv'_succAbove

Goal state after:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ some m = some m
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (finSuccEquiv' (Fin.last n)) ((Fin.last n).succAbove i) = some i

Tactic:
finSuccEquiv'_succAbove

Goal state after:
n : ℕ
i : Fin n
⊢ some i = some i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : HasFiniteMulSupport (f ∘ some)
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)

Tactic:
replace hf : (mulSupport f).Finite := by simpa [finite_option]
  convert!
    finprod_mem_insert' f (show none ∉ Set.range Option.some by simp) (hf.subset inter_subset_right)
  · simp
  · rw [finprod_mem_range]
    exact Option.some_injective _

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
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ᶠ (x : α), ∏ y ∈ s with f y = x, g y = ∏ k ∈ s, g k

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset]
  · rw [Finset.prod_image']
    exact fun _ _ ↦ rfl
  · intro x hx
    rw [mem_mulSupport] at hx
    obtain ⟨a, h, -⟩ := Finset.exists_ne_one_of_prod_ne_one hx
    simp only [Finset.mem_filter, Finset.coe_image, mem_image, SetLike.mem_coe] at h ⊢
    exact ⟨a, h⟩

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n✝ n : ℕ
inst✝ : NeZero n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ (n - ↑⟨a, ha⟩ + a) % n = ↑0

Tactic:
rw [Fin.val_zero, Nat.sub_add_cancel, Nat.mod_self]
      exact le_of_lt ha

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

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

Tactic:
by_cases h' : i < n

Goal state after:
case pos
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⟩)

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⟩)
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ (if ⊤ < ⊤ then x ^ ⊤.toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤) = ⊤

Tactic:
if_neg,

Goal state after:
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ (if x = 0 then 0 else if x = 1 then 1 else ⊤) = ⊤

case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬⊤ < ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ (if x = 0 then 0 else if x = 1 then 1 else ⊤) = ⊤

pp: case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬⊤ < ⊤

Tactic:
if_neg,

Goal state after:
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ (if x = 1 then 1 else ⊤) = ⊤

case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬x = 0

case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬⊤ < ⊤
Module: Mathlib.Data.ENat.Pow

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

Tactic:
Order.lt_one_iff.1 x_0

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

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

Tactic:
simp [z_0]

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
i_lt : i < n + 1
⊢ ∏ j, ⟨i + 1, h⟩.insertNth x (cons hd tl) j = x * ∏ j, cons hd tl j

Tactic:
let i_fin : Fin (n + 1) := ⟨i, i_lt⟩

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
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
⊢ ∏ j, ⟨i + 1, h⟩.insertNth x (cons hd tl) j = x * ∏ j, cons hd tl j
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
by
  simp [← map_finCongr_Ioo]

Goal state after: