mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
f g : M →ₛₗ[σ] M₃
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f
    cases g
    congr
    apply DFunLike.coe_injective
    exact h

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝³ : DistribSMul S M₂
inst✝² : SMulCommClass R₂ S M₂
inst✝¹ : DistribSMul T M₂
inst✝ : SMulCommClass R₂ T M₂
a : S
f : M →ₛₗ[σ₁₂] M₂
c : R
x : M
⊢ (a • ⇑f) (c • x) = σ₁₂ c • (a • ⇑f) x

Tactic:
by simp [Pi.smul_apply, smul_comm]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R M
inst✝⁶ : Module R M₁
inst✝⁵ : Semiring S
inst✝⁴ : Module R S
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : IsDomain S
f : M₁ →ₗ[R] S
x : M
inst✝ : Module.IsTorsionFree S M
⊢ f.smulRight x = 0 ↔ f = 0 ∨ x = 0

Tactic:
by simp [DFunLike.ext_iff, forall_or_right]

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ ∀ {a b : M}, a ∈ ⋂ s ∈ S, ↑s → b ∈ ⋂ s ∈ S, ↑s → a + b ∈ ⋂ s ∈ S, ↑s

Tactic:
by simp +contextual [add_mem]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ ∀ {a b : M}, a ∈ ↑p ∩ ↑q → b ∈ ↑p ∩ ↑q → a + b ∈ ↑p ∩ ↑q

Tactic:
by simp +contextual [add_mem]

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₂
S : Submodule R M
⊢ Injective ⇑(f.domRestrict S) ↔ Disjoint S f.ker

Tactic:
simp [← ker_eq_bot, ker_domRestrict, disjoint_iff_comap_eq_bot]

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

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
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x✝ y✝ : ↥p
⊢ (Equiv.Set.image (⇑f) (↑p) i).toFun (x✝ + y✝) =
    (Equiv.Set.image (⇑f) (↑p) i).toFun x✝ + (Equiv.Set.image (⇑f) (↑p) i).toFun y✝

Tactic:
simp only [coe_add, map_add, Equiv.toFun_as_coe, Equiv.Set.image_apply]

Goal state after:
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
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x✝ y✝ : ↥p
⊢ ⟨f ↑x✝ + f ↑y✝, ⋯⟩ = ⟨f ↑x✝, ⋯⟩ + ⟨f ↑y✝, ⋯⟩
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 p ⊓ map f q = ⊥

Tactic:
← map_inf f hf,

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
⊢ map f (p ⊓ q) = ⊥
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✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ p ≤ comap (c • f) (map f p)

Tactic:
← comap_le_comap_smul (map f p) f c,

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ p ≤ comap f (map f p)
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 σ₁₂
p : Submodule R M
f : M →ₛₗ[σ₁₂] M₂
hf : InjOn ⇑f ↑p
x : M
hx : x ∈ p
y : M
hy : y ∈ p
hxy : (f.submoduleMap p) ⟨x, hx⟩ = (f.submoduleMap p) ⟨y, hy⟩
⊢ f x = f y

Tactic:
simpa [Subtype.ext_iff] using hxy

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
a : A
m : M
⊢ (a * (algebraMap R A) r) • m = a • r • m

Tactic:
mul_smul,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
a : A
m : M
⊢ a • (algebraMap R A) r • m = a • r • m
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
a : A
m : M
⊢ r • a • m = a • r • m

Tactic:
by
    rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ←
      algebra_compatible_smul]

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

Goal state before:
pp: case mpr
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 ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)

Tactic:
· rintro ⟨r, hr, rfl⟩
    simp only [Submonoid.mem_map]
    use (algebraMap R A r)
    simp only [AlgHom.commutes, and_true]
    use r

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

Goal state before:
pp: R : Type u
inst✝¹ : NonAssocSemiring R
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Subsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    Subsemigroup.coe_iSup_of_directed dir] using! Subsemigroup.isMulCommutative_iSup dir

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

Goal state before:
pp: case mem.one
R : Type u
inst✝ : NonAssocRing R
s : Set R
x✝ x : R
⊢ 1 ∈ closure s

Tactic:
exact one_mem _

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

Goal state before:
pp: R : Type u
inst✝¹ : NonAssocRing R
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Subring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    Subsemigroup.coe_iSup_of_directed dir] using! Subsemigroup.isMulCommutative_iSup dir

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
x : M₀
⊢ x ∉ nonZeroDivisorsRight M₀ ↔ {y | y * x = 0 ∧ y ≠ 0}.Nonempty

Tactic:
by
  simpa [mem_nonZeroDivisorsRight_iff] using! Set.nonempty_def.symm

Goal state after:
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₂
⊢ f.range ≤ ⊥ ↔ f = 0

Tactic:
rw [range_le_iff_comap]

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₂
⊢ comap f ⊥ = ⊤ ↔ f = 0
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b : α
ha : IsAtom a
⊢ ¬Disjoint a b ↔ a ≤ b

Tactic:
by
  rw [disjoint_iff, ← inf_eq_left]; exact ha.ne_bot_iff_eq inf_le_left

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α

Tactic:
by
  simpa [isStronglyAtomic_iff, OrderDual.exists, OrderDual.forall,
    OrderDual.toDual_le_toDual, and_comm, isStronglyCoatomic_iff] using forall_comm

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
x y : M
⊢ (∃ a, a • y = x) → x ∈ R ∙ y

Tactic:
rintro ⟨a, y, rfl⟩; exact smul_mem _ _ (subset_span <| by simp)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
by
    rcases isLUB_atoms b with ⟨s, hsb, hs⟩
    rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
    · simp_all
    · exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

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

Goal state before:
pp: case neg
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}
m : M
hm : m ∈ p
h : ¬m = 0
⊢ m ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

Tactic:
· exact @le_sSup _ _ S _ ⟨m, ⟨hm, ⟨h, rfl⟩⟩⟩ m (mem_span_singleton_self m)

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
p : ι → Submodule R M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← span_singleton_le_iff_mem, le_iSup_iff]
  simp only [span_singleton_le_iff_mem]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1.hu
α : 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) := ⋯
v : Finset ((x : ι) × β x) := ⋯
⊢ u ⊆ s.sigma g

Tactic:
grind [disjoint_left]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1.hv
α : 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) := ⋯
v : Finset ((x : ι) × β x) := ⋯
⊢ v ⊆ s.sigma g

Tactic:
grind [disjoint_left]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1.huv
α : 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) := ⋯
v : Finset ((x : ι) × β x) := ⋯
⊢ Disjoint u v

Tactic:
grind [disjoint_left]

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le] at hk

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i
Module: Mathlib.Order.CompactlyGenerated.Basic

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

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le] at hk

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
⊢ sSup s < k
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
A : Type w
M : Type v₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : MulAction A M
inst✝ : SMul R M
h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x
r : R
a : A
x : M
⊢ ((algebraMap R A) r * a) • x = r • a • x

Tactic:
mul_smul,

Goal state after:
R : Type u
A : Type w
M : Type v₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : MulAction A M
inst✝ : SMul R M
h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x
r : R
a : A
x : M
⊢ (algebraMap R A) r • a • x = r • a • x
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ t.mulIndicator 1 ⁻¹' s ∈ {univ, ∅}

Tactic:
by
  classical
  rw [mulIndicator_one', Pi.one_def, Set.preimage_const]
  split_ifs <;> simp

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
h' : a ⊓ sSup (insert a ↑t \ {a}) = ⊥
⊢ a ∉ ↑t

Tactic:
exact fun con => ((Set.mem_sdiff a).1 (ht con)).2 (Set.mem_singleton a)

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
ι : Sort u_8
p : ι → Submodule R M
x : M
⊢ x ∈ (⨆ i, p i).toAddSubmonoid → x ∈ ⨆ i, (p i).toAddSubmonoid

Tactic:
simp_rw [iSup_eq_span, AddSubmonoid.iSup_eq_closure, mem_toAddSubmonoid, coe_toAddSubmonoid]

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 ∈ span R (⋃ i, ↑(p i)) → x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ ψ : ((i : ι) → M i) →* M'
⊢ (fun i ↦ (φ * ψ).comp (MonoidHom.mulSingle M i)) =
    (fun i ↦ φ.comp (MonoidHom.mulSingle M i)) * fun i ↦ ψ.comp (MonoidHom.mulSingle M i)

Tactic:
ext
    simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.mul_apply, mul_apply]

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
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
this : x ∈ sSup d
y : Submodule R M
hyd : y ∈ d
hxy : x ∈ y
⊢ R ∙ x ≤ y

Tactic:
simpa only [span_le, singleton_subset_iff]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
⊢ (f * g) x = f x

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
⊢ f x * g x = f x
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ (f * g) x = g x

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ f x * g x = g x
Module: Mathlib.Algebra.Group.Indicator

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

Tactic:
Pi.mul_apply,

Goal state after:
case pos
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : x ∈ s
⊢ s.mulIndicator f x * sᶜ.mulIndicator g x = f x
Module: Mathlib.Algebra.Group.Indicator

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

Tactic:
Pi.mul_apply,

Goal state after:
case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ s.mulIndicator f x * sᶜ.mulIndicator g x = g x
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
q : Submodule R₂ M₂
le : comap f q ≤ p
⊢ comap f (map f p ⊔ q) = p

Tactic:
refine le_antisymm (fun x h ↦ ?_) (map_le_iff_le_comap.mp le_sup_left)
  obtain ⟨_, ⟨y, hy, rfl⟩, z, hz, eq⟩ := mem_sup.mp h
  rw [add_comm, ← eq_sub_iff_add_eq, ← map_sub] at eq; subst eq
  simpa using p.add_mem (le hz) hy

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),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h ∈ {True, False}) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1

Tactic:
mem_insert

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ a a_1 h ∈ {False}) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
Module: Mathlib.Algebra.BigOperators.Ring.Finset

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

Tactic:
simp only [sub_eq_add_neg]
  convert! prod_add_ordered s f fun i => -g i
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ ∃ x, l = single x b ∧ f x = a

Tactic:
have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]
    have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
    rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
    use c
    constructor
    · ext d
      rw [← embDomain_apply_self f l, h]
      grind
    · exact hc₂

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ (single (Option.some a) m).some = single a m

Tactic:
ext b
    simp [single_apply]

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
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ ∀ x ∈ f.support.erase y, g x ((erase y f) x) = g x (f x)

Tactic:
intro h hx

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
h : α
hx : h ∈ f.support.erase y
⊢ g h ((erase y f) h) = g h (f h)
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case pos
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 : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
x : M
⊢ f x = 0

Tactic:
← smul_inv_smul₀ hR x,

Goal state after:
case pos
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 : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
x : M
⊢ f (↑n • (↑n)⁻¹ • x) = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' ↑x.support
⊢ (mapDomain f x) b = 0

Tactic:
by
  rw [mapDomain, sum_apply, sum, Finset.sum_eq_zero]
  exact fun a ha ↦ single_eq_of_ne fun eq => hb <| eq ▸ Set.mem_image_of_mem _ ha

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ (Multiset.map g (Multiset.map (fun x ↦ f x) s.val)).sum = ∑ x ∈ s, g (f x)

Tactic:
rw [Multiset.map_map, Function.comp_def, Finset.sum_map_val]

Goal state after: