mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⨆ i, p i ↔ ∃ i, x ∈ p i

Tactic:
change x ∈ ⋃ s ∈ Set.range p, s ↔ _

Goal state after:
R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⋃ s ∈ Set.range p, ↑s ↔ ∃ i, x ∈ p i
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
hpq : Disjoint p q
⊢ map f ⊥ = ⊥

Tactic:
map_bot

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
hpq : Disjoint p q
⊢ ⊥ = ⊥
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ x✝² • ((algebraMap R A) x✝¹ + (algebraMap R A) x✝) = (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝)

Tactic:
smul_add,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ x✝² • (algebraMap R A) x✝¹ + x✝² • (algebraMap R A) x✝ = (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝)
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
by
    apply FaithfulSMul.algebraMap_injective R A
    rw [algebraMap.smul', map_add, smul_add, ← algebraMap.smul', ← algebraMap.smul', ← map_add]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case closed_under_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 S R M
r✝ : S
m : M
hm : m ∈ N
⊢ r✝ • m ∈ r✝ • N

Tactic:
exact ⟨m, hm, rfl⟩

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
a b : α
hab : Disjoint a b
u : α
hu : IsCompl (a ⊔ b) u
⊢ ∃ a', a ≤ a' ∧ IsCompl a' b

Tactic:
exact ⟨u ⊔ a, le_sup_right, hab.isCompl_sup_left_of_isCompl_sup_right hu.symm⟩

Goal state after:
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
ι : Sort u_9
v : ι → M
⊢ span R (range v) = ⨆ i, R ∙ v i

Tactic:
by
  rw [span_eq_iSup_of_singleton_spans, iSup_range]

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) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
w✝ : M
left✝¹ : w✝ ∈ p
left✝ : w✝ ≠ 0
⊢ R ∙ w✝ ≤ p

Tactic:
rwa [span_singleton_le_iff_mem]

Goal state after:
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 : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T

Tactic:
classical
  refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
  · refine ⟨{x}, ?_, ?_⟩
    · rwa [Finset.coe_singleton, Set.singleton_subset_iff]
    · rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x
  · use ∅
    simp
  · rintro x y - - ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩
    refine ⟨X ∪ Y, ?_, ?_⟩
    · rw [Finset.coe_union]
      exact Set.union_subset hX hY
    rw [Finset.coe_union, span_union, mem_sup]
    exact ⟨x, hxX, y, hyY, rfl⟩
  · rintro a x - ⟨T, hT, h2⟩
    exact ⟨T, hT, smul_mem _ _ h2⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case hs
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b ↦ f ⟨i, b⟩
⊢ s.SupIndep fun i ↦ (map (Function.Embedding.sigmaMk i) (g i)).sup f

pp: case hg
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b ↦ f ⟨i, b⟩
⊢ ∀ i' ∈ s, (map (Function.Embedding.sigmaMk i') (g i')).SupIndep f

Tactic:
· simpa using! hs

Goal state after:
case hg
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b ↦ f ⟨i, b⟩
⊢ ∀ i' ∈ s, (map (Function.Embedding.sigmaMk i') (g i')).SupIndep f
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case hs
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')
ht : t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')
⊢ s.SupIndep fun i ↦ (image (fun b ↦ (i, b)) t).sup f

pp: case hg
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')
ht : t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')
⊢ ∀ i' ∈ s, (image (fun b ↦ (i', b)) t).SupIndep f

Tactic:
· simpa using! hs

Goal state after:
case hg
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')
ht : t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')
⊢ ∀ i' ∈ s, (image (fun b ↦ (i', b)) t).SupIndep f
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
⊢ InjOn (fun b ↦ ⨅ i, t i (b i)) {b | ⨅ i, t i (b i) ≠ ⊥}

Tactic:
by
  intro b₁ hb₁ b₂ hb₂ h_eq
  beta_reduce at h_eq
  by_contra h_ne
  obtain ⟨i, hi⟩ : ∃ i, b₁ i ≠ b₂ i := Function.ne_iff.mp h_ne
  have := calc
    ⨅ i, t i (b₁ i) ≤ t i (b₁ i) ⊓ t i (b₂ i) := le_inf (iInf_le ..) (h_eq ▸ iInf_le ..)
    _ = ⊥ := (ht i (b₁ i) |>.mono_right <| le_iSup₂_of_le (b₂ i) hi.symm le_rfl).eq_bot
  simp_all

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

Goal state before:
pp: case empty
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ ∅, f x = 0 ↔ ∃ a ∈ ∅, f a = 0

Tactic:
exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f g : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
⊢ f = g → ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩

Tactic:
rintro rfl _

Goal state after:
case mp
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
s✝ : ↑S
⊢ f ⟨↑s✝, ⋯⟩ = f ⟨↑s✝, ⋯⟩
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) ((s.erase ⊥).sup id)

Tactic:
set t := s.erase ⊥

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
⊢ Disjoint (f i) (t.sup id)
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:
apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i) <;> simp

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 ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) ((s.erase ⊥).sup id)

Tactic:
set t := s.erase ⊥

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

Tactic:
ext ⟨x, y⟩; simp

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
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ (p ⊔ p').prod (q₁ ⊔ q₁') ≤ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
simp only [SetLike.le_def, mem_prod, and_imp, Prod.forall]

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ ∀ (a : M) (b : M'), a ∈ p ⊔ p' → b ∈ q₁ ⊔ q₁' → (a, b) ∈ p.prod q₁ ⊔ p'.prod q₁'
Module: Mathlib.Data.List.Find

Goal state before:
pp: case swap
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

Tactic:
by_cases p x <;> by_cases p y

Goal state after:
case pos
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : p x = true
h✝ : p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

case neg
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : p x = true
h✝ : ¬p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

case pos
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : ¬p x = true
h✝ : p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)

