mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
x : AddSubmonoid (Additive M)
⊢ (fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
x : AddSubmonoid A
⊢ (fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
x : Submonoid (Multiplicative A)
⊢ (fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: P : Type u_3
inst✝ : MulOneClass P
S : Submonoid P
⊢ ∀ (x : P), x ∈ comap (MonoidHom.id P) S ↔ x ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f (x * y) = f x * f y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
⊢ ∀ {a b : N}, a ∈ ⇑f '' ↑S → b ∈ ⇑f '' ↑S → a * b ∈ ⇑f '' ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
inst✝ : Nonempty ι
f : F
hf : Injective ⇑f
s : ι → Submonoid M
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ Disjoint (map f H) (map f K)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Injective ⇑f
S : Submonoid M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Surjective ⇑f
S : Submonoid N
x : N
h : x ∈ S
y : M
hy : f y = x
⊢ y ∈ comap f S ∧ f y = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
x : M × N
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (MonoidHom.fst M N) s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid N
x : M × N
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (MonoidHom.snd M N) s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
by

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

Goal state before:
pp: α : Sort u
⊢ ¬Uncountable α ↔ Countable α

Tactic:
by

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

Goal state before:
pp: α : Sort u
inst✝ : Nonempty α
⊢ Uncountable α ↔ ∀ (f : ℕ → α), ¬Surjective f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ s.prod t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
⊢ (inl M N) x1 ∈ u

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
⊢ (inr M N) x2 ∈ u

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ s.prod t ≤ u ↔ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Set M
⊢ map (inr M N) ⊥ ≤ closure (s ×ˢ {1})

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
t : Set N
⊢ map (inl M N) ⊥ ≤ closure ({1} ×ˢ t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
⊢ mrange (id M) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
g : N →* P
f : M →* N
⊢ map g (mrange f) = mrange (g.comp f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ ↑(mrange f) = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ closure (Set.range ⇑f) = mrange f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝³ : MulOneClass M
N : Type u_5
S : Type u_6
inst✝² : MulOneClass N
f : M →* N
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
⊢ f.domRestrict s = 1 ↔ ∀ x ∈ s, f x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
f : M →* N
⊢ mrange (f.domRestrict S) = map f S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
⊢ domRestrict 1 M' = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝¹ x✝ : M →* A
⊢ (x✝¹ * x✝).domRestrict M' = x✝¹.domRestrict M' * x✝.domRestrict M'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
⊢ mker f.mrangeRestrict = mker f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker 1 = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ mker (f.prodMap g) = (mker f).prod (mker g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker (inl M N) = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker (inr M N) = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective ⇑f
y : ↥N'
⊢ ∃ a, (f.submonoidComap N') a = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
M' : Submonoid M
⊢ Surjective ⇑(f.submonoidMap M')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
hf : Injective ⇑f
M' : Submonoid M
⊢ Injective ⇑(f.submonoidMap M')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inl M N) = ⊤.prod ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inr M N) = ⊥.prod ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
s : Submonoid M
t : Submonoid N
⊢ s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
s : Submonoid M
t : Submonoid N
⊢ s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inl M N) ⊔ mrange (inr M N) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ (∀ (x : M), x ∈ S ↔ x ∈ ⊥) ↔ ∀ x ∈ S, x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ S = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ (∃ x, ∃ (hx : x ∈ S), ⟨x, hx⟩ ≠ ⟨1, ⋯⟩) ↔ ∃ x ∈ S, x ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ S = ⊥ ∨ Nontrivial ↥S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ Codisjoint (map f H) (map f K)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
I : Set ι
x : (i : ι) → M i
⊢ (x ∈ pi I fun i ↦ ⊤) ↔ x ∈ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
H : (i : ι) → Submonoid (M i)
x : (i : ι) → M i
⊢ x ∈ pi ∅ H ↔ x ∈ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
x : (i : ι) → M i
⊢ (x ∈ pi Set.univ fun i ↦ ⊥) ↔ x ∈ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → MulOneClass (M i)
inst✝ : DecidableEq ι
S : (i : ι) → Submonoid (M i)
I : Set ι
i : ι
x : M i
hx : x ∈ S i
⊢ x ∈ comap (mulSingle M i) (pi I S)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
e : M ≃* N
⊢ S.equivMapOfInjective ↑e ⋯ = e.submonoidMap S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x : ↥(IsUnit.submonoid M)
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ IsUnit.unit ⋯) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑(x * y), ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
h : S ≤ MonoidHom.mrange f
⊢ map f (comap f S) = S

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Nat

Goal state before:
pp: α : Type u_1
x✝ : Bool × ℕ
b : Bool
n : ℕ
⊢ (fun n ↦ (n.bodd, n.div2)) (uncurry bit (b, n)) = (b, n)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Nat

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ uncurry bit ((fun n ↦ (n.bodd, n.div2)) n) = n

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Nat

Goal state before:
pp: ⊢ ⇑natSumNatEquivNat = Sum.elim (fun x ↦ 2 * x) fun x ↦ 2 * x + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.succ.bodd = !n.bodd

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
⊢ (m * n).bodd = (m.bodd && n.bodd)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b n).bodd = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n % 2 = n.bodd.toNat

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ (n + 1).div2 = bif n.bodd then n.div2.succ else n.div2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b n).div2 = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.bodd.toNat + 2 * n.div2 = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
⊢ 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n ≤ s * s + (s + s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ n.div2 < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
⊢ pair (unpair n).1 (unpair n).2 = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n a b : ℕ
H : unpair n = (a, b)
⊢ pair a b = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b : ℕ
h : ¬a < b
⊢ (a * a + (a + b)).sqrt = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n + 1 - (k + 1)) = shiftLeft' b m (n + 1) >>> (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b : ℕ
⊢ unpair (pair a b) = (a, b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝² x✝¹ x✝ : ℕ
hk : x✝ ≤ x✝¹
⊢ x✝² <<< (x✝¹ - x✝) = x✝² <<< x✝¹ >>> x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ (n + 2).bodd = (1 &&& n + 2 != 0)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b n >>> 1 >>> m).bodd = (n >>> m).bodd

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
n1 : 1 ≤ n
⊢ (unpair n).1 < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: ⊢ unpair 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: ⊢ (unpair 0).1 ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b : ℕ
⊢ a ≤ pair a b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b : ℕ
⊢ b ≤ pair a b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
⊢ (unpair n).2 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.boddDiv2 = (n.bodd, n.div2)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ some x = some y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ bit true (x✝¹ + x✝) = bit false x✝¹ + bit true x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ bit false (x✝¹ + x✝) = bit false x✝¹ + bit false x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ bit true (x✝¹ + x✝) = bit true x✝¹ + bit false x✝

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (fun n ↦ (decode n).getD d) (encode x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable α
f : β → α
finv : α → Option β
linv : ∀ (b : β), finv (f b) = some b
b : β
⊢ (decode (encode (f b))).bind finv = some b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: motive : ℕ → Sort u
⊢ Function.Injective fun H n ↦ bitCasesOn n H

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ bit true x✝¹ ≤ bit true x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ bit false x✝¹ ≤ bit false x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a₁ a₂ b : ℕ
h : a₁ < a₂
⊢ pair a₁ b < pair a₂ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
a b : Bool
h : m < n
⊢ bit a m < 2 * n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
a b : Bool
h : m < n
⊢ 2 * n ≤ bit b n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: ⊢ bits 0 = []

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : PUnit.{?u.4 + 1}
⊢ (Nat.casesOn 0 (some PUnit.unit) fun x ↦ none) = some x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ (bit b n).bits = b :: n.bits

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.bodd = n.bits.headI

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.div2.bits = n.bits.tail

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
o : Option α
⊢ (Nat.casesOn (Option.casesOn o zero fun a ↦ (encode a).succ) (some none) fun m ↦ Option.map some (decode m)) = some o

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
a : α
⊢ a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
a : α
⊢ decode₂ α (encode a) = some a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.op.Normal ↔ H.Normal

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.Normal ↔ H.Normal

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range encode

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
h : (decode₂ α x).isSome = true
⊢ encode ((decode₂ α x).get h) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b₁ b₂ : ℕ
h : b₁ < b₂
⊢ pair a b₁ < pair a b₂

Tactic:
by

Goal state after: