mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : MeasurableSet {a | p a}
⊢ MeasurableSet (p ⁻¹' {True})

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : Measurable p
⊢ MeasurableSet {a | p a}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | p a ↔ q a}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet {a | ∀ (i : ι), p i a}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet {a | ∃ i, p i a}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
⊢ Measurable fun x ↦ a = f x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable α
s t : β → Set α
hs✝ : Measurable s
hs : Measurable t
i : α
⊢ Measurable fun a ↦ i ∈ s a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable α
s t : β → Set α
hs✝ : Measurable s
hs : Measurable t
i : α
⊢ Measurable fun a ↦ i ∈ t a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace β
g : β → Finset α
⊢ Measurable g ↔ ∀ (a : α), Measurable fun x ↦ a ∈ g x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace β
g : β → Finset α
inst✝ : Countable α
S : Finset α
⊢ MeasurableSet {↑S}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace β
g : β → Finset α
inst✝ : Countable α
S : Finset α
⊢ {s | ↑s ∈ {↑S}} = {S}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
inst✝ : MeasurableSpace X
⊢ Measurable uncurry

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst✝ : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
⊢ Measurable Sigma.uncurry

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableEq α
⊢ MeasurableSingletonClass α

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ MeasurableEq α

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
by

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

Goal state before:
pp: ⊢ zero ≤ zero

Tactic:
by

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

Goal state before:
pp: ⊢ zero ≤ neg

Tactic:
by

Goal state after:
⊢ zero ≤ neg
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ¬zero ≤ neg

Tactic:
by

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

Goal state before:
pp: ⊢ zero ≤ pos

Tactic:
by

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

Goal state before:
pp: ⊢ neg ≤ zero

Tactic:
by

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

Goal state before:
pp: ⊢ neg ≤ neg

Tactic:
by

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

Goal state before:
pp: ⊢ neg ≤ pos

Tactic:
by

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

Goal state before:
pp: ⊢ pos ≤ zero

Tactic:
by

Goal state after:
⊢ pos ≤ zero
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ¬pos ≤ zero

Tactic:
by

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

Goal state before:
pp: ⊢ pos ≤ neg

Tactic:
by

Goal state after:
⊢ pos ≤ neg
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ¬pos ≤ neg

Tactic:
by

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

Goal state before:
pp: ⊢ pos ≤ pos

Tactic:
by

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

Goal state before:
pp: a b : SignType
⊢ Decidable (a ≤ b)

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b c : SignType), a * b * c = a * (b * c)

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ 1 * a = a

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ a * 1 = a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : SignType), a * b = b * a

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ 0 * a = 0

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ a * 0 = 0

Tactic:
by

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
by

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

Goal state before:
pp: a : SignType
ha : a ≠ 0
⊢ a * id a = 1

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ a ≤ a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b c : SignType), a ≤ b → b ≤ c → a ≤ c

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : SignType), a ≤ b → b ≤ a → a = b

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : SignType), a ≤ b ∨ b ≤ a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a : SignType), -1 ≤ a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x : SignType), - -x = x

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x y : SignType), -x * y = -(x * y)

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x y : SignType), x * -y = -(x * y)

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ 0 < 3

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ 1 < 3

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ 2 < 3

Tactic:
by

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

Goal state before:
pp: s : SignType
n : ℕ
hn : Odd n
⊢ s ^ n = s

Tactic:
by

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

Goal state before:
pp: s : SignType
z : ℤ
hz : Odd z
⊢ s ^ z = s

Tactic:
by

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

Goal state before:
pp: s : SignType
n : ℕ
hn : Even n
hs : s ≠ 0
⊢ s ^ n = 1

Tactic:
by

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

Goal state before:
pp: s : SignType
z : ℤ
hz : Even z
hs : s ≠ 0
⊢ s ^ z = 1

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ (fun a ↦
        match a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1)
      ((fun a ↦
          match a with
          | zero => ⟨0, fin3Equiv._proof_7⟩
          | pos => ⟨1, fin3Equiv._proof_8⟩
          | neg => ⟨2, fin3Equiv._proof_9⟩)
        a) =
    a

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
x y : SignType
⊢ ↑(x * y) = ↑x * ↑y

Tactic:
by

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

Goal state before:
pp: ⊢ Finset.univ = {0, -1, 1}

Tactic:
by

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

Goal state before:
pp: a : Fin 3
isLt✝ : 0 < 3
⊢ (fun a ↦
        match a with
        | zero => ⟨0, fin3Equiv._proof_7⟩
        | pos => ⟨1, fin3Equiv._proof_8⟩
        | neg => ⟨2, fin3Equiv._proof_9⟩)
      ((fun a ↦
          match a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1)
        ⟨0, isLt✝⟩) =
    ⟨0, isLt✝⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : Nontrivial α
inst✝ : DecidableLT α
n : ℤ
⊢ sign ↑n = sign n

Tactic:
by

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