case neg
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x y : α
l : List α
hp : ∀ ⦃x_1 : α⦄, x_1 ∈ y :: x :: l ∧ p x_1 = true → ∀ ⦃y_1 : α⦄, y_1 ∈ y :: x :: l ∧ p y_1 = true → x_1 = y_1
h✝¹ : ¬p x = true
h✝ : ¬p y = true
⊢ find? p (y :: x :: l) = find? p (x :: y :: l)
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
n k : ℕ
⊢ ∏ i ∈ range k, (↑n - ↑i) = ↑(∏ i ∈ range k, (n - i))

Tactic:
rw [prod_natCast]

Goal state after:
R : Type u_4
inst✝ : CommRing R
n k : ℕ
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint {a} f.support

Tactic:
disjoint_singleton_left

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ a ∉ f.support
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • f x

Tactic:
· simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg,
      map_inv_natCast_smul _ R S]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a) * abv (-a) = abv a * abv a

Tactic:
rw [← abv.map_mul, neg_mul_neg, abv.map_mul]

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
⊢ indicator s f = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)

Tactic:
← sum_single (indicator s f),

Goal state after:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ (indicator s f).sum single = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ f hx_w ∈ (mapDomain f s).support

Tactic:
simp only [mem_support_iff, Ne]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ ¬(mapDomain f s) (f hx_w) = 0
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✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i

Tactic:
by
  classical
  simp_rw [prod_eq_mul_prod_sdiff_singleton_of_mem hi]
  refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
  · rw [right_distrib]
    gcongr with j hj <;> aesop
  · apply prod_nonneg
    simp only [and_imp, mem_sdiff, mem_singleton]
    exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
y : β
⊢ (single a (single b m)).uncurry (a, y) = (single (a, b) m) (a, y)

Tactic:
simp [single_apply, *]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
x : α
y : β
hne : a ≠ x
⊢ (single a (single b m)).uncurry (x, y) = (single (a, b) m) (x, y)

Tactic:
simp [single_apply, *]

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.uncurry.sum fun p c ↦ g p c) = f.sum fun a f ↦ f.sum fun b ↦ g (a, b)

Tactic:
simp [Finsupp.sum, Finsupp.uncurry, Finset.sum_disjiUnion]

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

Goal state before:
pp: case hf
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : x ∉ insert i s
⊢ 1 ≤ f x

Tactic:
simp only [mem_insert, not_or] at h'x

Goal state after:
case hf
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x = i ∧ x ∉ s
⊢ 1 ≤ f x
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case inr
ι : 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, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
refine le_of_mul_le_mul_of_pos_left
      (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2) ?_) h
    calc
      _ = ∑ i ∈ s, 2 * r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j) := by
          simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
      _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) := by
          gcongr with i hi
          have ht : (r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j)) ^ 2 ≤
              (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, r j) ^ 2) := by
            grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]
            exact sq_nonneg _
          refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_le_mul
            (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
          repeat rw [mul_assoc]
      _ = _ := by simp_rw [sum_add_distrib, ← sum_mul]; ring

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

Goal state before:
pp: case refine_1
α : Type u_2
s : Finset α
f : α → ℕ
h : ∑ x ∈ s, f x ≤ 1
x y : α
hsx : x ∈ s
hsy : y ∈ s
hfx : f x ≠ 0
hfy : f y ≠ 0
⊢ x = y ∧ f x = 1

Tactic:
replace h := (sum_mono_set f (show {x, y} ⊆ s by grind)).trans h
    grind

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

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (mapRange.addMonoidHom ↑f) (g • (x✝¹ + x✝)) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (x✝¹ + x✝)

Tactic:
smul_add,

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (mapRange.addMonoidHom ↑f) (g • x✝¹ + g • x✝) =
    (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (x✝¹ + x✝)
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 α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
⊢ Disjoint (supported M R s) (lmapDomain M R f).ker

Tactic:
rw [disjoint_iff_inf_le]

Goal state after:
α : 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 α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
⊢ supported M R s ⊓ (lmapDomain M R f).ker ≤ ⊥
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n x✝ : ℕ
⊢ x✝ ∈ range val ↔ x✝ ∈ Iio n

Tactic:
simp [Fin.exists_iff]

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ t

Tactic:
refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1
      rw [← Set.ext_iff.mp h x, mem_inter_iff]
      exact ⟨hx, hxf⟩

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

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

Tactic:
refine ⟨fun i ↦ c i, ?_⟩

Goal state after:
case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∑ i, (fun i ↦ c ↑i) i • v ↑i = x
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
w : Set M
x : ↥(span R w)
⊢ (linearCombination R Subtype.val) (repr R w x) = ↑x

Tactic:
rw [Span.repr_def]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : Set M
x : ↥(span R w)
⊢ (linearCombination R Subtype.val) ⋯.choose = ↑x
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ Disjoint {a} s

Tactic:
disjoint_singleton_left

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ a ∉ s
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n a✝ : ℕ
⊢ a✝ ∈ image val univ ↔ a✝ ∈ range n

Tactic:
simp [Fin.exists_iff]

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]

Goal state after:
case hst
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ s ∩ t ⊓ s \ t ⊆ ⊥
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j

Tactic:
by
  have := hI.fintype
  rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]
  exacts [fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2]

Goal state after: