mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Span.Defs

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case false
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
a✝ : Nontrivial α
⊢ (c < bif false then c else cᶜ) → c = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case true
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
a✝ : Nontrivial α
⊢ (c < bif true then c else cᶜ) → c = ⊥

Tactic:
simp

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
I : Submodule R M
a : M
⊢ I < I ⊔ R ∙ a ↔ a ∉ I

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
h : ∀ a ∈ Subtype.val '' S, IsAtom a
a : α
⊢ a ∈ Subtype.val '' (fun A ↦ {a | ↑a ≤ A}) ((fun S ↦ sSup (Subtype.val '' S)) S) ↔
    a ∈ {a | a ≤ sSup (Subtype.val '' S) ∧ IsAtom a}

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x : M
hx : x ∈ span R S
⊢ ↑∅ ⊆ S ∧ 0 ∈ span R ↑∅

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b c : α
⊢ ⊥ ≤ b → b ≤ c → ⊥ ≤ c

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl.inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ ⊥ → ⊤ ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl.inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ ⊤ → ⊤ ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ c → ⊤ ≤ c

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
b : α
⊢ ⊥ ≤ b ∨ b ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
b : α
⊢ ⊤ ≤ b ∨ b ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y z : α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y z : α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
ht : ↑∅ ⊆ ↑(span R s)
⊢ ↑∅ ⊆ s ∧ ↑∅ ⊆ ↑(span R ↑∅)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
t : Finset M
ht : ↑t ⊆ ↑(span R s)
⊢ ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)

Tactic:
induction t using Finset.induction_on with
  | empty => exact ⟨∅, by simp⟩
  | insert a t hat IH =>
    obtain ⟨T, hTs, htT⟩ := IH (by simp_all [Set.insert_subset_iff])
    obtain ⟨T', hT's, haT'⟩ := mem_span_finite_of_mem_span (ht (Finset.mem_insert_self _ _))
    refine ⟨T ∪ T', by simp_all, ?_⟩
    simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_subset_iff, SetLike.mem_coe]
    exact ⟨mem_sup_right haT', htT.trans (le_sup_left (a := span R _))⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
⊢ equivBool ⊥ ≤ equivBool b ↔ ⊥ ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ equivBool ⊤ ≤ equivBool ⊤ ↔ ⊤ ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (⊥ ⊓ if ⊥ = ⊥ then ⊤ else ⊥) ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (⊤ ⊓ if ⊤ = ⊥ then ⊤ else ⊥) ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ ⊔ if ⊥ = ⊥ then ⊤ else ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊤ ⊔ if ⊤ = ⊥ then ⊤ else ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s : Set α
t : Set β
⊢ supClosure (infClosure (s ×ˢ t)) = supClosure (infClosure s) ×ˢ supClosure (infClosure t)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y : α
⊢ (if ⊥ = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = ⊥ ⊓ if y = ⊥ then ⊤ else ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y : α
⊢ (if ⊤ = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = ⊤ ⊓ if y = ⊥ then ⊤ else ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Order

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
ι : Type u_1
hι : Nonempty ι
f : ι → α
D : Directed r f
s : Finset ι
z x✝ : ι
⊢ x✝ ∈ 0 → r (f x✝) (f z)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ ⊥ ≤ x ⊓ a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : Fin 2 → α
⊢ 0 ≠ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ x ⊓ a ≤ x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: p : Prop
⊢ IsAtom p ↔ p

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: p : Prop
⊢ IsCoatom p ↔ ¬p

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomic (π i)
b : (i : ι) → π i
h : ¬b = ⊥
i : ι
hi : ¬b i = ⊥
a : π i
ha : IsAtom a
hab : a ≤ b i
⊢ ∀ (j : ι), j ≠ i → ⊥ j ≤ b j

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
j : π i
hj : j ∈ upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s})
x : π i
x✝ : x ∈ {a | IsAtom a ∧ a ≤ s i}
hx₁ : IsAtom x
hx₂ : x ≤ s i
⊢ Function.eval i (Function.update ⊥ i x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
j : π i
hj : j ∈ upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s})
x : π i
x✝ : x ∈ {a | IsAtom a ∧ a ≤ s i}
hx₁ : IsAtom x
hx₂ : x ≤ s i
⊢ x ≤ j

Tactic:
exact hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, by simp [update_le_iff, hx₂]⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
hs : s.SupIndep f
v : Finset ι
hu : ∅ ⊆ s
hv : v ⊆ s
huv : Disjoint ∅ v
⊢ Disjoint (∅.sup f) (v.sup f)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → α
hs : s.SupIndep f
ht : t.SupIndep f
h : Disjoint (s.sup f) (t.sup f)
⊢ s ∪ t = {s, t}.biUnion id

Tactic:
simp

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

Goal state before:
pp: case h
α : 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
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
⊢ ↑∅ ⊆ s ∧ ⊥ = ∅.sup id

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ t.sup Subtype.val
⊢ ↑(Finset.image Subtype.val t) ⊆ s

Tactic:
simp

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
t : Set ι
hst : Disjoint (↑∅) t
⊢ Disjoint (⨆ i ∈ ∅, f i) (⨆ i ∈ t, f i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
⊢ ↑∅ ⊆ s ∧ ∅.sup id = ⊥

Tactic:
simp

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ (insert y t).sup id

Tactic:
simp

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

Goal state before:
pp: case h.e_f
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
i : ↥s
⊢ f ↑i = ⋯.choose ^ 2

Tactic:
exact ((isSquare_iff_exists_sq _).mp (h _ i.2)).choose_spec

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
x : α
⊢ x ∈ mulSupport (s.mulIndicator f) ↔ x ∈ s ∩ mulSupport f

Tactic:
by simp [Function.mem_mulSupport, mulIndicator_apply_eq_one]

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ (algebraMap S B) ((algebraMap R S) r) = (algebraMap R B) r

Tactic:
← algebraMap_apply R S B

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ (algebraMap R B) r = (algebraMap R B) r
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ t.sup id ∈ s

Tactic:
exact hsc.finsetSup_mem h ht₁

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A ≃ₐ[S] B
x : B
⊢ (restrictScalars R f).symm x = f.symm x

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A ≃ₐ[S] B
⊢ (restrictScalars R f).symm.toRingEquiv = f.symm.toRingEquiv

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
h✝ : 1 ∈ s
⊢ univ ∈ {univ, ∅}

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
h✝ : ¬1 ∈ s
⊢ ∅ ∈ {univ, ∅}

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A ≃ₐ[S] B
⊢ ⇑(restrictScalars R f).symm = ⇑f.symm

Tactic:
simp

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
⊢ x ∈ ↑t ∪ {x}

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : 1 ∈ s
⊢ U ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : ¬1 ∈ s
⊢ U ∪ ∅ ∈ {univ, U, Uᶜ, ∅}

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : 1 ∈ s
⊢ ∅ ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : ¬1 ∈ s
⊢ ∅ ∪ ∅ ∈ {univ, U, Uᶜ, ∅}

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0

Tactic:
rw [Ne, prod_eq_zero_iff]

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (¬∃ a ∈ s, f a = 0) ↔ ∀ a ∈ s, f a ≠ 0
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
inst✝³ : FunLike F α α
inst✝² : Monoid F
inst✝¹ : IsOneApplyEqSelf F α
inst✝ : IsMulApplyEqComp F α
f : F
x : α
⊢ (f ^ 0) x = (⇑f)^[0] x

Tactic:
simp

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

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
x✝ : α
⊢ 1 x✝ = 1 x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Mul F
inst✝¹ : Mul β
inst✝ : IsMulApply F α β
f g : F
x✝ : α
⊢ (f * g) x✝ = (⇑f * ⇑g) x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Div F
inst✝¹ : Div β
inst✝ : IsDivApply F α β
f g : F
x✝ : α
⊢ (f / g) x✝ = (⇑f / ⇑g) x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Inv F
inst✝¹ : Inv β
inst✝ : IsInvApply F α β
f : F
x✝ : α
⊢ f⁻¹ x✝ = (⇑f)⁻¹ x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : SMul M F
inst✝¹ : SMul M β
inst✝ : IsSMulApply M F α β
n : M
f : F
x✝ : α
⊢ (n • f) x✝ = (n • ⇑f) x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Pow F M
inst✝¹ : Pow β M
inst✝ : IsPowApply M F α β
f : F
n : M
x✝ : α
⊢ (f ^ n) x✝ = (⇑f ^ n) x✝

Tactic:
simp

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

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
x✝ : α
⊢ 1 x✝ = id x✝

Tactic:
simp

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

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : Mul F'
inst✝ : IsMulApplyEqComp F' α
f g : F'
x✝ : α
⊢ (f * g) x✝ = (⇑f ∘ ⇑g) x✝

Tactic:
simp

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

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝⁷ : FunLike F' α α
inst✝⁶ : NatCast F'
inst✝⁵ : One F'
inst✝⁴ : SMul ℕ α
inst✝³ : SMul ℕ F'
inst✝² : IsSMulApply ℕ F' α α
inst✝¹ : IsNatCastApply F' α
inst✝ : IsOneApplyEqSelf F' α
n : ℕ
⊢ ∀ (x : α), ↑n x = (n • 1) x

Tactic:
simp

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

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝⁷ : FunLike F' α α
inst✝⁶ : IntCast F'
inst✝⁵ : One F'
inst✝⁴ : SMul ℤ α
inst✝³ : SMul ℤ F'
inst✝² : IsSMulApply ℤ F' α α
inst✝¹ : IsIntCastApply F' α
inst✝ : IsOneApplyEqSelf F' α
n : ℤ
⊢ ∀ (x : α), ↑n x = (n • 1) x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V✝ : Type u_6
S✝ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s✝ t : Set M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f g : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
s : ↑S
⊢ ↑s ∈ S

Tactic:
simp

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
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
⊢ x ∈ ⊤

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V✝ : Type u_6
S✝ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s✝ t : Set M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
s : ↑S
⊢ ↑s ∈ S

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
s t : Set M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x y : ↥p
⊢ ⟨↑(x + y), ⋯⟩ = ⟨↑x, ⋯⟩ + ⟨↑y, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
s t✝ : Set M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
t : R
x : ↥p
⊢ ⟨↑(t • x), ⋯⟩ = (RingHom.id R) t • ⟨↑x, ⋯⟩

Tactic:
simp

Goal state after: