mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Atoms

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

Tactic:
simpa using

Goal state after:
α : Type u_4
inst✝ : Preorder α
⊢ (∀ (a a_1 : α), a_1 < a → ∃ a_3, a_3 ⋖ a ∧ a_1 ≤ a_3) ↔ ∀ (a b : α), a < b → ∃ x, x ⋖ b ∧ a ≤ x
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
hbot : ¬x ⊓ yᶜ = ⊥
a : α
ha : IsAtom a
hle : a ≤ x ⊓ yᶜ
hx : a ≤ x
hy' : a ≤ yᶜ
hy : a ≤ y
this : a ≤ y ⊓ yᶜ
⊢ a = ⊥

Tactic:
simpa using

Goal state after:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
hbot : ¬x ⊓ yᶜ = ⊥
a : α
ha : IsAtom a
hle : a ≤ x ⊓ yᶜ
hx : a ≤ x
hy' : a ≤ yᶜ
hy : a ≤ y
this : a ≤ y ⊓ yᶜ
⊢ a = ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : IsAtomistic α
inst✝ : OrderTop α
⊢ IsLUB {a | IsAtom a} ⊤

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : IsAtomistic α
inst✝ : OrderTop α
⊢ IsLUB {a | IsAtom a} ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
b : α
hbS : b ∈ S
x✝ : ⊥ ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : ⊥ ≤ sSup S
hatom : IsAtom ⊥
hba : ⊥ ≤ b
⊢ ⊥ ∈ S

Tactic:
simpa using

Goal state after:
case inl
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
b : α
hbS : b ∈ S
x✝ : ⊥ ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : ⊥ ≤ sSup S
hatom : IsAtom ⊥
hba : ⊥ ≤ b
⊢ ⊥ ∈ S
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
a b : α
⊢ { toFun := fun A ↦ {a | ↑a ≤ A}, invFun := fun S ↦ sSup (Subtype.val '' S), left_inv := ⋯, right_inv := ⋯ } a ⊆
      { toFun := fun A ↦ {a | ↑a ≤ A}, invFun := fun S ↦ sSup (Subtype.val '' S), left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b

Tactic:
simpa using

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
a b : α
⊢ (∀ (a_1 : α), IsAtom a_1 → a_1 ≤ a → a_1 ≤ b) ↔ a ≤ b
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b : α
ha : a ∈ f ⁻¹' latticeClosure (f '' s)
hb : b ∈ f ⁻¹' latticeClosure (f '' s)
⊢ a ⊔ b ∈ f ⁻¹' latticeClosure (f '' s)

Tactic:
simpa using

Goal state after:
case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b : α
ha : a ∈ f ⁻¹' latticeClosure (f '' s)
hb : b ∈ f ⁻¹' latticeClosure (f '' s)
⊢ f a ⊔ f b ∈ latticeClosure (f '' s)
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊥
⊢ ⊥ ≠ ⊤

Tactic:
simpa using

Goal state after:
case inl.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊥
⊢ ¬⊥ = ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊥
⊢ ⊥ ≠ ⊤

Tactic:
simpa using

Goal state after:
case inr.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊥
⊢ ¬⊥ = ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤

Tactic:
simpa using

Goal state after:
case inr.inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ¬⊥ = ⊤
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case left.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b : α
ha : a ∈ f ⁻¹' latticeClosure (f '' s)
hb : b ∈ f ⁻¹' latticeClosure (f '' s)
⊢ a ⊓ b ∈ f ⁻¹' latticeClosure (f '' s)

Tactic:
simpa using

Goal state after:
case left.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b : α
ha : a ∈ f ⁻¹' latticeClosure (f '' s)
hb : b ∈ f ⁻¹' latticeClosure (f '' s)
⊢ f a ⊓ f b ∈ latticeClosure (f '' s)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective ⇑f
inst✝ : IsPrincipal R M
m : M
hm : ⊤ = R ∙ m
r : R
x✝ : f (r • m) ∈ ⊤
⊢ f (r • m) ∈ R ∙ f m

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective ⇑f
inst✝ : IsPrincipal R M
m : M
hm : ⊤ = R ∙ m
r : R
x✝ : f (r • m) ∈ ⊤
⊢ r • f m ∈ R ∙ f m
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
ha'b : ⊥ ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨⊥, ha'b⟩
⊢ a = b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
ha'b : ⊥ ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨⊥, ha'b⟩
⊢ a = b
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ a ⊓ a' = ⊥

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ a ⊓ a' = ⊥
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))

Tactic:
simp_rw [sSup_image]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ a ∈ {j | j ≠ i}, t a)
Module: Mathlib.Algebra.Module.Torsion.Field

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_2
inst✝² : DivisionSemiring 𝕜
inst✝¹ : AddCommMonoid M
inst✝ : Module 𝕜 M
r : 𝕜
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ m₁ = m₂

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
M : Type u_2
inst✝² : DivisionSemiring 𝕜
inst✝¹ : AddCommMonoid M
inst✝ : Module 𝕜 M
r : 𝕜
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ m₁ = m₂
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
this : univ = {i | t i ≠ ⊥}
⊢ Injective t

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
this : univ = {i | t i ≠ ⊥}
⊢ Injective t
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 0) (f 1 ⊔ f 2)

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 0) (f 1 ⊔ f 2)
Module: Mathlib.Algebra.Module.Submodule.EqLocus

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f g : M →ₛₗ[τ₁₂] M₂
r : R
x : M
hx : f x = g x
⊢ f (r • x) = g (r • x)

Tactic:
simpa using

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f g : M →ₛₗ[τ₁₂] M₂
r : R
x : M
hx : f x = g x
⊢ τ₁₂ r • f x = τ₁₂ r • g x
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 1) (f 0 ⊔ f 2)

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 1) (f 0 ⊔ f 2)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)

Tactic:
simpa using

Goal state after:
case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: S : Type u
A : Type v
inst✝¹ : CommSemiring S
inst✝ : Semiring A
h1 h2 : Algebra S A
h :
  ∀ (r : S) (x : A),
    (have I := h1;
      r • x) =
      r • x
r : S
⊢ (algebraMap S A) r = (algebraMap S A) r

Tactic:
simpa using

Goal state after:
S : Type u
A : Type v
inst✝¹ : CommSemiring S
inst✝ : Semiring A
h1 h2 : Algebra S A
h :
  ∀ (r : S) (x : A),
    (have I := h1;
      r • x) =
      r • x
r : S
⊢ (algebraMap S A) r = (algebraMap S A) r
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✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m✝ : M
hm✝ : m✝ ∈ restrictScalars R (span A X)
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
r : R
⊢ (algebraMap R A) r • m ∈ span R X

Tactic:
simpa using

Goal state after:
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m✝ : M
hm✝ : m✝ ∈ restrictScalars R (span A X)
m : M
x✝ : m ∈ span A X
hm : m ∈ span R X
r : R
⊢ r • m ∈ span R X
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R✝ : Type u
S✝ : Type v
A : Type w
B : Type u₁
M✝ : Type v₁
inst✝¹³ : CommSemiring R✝
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R✝ A
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module A M✝
inst✝⁷ : IsScalarTower R✝ A M✝
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
N : Submodule R M
⊢ ∀ (c : S) {x : M}, x ∈ N.carrier → c • x ∈ N.carrier

Tactic:
simpa using

Goal state after:
R✝ : Type u
S✝ : Type v
A : Type w
B : Type u₁
M✝ : Type v₁
inst✝¹³ : CommSemiring R✝
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R✝ A
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module A M✝
inst✝⁷ : IsScalarTower R✝ A M✝
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
N : Submodule R M
⊢ ∀ (x : R) {x_1 : M}, x_1 ∈ N → x • x_1 ∈ N
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ ↑(insert ⊥ t)).Infinite
x : α
hx₁ : x ∈ s
hx₂ : x ∉ ↑(insert ⊥ t)
⊢ x ≠ ⊥ ∧ x ∉ t

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ ↑(insert ⊥ t)).Infinite
x : α
hx₁ : x ∈ s
hx₂ : x ∉ ↑(insert ⊥ t)
⊢ ¬x = ⊥ ∧ x ∉ t
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ (U.mulIndicator fun x ↦ a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
by
  rw [mulIndicator_preimage, Pi.one_def, Set.preimage_const, preimage_const]
  split_ifs <;> simp [← compl_eq_univ_sdiff]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
this : Disjoint x (sSup ((↑t ∪ {x}) \ {x}))
⊢ x ⊓ sSup s = ⊥

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
this : Disjoint x (sSup ((↑t ∪ {x}) \ {x}))
⊢ x ⊓ sSup s = ⊥
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr.add
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
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ x y : M
hx : x ∈ span R S
hy : y ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
hy' : f ⟨y, hy⟩ = g ⟨y, hy⟩
⊢ f ⟨x + y, ⋯⟩ = g ⟨x + y, ⋯⟩

Tactic:
| add x y hx hy hx' hy' =>

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
x y : ↥p
hxy : ↑((inclusionSpan S p) x) = ↑((inclusionSpan S p) y)
⊢ x = y

Tactic:
simpa using

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
x y : ↥p
hxy : ↑((inclusionSpan S p) x) = ↑((inclusionSpan S p) y)
⊢ x = y
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 ↑p ≤ q

Tactic:
simpa using

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
this : ⇑q.subtype '' ↑(inclusion h₁).range = ↑p
⊢ span S ↑p ≤ q
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
x : M
⊢ x ∈ ⇑q.subtype '' ↑(inclusion h₁).range ↔ x ∈ ↑p

Tactic:
simpa using

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 ∈ p → x ∈ q
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ ∀ (i : ↑s), sSupIndep ↑i

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ ∀ a ∈ s, sSupIndep a
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ ?m.85

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ ?m.85
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
a : κ
⊢ (∏ i ∈ s, (f i).indicator (g i)) a = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) a

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
a : κ
⊢ ∏ c ∈ s, (f c).indicator (g c) a = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) a
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
⊢ (a ::ₘ s + t).antidiagonal = (a ::ₘ s).antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal

Tactic:
simp_rw [cons_add, antidiagonal_cons, ih, add_bind, bind_map, map_bind, map_map]

Goal state after:
case cons
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
⊢ ((s.antidiagonal.bind fun a_1 ↦
        map ((fun x ↦ Prod.map id (cons a) x) ∘ fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal) +
      s.antidiagonal.bind fun a_1 ↦
        map ((fun x ↦ Prod.map (cons a) id x) ∘ fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal) =
    (s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map id (cons a) a_1).1 + q.1, (Prod.map id (cons a) a_1).2 + q.2)) t.antidiagonal) +
      s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map (cons a) id a_1).1 + q.1, (Prod.map (cons a) id a_1).2 + q.2)) t.antidiagonal
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s✝ : Multiset ι
f g : ι → R
a : ι
s : Multiset ι
ih : (map (fun i ↦ f i + g i) s).prod = (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
⊢ (map (fun i ↦ f i + g i) (a ::ₘ s)).prod =
    (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) (a ::ₘ s).antidiagonal).sum

Tactic:
simp only [map_cons, prod_cons, ih, sum_map_mul_left.symm, add_mul, mul_left_comm (f a),
      mul_left_comm (g a), sum_map_add, antidiagonal_cons, Prod.map_fst, Prod.map_snd,
      id_eq, map_add, map_map, Function.comp_apply, mul_assoc, sum_add]

Goal state after:
case refine_2
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s✝ : Multiset ι
f g : ι → R
a : ι
s : Multiset ι
ih : (map (fun i ↦ f i + g i) s).prod = (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
⊢ (map (fun i ↦ (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal).sum +
      (map (fun i ↦ (map f i.1).prod * (g a * (map g i.2).prod)) s.antidiagonal).sum =
    (map (fun x ↦ (map f x.1).prod * (g a * (map g x.2).prod)) s.antidiagonal).sum +
      (map (fun i ↦ (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal).sum
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case add_left
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u₁ u₂ : M
v : N
hu₁ : u₁ ∈ span R s
hu₂ : u₂ ∈ span R s
hv : v ∈ span R t
huv₁ : (B u₁) v ∈ P'
huv₂ : (B u₂) v ∈ P'
⊢ (B (u₁ + u₂)) v ∈ P'

Tactic:
simpa using

Goal state after:
case add_left
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u₁ u₂ : M
v : N
hu₁ : u₁ ∈ span R s
hu₂ : u₂ ∈ span R s
hv : v ∈ span R t
huv₁ : (B u₁) v ∈ P'
huv₂ : (B u₂) v ∈ P'
⊢ (B u₁) v + (B u₂) v ∈ P'
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case add_right
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u : M
v₁ v₂ : N
hu : u ∈ span R s
hv₁ : v₁ ∈ span R t
hv₂ : v₂ ∈ span R t
huv₁ : (B u) v₁ ∈ P'
huv₂ : (B u) v₂ ∈ P'
⊢ (B u) (v₁ + v₂) ∈ P'

Tactic:
simpa using

Goal state after:
case add_right
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u : M
v₁ v₂ : N
hu : u ∈ span R s
hv₁ : v₁ ∈ span R t
hv₂ : v₂ ∈ span R t
huv₁ : (B u) v₁ ∈ P'
huv₂ : (B u) v₂ ∈ P'
⊢ (B u) v₁ + (B u) v₂ ∈ P'
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case smul_left
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t✝ : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t✝, (B x) y ∈ P'
x : M
y : N
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ (B (t • u)) v ∈ P'

Tactic:
simpa using

Goal state after:
case smul_left
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t✝ : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t✝, (B x) y ∈ P'
x : M
y : N
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ t • (B u) v ∈ P'
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case smul_right
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t✝ : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t✝, (B x) y ∈ P'
x : M
y : N
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ (B u) (t • v) ∈ P'

Tactic:
simpa using

Goal state after:
case smul_right
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t✝ : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t✝, (B x) y ∈ P'
x : M
y : N
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ t • (B u) v ∈ P'