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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints (↥H) α
h : ↥H
⊢ h • g • a = g • a

Tactic:
rw [Subgroup.smul_def, ← inv_smul_eq_iff, smul_smul, smul_smul]

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints (↥H) α
h : ↥H
⊢ (g⁻¹ * ↑h * g) • a = a
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
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₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
x : M
hx : x ∈ f.ker
⊢ x ∈ comap f p

Tactic:
simp [mem_ker.mp hx]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.ker = ⊥ ↔ Injective ⇑f

Tactic:
simpa [disjoint_iff_inf_le] using disjoint_ker_iff_injOn (f := f) (p := ⊤)

Goal state after:
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₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x : ↥(map f p)
⊢ f ↑((equivMapOfInjective f i p).symm ((equivMapOfInjective f i p) ((equivMapOfInjective f i p).symm x))) =
    ↑((equivMapOfInjective f i p) ((equivMapOfInjective f i p).symm x))

Tactic:
coe_equivMapOfInjective_apply,

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₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x : ↥(map f p)
⊢ f ↑((equivMapOfInjective f i p).symm ((equivMapOfInjective f i p) ((equivMapOfInjective f i p).symm x))) =
    f ↑((equivMapOfInjective f i p).symm x)
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y : R
hx : -x ∈ s
hy : y ∈ s
⊢ -(x * y) ∈ s

Tactic:
by
  simpa using mul_mem hx hy

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y : R
hx : x ∈ s
hy : -y ∈ s
⊢ -(x * y) ∈ s

Tactic:
by
  simpa using mul_mem hx hy

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
s : Set M₀
⊢ 0 ∈ s.centralizer

Tactic:
by simp [mem_centralizer_iff]

Goal state after:
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:
ext <;> exact left_distrib ..

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

Goal state before:
pp: case mem.mul
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ * y✝) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: case mem.mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ * y✝) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂

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

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

Tactic:
clear _hx _hy

Goal state after:
case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mem.mul
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ * y✝) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: case mem.mul
R : Type u
inst✝ : NonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ * y✝) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂

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

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

Tactic:
clear _hx _hy

Goal state after:
case mul
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ y✝ : R
hx : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
n : ℕ
hp : Prime (p ^ n)
⊢ n = 1

Tactic:
grind [not_prime_pow, Nat.zero_eq_one_mod_iff]

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
x : R
hx : f x ∈ map f s
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
mem_map

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : ∃ x_1 ∈ s, f x_1 = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
p : Submodule R M
q : Submodule R₂ M₂
h : ∀ x ∈ p, f x ∈ q
⊢ (f.restrict h).range = comap q.subtype (map f p)

Tactic:
← Submodule.map_top,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
p : Submodule R M
q : Submodule R₂ M₂
h : ∀ x ∈ p, f x ∈ q
⊢ map (f.restrict h) ⊤ = comap q.subtype (map f p)
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
p p' : Submodule R M
P : M → Prop
⊢ (∀ x ∈ p ⊔ p', P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)

Tactic:
simp [mem_sup]
  aesop

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h✝ : Nonempty ι
⊢ ⨆ i, f i ∈ s

Tactic:
exact hs.iSup_mem_of_nonempty hf

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

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ range s
ht' : k ≤ t.sup id
⊢ ∃ t, k ≤ t.sup s

Tactic:
have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop

Goal state after:
case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ range s
ht' : k ≤ t.sup id
this : ∀ (x : ↥t), ∃ i, s i = ↑x
⊢ ∃ t, k ≤ t.sup s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
⊢ sSup s < k

Tactic:
by_contra h

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬sSup s < k
⊢ False
Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ IsSquare (∏ i ∈ s, f i)

Tactic:
by
  rw [isSquare_iff_exists_sq]
  use (∏ (x : s), ((isSquare_iff_exists_sq _).mp (h _ x.2)).choose)
  rw [@sq, ← Finset.prod_mul_distrib, ← Finset.prod_coe_sort]
  congr
  ext i
  rw [← @sq]
  exact ((isSquare_iff_exists_sq _).mp (h _ i.2)).choose_spec

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite

Tactic:
exact WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
T : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : S
a : Set S
hx : x ∈ span R a
⊢ (algebraMap S T) x ∈ map (↑R (Algebra.linearMap S T)) (span R a)

Tactic:
mem_map

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
T : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : S
a : Set S
hx : x ∈ span R a
⊢ ∃ y ∈ span R a, (↑R (Algebra.linearMap S T)) y = (algebraMap S T) x
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case refine_4.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ ∀ x ∈ ⋃ i, ↑(p i), r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
rintro x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩
      apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)
      exact smul_mem _ r hix

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : WellFoundedGT α
⊢ IsCompactlyGenerated α

Tactic:
wellFoundedGT_iff_isSupFiniteCompact,

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
⊢ IsCompactlyGenerated α
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
⊢ ∀ (b : ↑(Iic k)), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
rintro ⟨b, hbk⟩

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
⊢ ⟨b, hbk⟩ = ⊤ ∨ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ l.prod = 0 ↔ 0 ∈ ↑l

Tactic:
exact List.prod_eq_zero_iff

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.powerset, (fun a_1 x ↦ a_1 ∈ a) ∈ s.pi fun x ↦ {True, False}

Tactic:
simp [Classical.em]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x ↦ {True, False}
⊢ (∏ a_1 ∈ s.attach, if a ↑a_1 ⋯ then f ↑a_1 else g ↑a_1) =
    (∏ a ∈ s with ∃ (h : a ∈ s), a a h, f a) * ∏ a ∈ s \ {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h}, g a

Tactic:
simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
            Subtype.map_coe, id_eq, prod_attach]
          congr 2 with x
          simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
          tauto

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ (Function.support ⇑f).Finite

Tactic:
exact f.fun_support_eq.symm ▸ f.support.finite_toSet

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 → α
i : ι
hi : (indicator s f) i ≠ 0
⊢ i ∈ s

Tactic:
by_contra h

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : (indicator s f) i ≠ 0
h : i ∉ s
⊢ False
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
this : (optionElim y f) none = 0 none
⊢ y = 0

Tactic:
simp only [optionElim_apply_eq_elim, Option.elim_none, coe_zero, Pi.zero_apply] at this

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
this : y = 0
⊢ y = 0
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid 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✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
suffices ∀ y, f y = 0 by rw [this, this, smul_zero]
    clear x
    intro x
    rw [← inv_smul_smul₀ hS (f x), ← map_natCast_smul f R S]
    simp [hR, map_zero f]

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

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ (embDomain f v).prod g = v.prod fun a b ↦ g (f a) b

Tactic:
rw [prod, prod, support_embDomain, Finset.prod_map]
  simp_rw [embDomain_apply_self]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
⊢ max (map f s).prod (map g s).prod ≤ (map (fun i ↦ max (f i) (g i)) s).prod

Tactic:
obtain ⟨l⟩ := s
  simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  apply List.max_prod_le

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 M
f : α ≃ β
⊢ (α →₀ M) ≃ (β →₀ M)

Tactic:
refine ⟨equivMapDomain f, equivMapDomain f.symm, fun f => ?_, fun f => ?_⟩

Goal state after:
case refine_1
α : 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 M
f✝ : α ≃ β
f : α →₀ M
⊢ equivMapDomain f✝.symm (equivMapDomain f✝ f) = f

case refine_2
α : 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 M
f✝ : α ≃ β
f : β →₀ M
⊢ equivMapDomain f✝ (equivMapDomain f✝.symm f) = f
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ (∀ (a : α), a ∈ l.support.preimage f ⋯ ↔ a ∈ ∅) → ∀ (a : β), a ∈ l.support ↔ a ∈ ∅

Tactic:
Finset.notMem_empty,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ (∀ (a : α), a ∈ l.support.preimage f ⋯ ↔ False) → ∀ (a : β), a ∈ l.support ↔ False
Module: Mathlib.Data.Finsupp.Basic

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

Tactic:
embDomain_apply_self,

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
a : α
⊢ (comapDomain (⇑f) g ⋯) a = g (f a)
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 M
p✝ p : α → Prop
f : α →₀ M
a : Subtype p
⊢ a ∈ Finset.subtype p f.support ↔ (⇑f ∘ Subtype.val) a ≠ 0

Tactic:
by simp only [@mem_subtype _ _ (Classical.decPred p), mem_support_iff]; rfl

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:
by
  simp [Finsupp.sum, Finsupp.uncurry, Finset.sum_disjiUnion]

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, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) =
    (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * ((∑ i ∈ s, f i) * ∑ i ∈ s, g i)

Tactic:
by simp_rw [sum_add_distrib, ← sum_mul]; ring

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 α
⊢ supported M R (⋃ i, s i) = ⨆ i, supported M R (s i)

Tactic:
refine le_antisymm ?_ (iSup_le fun i => supported_mono <| Set.subset_iUnion _ _)

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
s : δ → Set α
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
this : (mulSupport fun x ↦ (fun x ↦ 1) x.down) ⊆ ↑∅
⊢ ∏ i ∈ ∅, 1 = 1

Tactic:
Finset.prod_empty

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
this : (mulSupport fun x ↦ (fun x ↦ 1) x.down) ⊆ ↑∅
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case neg
α : 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
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
xs : x ∉ s
⊢ l x = 0 x

Tactic:
by_contra h

Goal state after:
case neg
α : 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
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
xs : x ∉ s
h : ¬l x = 0 x
⊢ False