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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
LE.le

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : instPartialOrder.toLE.1 S (S ⊔ T)
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
LE.le

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : instPartialOrder.toLE.1 T (S ⊔ T)
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
LE.le

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : completeLattice.toCompleteSemilatticeSup.toLE.1 s (sSup S)
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ ∀ x ∈ center G₀ˣ, x ∈ Units.val ⁻¹' center G₀

Tactic:
mem_preimage,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ ∀ x ∈ center G₀ˣ, ↑x ∈ center G₀
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case pos
M : Type u_2
inst✝ : Mul M
p : Prop
S : p → Subsemigroup M
x : M
h : p
⊢ x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h

Tactic:
simp +contextual [h]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ f ((algebraMap R A) r * a) = (algebraMap R B) r * f a

Tactic:
by
  rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]

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

Goal state before:
pp: case mul.neg_left
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ -x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa [neg_mul] using neg_mem h

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : A →ₐ[R] A
n x✝ : ℕ
ih : ⇑(φ ^ x✝) = (⇑φ)^[x✝]
⊢ ⇑(φ ^ x✝.succ) = (⇑φ)^[x✝.succ]

Tactic:
ext; simp [pow_succ, ih]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s t : Subsemiring R
g : S → R
f : R →+* S
h : Function.LeftInverse g ⇑f
x : ↥f.rangeS
⊢ ↑((fun x ↦ f.rangeSRestrict x) ((fun x ↦ (g ∘ ⇑f.rangeS.subtype) x) x)) = ↑x

Tactic:
let ⟨x', hx'⟩ := RingHom.mem_rangeS.mp x.prop

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s t : Subsemiring R
g : S → R
f : R →+* S
h : Function.LeftInverse g ⇑f
x : ↥f.rangeS
x' : R
hx' : f x' = ↑x
⊢ ↑((fun x ↦ f.rangeSRestrict x) ((fun x ↦ (g ∘ ⇑f.rangeS.subtype) x) x)) = ↑x
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.neg_left
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ -x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simpa [neg_mul] using neg_mem h

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
⊢ ¬IsUnit y → ((∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)

Tactic:
refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩

Goal state after:
case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B

case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : ↑u * y = A * B
⊢ IsUnit A ∨ IsUnit B
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
⊢ ¬IsUnit y → ((∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)

Tactic:
refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩

Goal state after:
case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B

case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ IsUnit A ∨ IsUnit B
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : a ∣ b
c : ↥M₀⁰
hc : b = a * c
⊢ ↑a ∣ ↑b

Tactic:
simp_rw [hc, Submonoid.coe_mul, dvd_mul_right]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : s ≠ 0 ∧ t ≠ 0
hst : (s * t).Nonempty
⊢ False

Tactic:
rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne, ← hst.of_smul_right.subset_zero_iff] at H

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : ¬s ⊆ 0 ∧ ¬t ⊆ 0
hst : (s * t).Nonempty
⊢ False
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
inst✝² : CommSemiring R
inst✝¹ : Semiring A₁
inst✝ : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n x✝ : ℕ
ih : ⇑(e ^ x✝) = (⇑e)^[x✝]
⊢ ⇑(e ^ x✝.succ) = (⇑e)^[x✝.succ]

Tactic:
ext; simp [pow_succ, ih]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
x₁ x₂ : M₁
y : M₂
⊢ (↑e ∘ₗ codRestrict i.range (f (x₁ + x₂)) ⋯) y =
    (↑e ∘ₗ codRestrict i.range (f x₁) ⋯ + ↑e ∘ₗ codRestrict i.range (f x₂) ⋯) y

Tactic:
simp [f.map_add, ← e.map_add, codRestrict]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : SetLike S M
inst✝¹ : AddSubmonoidClass S M
inst✝ : SMulMemClass S R M
s : S
⊢ ↑(span R ↑s) = ↑s

Tactic:
by
  refine le_antisymm ?_ subset_span
  let s' : Submodule R M :=
    { carrier := s
      add_mem' := add_mem
      zero_mem' := zero_mem _
      smul_mem' := SMulMemClass.smul_mem }
  exact span_le (p := s') |>.mpr le_rfl

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
⊢ span R (insert 0 s) = span R s

Tactic:
by
  refine le_antisymm ?_ (Submodule.span_mono (Set.subset_insert 0 s))
  rw [span_le, Set.insert_subset_iff]
  exact ⟨by simp only [SetLike.mem_coe, Submodule.zero_mem], Submodule.subset_span⟩

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
⊢ b ⊔ (d ⊔ a) ⊓ c = c

Tactic:
simp [← sup_inf_assoc_of_le _ hc, ← sup_assoc, hcodisjoint.eq_top]

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 (Set M)
⊢ ⋃₀ s ⊆ ↑(sSup (span R '' s))

Tactic:
exact fun x ⟨t, hts, hxt⟩ ↦ le_sSup (mem_image_of_mem (span R) hts) (subset_span hxt)

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
⊢ ∃ a', a ≤ a' ∧ IsCompl a' b

Tactic:
by
  obtain ⟨u, hu⟩ := ComplementedLattice.exists_isCompl (a ⊔ b)
  exact ⟨u ⊔ a, le_sup_right, hab.isCompl_sup_left_of_isCompl_sup_right hu.symm⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
by
  rw [← sSup_image]
  exact hs.sSup_mem_of_nonempty (ht.image _) (by simpa) (by simpa)

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ span R (range (update v j (v j - r • v i))) = span R (range v)

Tactic:
by
  rw [sub_eq_add_neg, ← neg_smul, span_range_update_add_smul hij]

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
⊢ b ∉ a → Disjoint (f b) (a.sup f)

Tactic:
hab

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
⊢ Disjoint (f b) (a.sup f)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : 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)
this : Disjoint (u.sup f) (v.sup f)
⊢ 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:
simpa only [sup_map, sup_biUnion, u, v]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inr
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))

Tactic:
convert! h.symm using 1
      simp [hab, sSup_singleton]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ sSupIndep s ↔ iSupIndep Subtype.val

Tactic:
simp_rw [iSupIndep, sSupIndep, SetCoe.forall, sSup_eq_iSup]
  refine forall₂_congr fun a ha => ?_
  simp [iSup_subtype, iSup_and]

Goal state after:
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.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ sSup '' c → Disjoint b b_1

Tactic:
rintro _ ⟨s, hs, rfl⟩
      exact (hc1 hs).2.1

Goal state after:
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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ comap f (map f q ⊔ p) = ⊤

Tactic:
hp.2 (map f q ⊔ p),

Goal state after:
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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ comap f ⊤ = ⊤

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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ p < map f q ⊔ p
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: κ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
⊢ (∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i ↦ s, ∏ i, f (p i)

Tactic:
convert! @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d

Goal state after:
κ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
⊢ (∑ a ∈ s, f a) ^ n = ∏ i, ∑ j ∈ s, f j
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
N : Submodule R M
x : M
hx : x ∈ N
⊢ (R ∙ x).submoduleOf N = R ∙ ⟨x, hx⟩

Tactic:
by
  ext y
  simp_rw [submoduleOf, mem_comap, subtype_apply, mem_span_singleton]
  aesop

Goal state after:
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
⊢ (single a b + f).support = cons a f.support ha

Tactic:
have H := support_single a hb

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}
⊢ (single a b + f).support = cons a f.support ha
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
⊢ (f + single a b).support = cons a f.support ha

Tactic:
have H := support_single a hb

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}
⊢ (f + single a b).support = cons a f.support ha
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∉ s
⊢ s.mulIndicator f a ≤ y

Tactic:
· simpa [ha] using hg ha

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
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
⊢ f.prod g = ∏ x ∈ s, g x (f x)

Tactic:
refine Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)
  exact notMem_support_iff.1 hx

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✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = (Multiset.map (fun g ↦ g.sum h) s).sum
⊢ (a ::ₘ s).sum.sum h = (Multiset.map (fun g ↦ g.sum h) (a ::ₘ s)).sum

Tactic:
rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]

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

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

Tactic:
classical
  refine Finset.induction_on s ?_ ?_
  · simp
  · intro i s hi
    simp only [hi, sum_insert, not_false_iff, biUnion_insert]
    intro hs
    rw [Finsupp.support_add_eq, hs]
    rw [hs, Finset.disjoint_biUnion_right]
    intro j hj
    exact h _ _ (ne_of_mem_of_not_mem hj hi).symm

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

Goal state before:
pp: α : 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
⊢ (mapDomain f x) (f a) = x a

Tactic:
classical
    rw [mapDomain, sum_apply, sum]
    simp_rw [single_apply]
    by_cases hax : a ∈ x.support
    · 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)
    · rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)

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✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

Tactic:
mapDomain_of_notMem_range,

Goal state after:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = 0

case neg.h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ a ∉ Set.range ⇑f
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
y : M
⊢ y ∈ f.frange ↔ y ≠ 0 ∧ y ∈ Set.range ⇑f

Tactic:
by
  rw [frange, @Finset.mem_image _ _ (Classical.decEq _) _ f.support]
  exact ⟨fun ⟨x, hx1, hx2⟩ => ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩, fun ⟨hy, x, hx⟩ =>
    ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩

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 ≤ f i * ∏ i ∈ s \ {i}, f i

Tactic:
grw [← h2i, right_distrib]

Goal state after:
ι : 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
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Surjective ⇑(ringHomEndFinsupp ι)

Tactic:
by
  intro f
  obtain _ | ⟨⟨i⟩⟩ := isEmpty_or_nonempty ι
  · exact ⟨0, Subsingleton.elim ..⟩
  · exact ⟨_, (ringEquivEndFinsupp i).right_inv f⟩

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
⊢ ∏ᶠ (x : α), 1 = 1

Tactic:
by
  have : (mulSupport fun x : PLift α => (fun _ => 1 : α → M) x.down) ⊆ (∅ : Finset (PLift α)) :=
    fun x h => by simp at h
  rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty]

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

Goal state before:
pp: M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ᶠ (x : α), g x) = ∏ᶠ (x : α), f (g x)

Tactic:
finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge,

Goal state after:
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ i ∈ Finite.toFinset h, g i.down) = ∏ᶠ (x : α), f (g 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:
by
  rw [disjoint_iff_inf_le]
  rintro l ⟨h₁, h₂⟩
  rw [SetLike.mem_coe, mem_ker, lmapDomain_apply, mapDomain] at h₂
  simp only [mem_bot]; ext x
  have := Classical.decPred fun x => x ∈ s
  by_cases xs : x ∈ s
  · have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 := by
      rw [h₂]
      rfl
    rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this
    · simpa
    · intro y hy xy
      simp only [SetLike.mem_coe, mem_supported, subset_def, mem_support_iff] at h₁
      simp [mt (H _ (h₁ _ hy) _ xs) xy]
    · simp +contextual
  · by_contra h
    exact xs (h₁ <| Finsupp.mem_support_iff.2 h)

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 : Set α
h : ∀ x ∈ s, f x = 1
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1

Tactic:
simp +contextual [h]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
h : ∀ (x : α), f x = 1
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
simp +contextual [h]

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

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

Tactic:
← preimage_addNat_Ici_addNat,

Goal state after:
n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Ici (i.addNat ?m) = Ici (i.addNat m)

case m
n m : ℕ
i : Fin n
⊢ ℕ
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∀ i ∈ hf.toFinset, 1 ≤ f i

Tactic:
simp +contextual [h]

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
l : M →₀ R
hl : l ∈ supported R R s
⊢ ↑l.support ⊆ _root_.id '' s ∧
    Function.support ⇑l ⊆ ↑l.support ∧ ∑ a ∈ l.support, l a • a = (linearCombination R _root_.id) l

Tactic:
simpa [linearCombination, Finsupp.sum] using! hl

Goal state after: