mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s

Tactic:
ext x

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
have : Nonempty S := Sne.to_subtype

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s

Tactic:
ext x

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
by
  refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  let U : NonUnitalSubring R :=
    NonUnitalSubring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup)
      (Subsemigroup.coe_iSup_of_directed hS) (AddSubgroup.coe_iSup_of_directed hS)
  suffices ⨆ i, S i ≤ U by simpa [U] using @this x
  exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
have : Nonempty S := Sne.to_subtype

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
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
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ Submonoid.map f (algebraMapSubmonoid A M) = algebraMapSubmonoid B M

Tactic:
ext x

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ Submonoid.map f (algebraMapSubmonoid A M) ↔ x ∈ algebraMapSubmonoid B M
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
have : Nonempty S := Sne.to_subtype

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
have : Nonempty S := Sne.to_subtype

Goal state after:
R : Type u
inst✝ : NonAssocRing R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p * p ∣ p * p * z

Tactic:
exact dvd_mul_right _ _

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀

Tactic:
ext x

Goal state after:
M₀ : Type u_2
inst✝ : CommMonoidWithZero M₀
x : M₀
⊢ x ∈ nonZeroDivisorsLeft M₀ ↔ x ∈ nonZeroDivisorsRight M₀
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
⊢ ↑(nonZeroDivisorsLeft M₀) = {x | x ≠ 0}

Tactic:
ext x

Goal state after:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsLeft M₀) ↔ x ∈ {x | x ≠ 0}
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
⊢ ↑(nonZeroDivisorsRight M₀) = {x | x ≠ 0}

Tactic:
ext x

Goal state after:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsRight M₀) ↔ x ∈ {x | x ≠ 0}
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case right
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
⊢ ∃ x_1, ¬IsUnit x_1 ∧ a * x = a * x_1

Tactic:
refine ⟨x, ?_, rfl⟩

Goal state after:
case right
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
⊢ ¬IsUnit x
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p m : Associates M
hp : Prime p
hle : m ≤ p
⊢ m = 1 ∨ m = p

Tactic:
by
  rcases mk_surjective p with ⟨p, rfl⟩
  rcases mk_surjective m with ⟨m, rfl⟩
  simpa [mk_eq_mk_iff_associated, Associated.comm]
    using (prime_mk.1 hp).irreducible.dvd_iff.mp (mk_le_mk_iff_dvd.1 hle)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
h : p * b ~ᵤ p
hp : p ≠ 0
⊢ IsUnit b

Tactic:
obtain ⟨a, ha⟩ := h

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ IsUnit b
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
⊢ {x | c.IsClosed x} = range ⇑c

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
x : α
⊢ x ∈ {x | c.IsClosed x} ↔ x ∈ range ⇑c
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ ⋯.closureOperator = c

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ ⋯.closureOperator x = c x
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
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ p x hx

Tactic:
refine AddSubmonoid.closure_induction (motive := fun x hx ↦ p x (key.mpr hx))
    ?_ zero (by simpa only [key] using add) (key.mp hx)

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ ∀ (x : M) (h : x ∈ univ • s), p x ⋯
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 ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid

Tactic:
ext x

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
x : M
⊢ x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
⊢ SupClosed (range ⇑f)

Tactic:
by
  simpa using supClosed_univ.image f

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : PredOrder α
⊢ IsStronglyCoatomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; infer_instance

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ b = sSup {a | IsAtom a ∧ a ≤ b}

Tactic:
refine le_antisymm ?_ (sSup_le fun c hc => hc.2)

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ b ≤ sSup {a | IsAtom a ∧ a ≤ b}
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ}

Tactic:
simp_rw [iInf_iSup_eq, iSup_le_iff]

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ ∀ (i : α → Bool), (⨅ a, b ⊓ bif i a then a else aᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨆ g, ⨅ a, b ⊓ bif g a then a else aᶜ}
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
p p' : Submodule R M
⊢ (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ (p ⊔ p').toAddSubgroup ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ⇑e ⁻¹' Iic b = Iic (e.symm b)

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Iic b ↔ x ∈ Iic (e.symm b)
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ⇑e ⁻¹' Iio b = Iio (e.symm b)

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Iio b ↔ x ∈ Iio (e.symm b)
Module: Mathlib.Order.SupIndep

Goal state before:
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 [Finset.supIndep_map] using! hg

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case mp
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
f : F
⊢ ⇑f = 1 → f = 1

Tactic:
intro h
    simp [DFunLike.ext_iff, h]

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case mp
F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
f : F'
⊢ ⇑f = id → f = 1

Tactic:
intro h
    simp [DFunLike.ext_iff, h]

Goal state after:
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
⊢ sSup s ⊓ a = ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → b ⊓ a = ⊥

Tactic:
h.sSup_inf_eq,

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ⨆ b ∈ s, b ⊓ a = ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → b ⊓ a = ⊥
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case e'_1.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
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f = g → f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype

pp: case e'_1.mpr
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
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype → f = g

Tactic:
· rintro rfl
    rfl

Goal state after:
case e'_1.mpr
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
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype → f = g
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case e'_1.mpr
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
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
h : f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype
⊢ f = g

Tactic:
ext x

Goal state after:
case e'_1.mpr
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
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
h : f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype
x : M
⊢ f x = g x
Module: Mathlib.LinearAlgebra.Span.Basic

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✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
this : ⇑q.subtype '' ↑(inclusion h₁).range = ↑p
⊢ span S (⇑q.subtype '' range ⇑(inclusion h₁)) = q

Tactic:
by
    refine this ▸ le_antisymm ?_ h₂
    simpa using span_mono (R := S) h₁

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

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✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
⊢ ⇑q.subtype '' ↑(inclusion h₁).range = ↑p

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
x : M
⊢ x ∈ ⇑q.subtype '' ↑(inclusion h₁).range ↔ x ∈ ↑p
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
ι : Sort u_8
p : ι → Submodule R M
⊢ (⨆ i, p i).toAddSubmonoid = ⨆ i, (p i).toAddSubmonoid

Tactic:
refine le_antisymm (fun x => ?_) (iSup_le fun i => toAddSubmonoid_mono <| le_iSup _ i)

Goal state after:
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
⊢ x ∈ (⨆ i, p i).toAddSubmonoid → x ∈ ⨆ i, (p i).toAddSubmonoid
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h : ∀ (b : R), b ∈ l → Commute a b
⊢ Commute a l.sum

Tactic:
by
  induction l with
  | nil => exact Commute.zero_right _
  | cons x xs ih =>
    rw [List.sum_cons]
    exact (h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
f : ι → κ → R
a : R
i : ι
l₁ : List ι
j : κ
l₂ : List κ
⊢ (zipWith (fun i j ↦ a * f i j) (i :: l₁) (j :: l₂)).sum = a * (zipWith f (i :: l₁) (j :: l₂)).sum

Tactic:
simp [sum_zipWith_distrib_left, mul_add]

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

Goal state before:
pp: R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
⊢ (s ⊔ t) ⊓ p = s ⊔ t ⊓ p

Tactic:
ext x

Goal state after:
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
⊢ x ∈ (s ⊔ t) ⊓ p ↔ x ∈ s ⊔ t ⊓ p
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ 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:
congr 2 <;> apply prod_congr rfl <;> simpa

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

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

Tactic:
ext x

Goal state after:
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : IsEmpty α
f g : α →₀ M
⊢ f = g

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : IsEmpty α
f g : α →₀ M
x : α
⊢ f x = g x
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : Subsingleton M
f g : α →₀ M
⊢ f = g

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : Subsingleton M
f g : α →₀ M
x : α
⊢ f x = g x
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ (a : α), a ∈ onFinsetSupport s f ↔ f a ≠ 0

Tactic:
simpa [onFinsetSupport]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
e : R
h : e * e = e
x✝ : R
⊢ x✝ * (e * e) = x✝ * e

Tactic:
by rw [h]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, (1 + f i) = 1 + ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j)

Tactic:
by
  rw [prod_add_ordered]
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ (single a b) a' = 0

Tactic:
exact Pi.single_eq_of_ne' h _

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 : α
h : f.support ⊆ {a}
⊢ f = single a (f a)

Tactic:
ext x

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
⊢ f x = (single a (f a)) x
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:
by
  classical
  have H := support_single a hb
  rw [support_add_eq, H, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_left]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
⊢ AddCommute f g

Tactic:
ext x

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
⊢ (f + g) x = (g + f) x
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
⊢ (f + g) x = (g + f) x

Tactic:
by_cases hf : x ∈ f.support

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
hf : x ∈ f.support
⊢ (f + g) x = (g + f) x

case neg
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
hf : x ∉ f.support
⊢ (f + g) x = (g + f) x
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)
⊢ ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)

Tactic:
convert! add_single using 7

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)
a✝⁵ : ι
a✝⁴ : M
a✝³ : ι →₀ M
a✝² : a✝⁵ ∉ a✝³.support
a✝¹ : a✝⁴ ≠ 0
a✝ : motive a✝³
⊢ single a✝⁵ a✝⁴ + a✝³ = a✝³ + single a✝⁵ a✝⁴
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
⊢ optionElim (i + j) (a + b) = optionElim i a + optionElim j b

Tactic:
ext x

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
x : Option α
⊢ (optionElim (i + j) (a + b)) x = (optionElim i a + optionElim j b) x
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
simpa [sub_eq_add_neg, add_assoc] using abv.add_le (a - b) (b - c)

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

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
simp [l.le_prod_of_submultiplicative f h_one h_mul]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
l : α →₀ M
⊢ equivMapDomain (Equiv.refl α) l = l

Tactic:
ext x

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
l : α →₀ M
x : α
⊢ (equivMapDomain (Equiv.refl α) l) x = l x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
⊢ equivMapDomain (Equiv.refl α) = id

Tactic:
ext x

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α →₀ M
a✝ : α
⊢ (equivMapDomain (Equiv.refl α) x) a✝ = (id x) a✝