Goal state before:
pp: a : Fin 3
isLt✝ : 1 < 3
⊢ (fun a ↦
        match a with
        | zero => ⟨0, fin3Equiv._proof_7⟩
        | pos => ⟨1, fin3Equiv._proof_8⟩
        | neg => ⟨2, fin3Equiv._proof_9⟩)
      ((fun a ↦
          match a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1)
        ⟨1, isLt✝⟩) =
    ⟨1, isLt✝⟩

Tactic:
by

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

Goal state before:
pp: a : Fin 3
isLt✝ : 2 < 3
⊢ (fun a ↦
        match a with
        | zero => ⟨0, fin3Equiv._proof_7⟩
        | pos => ⟨1, fin3Equiv._proof_8⟩
        | neg => ⟨2, fin3Equiv._proof_9⟩)
      ((fun a ↦
          match a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1)
        ⟨2, isLt✝⟩) =
    ⟨2, isLt✝⟩

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ sign (x * y) = sign x * sign y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ ↑(sign x) * |x| = x

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ |x| * ↑(sign x) = x

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ ↑(sign x) * x = |x|

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ x * ↑(sign x) = |x|

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
t : SignType
h : ∀ i ∈ s, sign (f i) = t
⊢ sign (∑ i ∈ s, f i) = t

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∃ β t sgn g,
    (∀ (b : β), g b ∈ s) ∧ #t = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
β : Type u
t : Finset β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
ht : #t = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card ↥t = ∑ a ∈ s, (f a).natAbs

Tactic:
by

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

Goal state before:
pp: a b : SignType
⊢ (match a * b with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match a with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match b with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ 0 ≤ a ↔ a = 0 ∨ a = 1

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ 0 ≤ a ↔ a ≠ -1

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ -1 < a ↔ 0 ≤ a

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ a ≤ 0 ↔ a = -1 ∨ a = 0

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ a ≤ 0 ↔ a ≠ 1

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ a < 1 ↔ a ≤ 0

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ a < 0 ↔ a = -1

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ 0 < a ↔ a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card (β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)) = n

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ a = -a ↔ a = 0

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ -a = a ↔ a = 0

Tactic:
by

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

Goal state before:
pp: a : SignType
⊢ -a = 0 ↔ a = 0

Tactic:
by

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

Goal state before:
pp: a b : SignType
⊢ -a ≤ -b ↔ b ≤ a

Tactic:
by

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

Goal state before:
pp: a b : SignType
⊢ -a < -b ↔ b < a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
a : α
ha : a ∈ s
⊢ (∑ i,
      if Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) i = a then ↑(Sum.elim sgn 0 i) else 0) =
    f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
s : SignType
⊢ f ↑s = ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f ↑s = ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
s : SignType
⊢ ↑(-s) = -↑s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous[inst✝², inst✝¹] ⇑(algebraMap R A)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
⊢ Continuous[inst✝², inst✝¹] ⇑(algebraMap R A) ↔ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1 • p.2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ toSpanSingleton R 1 = algebraMapCLM R A

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →A[R] B
h : (fun f ↦ ⇑f.toAlgHom) f = (fun f ↦ ⇑f.toAlgHom) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
⊢ ∃ β x sgn g,
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i, if g i = a then ↑(sgn i) else 0) = f a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →A[R] B
⊢ ↑f = ↑g ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ (↑0)⁻¹ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
⊢ 1 ≤ ↑(n + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →A[R] B
f' : A → B
h : f' = ⇑f
r : R
⊢ (↑↑((↑f).copy f' h)).toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
⊢ 0 < 1 / (↑n + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : IsSemitopologicalSemiring A
s : Subalgebra R A
r : R
⊢ (algebraMap R A) r ∈ s.topologicalClosure.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 1 / (↑m + 1) ≤ 1 / (↑n + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsSemitopologicalSemiring A
inst✝ : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : s.topologicalClosure = ⊤
⊢ (map (↑f) s).topologicalClosure = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ 1 / (↑m + 1) < 1 / (↑n + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
inst✝¹ : TopologicalSpace A
inst✝ : Algebra R A
f : A →A[R] A
⊢ ↑f = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
⊢ (fun a ↦ if 0 < a then 1 else if a < 0 then -1 else 0) a ≤ (fun a ↦ if 0 < a then 1 else if a < 0 then -1 else 0) b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ 0 ≤ 1 - 1 / ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
⊢ sign 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsSemitopologicalSemiring A
s : Subalgebra R A
⊢ IsClosed[inst✝³] ↑s.topologicalClosure

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddLeftMono α
n : ℕ
⊢ 1 - 1 / ↑n ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : 0 < a
⊢ sign a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ sign a = -1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
⊢ sign a = 1 ↔ 0 < a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : IsSemitopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ⇑f = ⇑f'
⊢ comap f s.topologicalClosure = (comap f s).topologicalClosure

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
⊢ sign a = -1 ↔ a < 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsSemitopologicalSemiring A
x : A
s : Subalgebra R A
hs : IsClosed[inst✝³] ↑s
hx : x ∈ s
⊢ {x} ⊆ ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Zero α
inst✝⁵ : LinearOrder α
β : Type u_2
F : Type u_3
inst✝⁴ : Zero β
inst✝³ : Preorder β
inst✝² : DecidableLT β
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ sign (f a) = sign a

Tactic:
by

Goal state after: