mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: case mk
x : Nat × ArgReorder
perm✝ : Permutation
argReorders✝ : Array (Nat × ArgReorder)
h✝ : x ∈ { perm := perm✝, argReorders := argReorders✝ }.argReorders
⊢ sizeOf x.snd < sizeOf { perm := perm✝, argReorders := argReorders✝ }

Tactic:
;

Goal state after:
case mk
x : Nat × ArgReorder
perm✝ : Permutation
argReorders✝ : Array (Nat × ArgReorder)
h✝ : x ∈ { perm := perm✝, argReorders := argReorders✝ }.argReorders
⊢ sizeOf x.snd < sizeOf { perm := perm✝, argReorders := argReorders✝ }
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: case mk
x : Nat × ArgReorder
perm✝ : Permutation
argReorders✝ : Array (Nat × ArgReorder)
perm : List String :=
  List.map
    (fun x ↦
      match x with
      | ⟨x, h⟩ =>
        " ".intercalate
          (List.map
            (fun x_1 ↦
              match x_1 with
              | ⟨x_2, h⟩ => ToString.toString (x_2 + 1))
            x.val.attach))
    (List.attach { perm := perm✝, argReorders := argReorders✝ }.perm)
h✝ : x ∈ { perm := perm✝, argReorders := argReorders✝ }.argReorders
⊢ sizeOf x.snd < sizeOf { perm := perm✝, argReorders := argReorders✝ }

Tactic:
;

Goal state after:
case mk
x : Nat × ArgReorder
perm✝ : Permutation
argReorders✝ : Array (Nat × ArgReorder)
perm : List String :=
  List.map
    (fun x ↦
      match x with
      | ⟨x, h⟩ =>
        " ".intercalate
          (List.map
            (fun x_1 ↦
              match x_1 with
              | ⟨x_2, h⟩ => ToString.toString (x_2 + 1))
            x.val.attach))
    (List.attach { perm := perm✝, argReorders := argReorders✝ }.perm)
h✝ : x ∈ { perm := perm✝, argReorders := argReorders✝ }.argReorders
⊢ sizeOf x.snd < sizeOf { perm := perm✝, argReorders := argReorders✝ }
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: hn : 0 >>> 1 ≠ 0
⊢ False

Tactic:
;

Goal state after:
hn : 0 >>> 1 ≠ 0
⊢ False
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case zero
n0 : ¬0 = 0
⊢ (if 0 >>> 1 = 0 then 0 else (0 >>> 1).log2.succ) < if 0 = 0 then 0 else (log2 0).succ

pp: case succ
n : Nat
n0 : ¬n + 1 = 0
⊢ (if (n + 1) >>> 1 = 0 then 0 else ((n + 1) >>> 1).log2.succ) < if n + 1 = 0 then 0 else (n + 1).log2.succ

Tactic:
;

Goal state after:
case zero
n0 : ¬0 = 0
⊢ (if 0 >>> 1 = 0 then 0 else (0 >>> 1).log2.succ) < if 0 = 0 then 0 else (log2 0).succ

case succ
n : Nat
n0 : ¬n + 1 = 0
⊢ (if (n + 1) >>> 1 = 0 then 0 else ((n + 1) >>> 1).log2.succ) < if n + 1 = 0 then 0 else (n + 1).log2.succ
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case succ.zero
n0 : ¬0 + 1 = 0
⊢ (if (0 + 1) >>> 1 = 0 then 0 else ((0 + 1) >>> 1).log2.succ) < if 0 + 1 = 0 then 0 else (0 + 1).log2.succ

pp: case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ

Tactic:
;

Goal state after:
case succ.zero
n0 : ¬0 + 1 = 0
⊢ (if (0 + 1) >>> 1 = 0 then 0 else ((0 + 1) >>> 1).log2.succ) < if 0 + 1 = 0 then 0 else (0 + 1).log2.succ

case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)
⊢ e ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n

Tactic:
;

Goal state after:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)
⊢ e ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e✝ : motive (bit b n) = motive (bit b n)
⊢ e✝ ▸ h b n = h b n

Tactic:
;

Goal state after:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e✝ : motive (bit b n) = motive (bit b n)
⊢ e✝ ▸ h b n = h b n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
e : motive (Nat.bit ((Nat.bit b n).testBit 0) (Nat.bit b n >>> 1)) = motive (Nat.bit b n)
⊢ e ▸ bit ((Nat.bit b n).testBit 0) (Nat.bit b n >>> 1) (binaryRec zero bit (Nat.bit b n >>> 1)) =
    bit b n (binaryRec zero bit n)

Tactic:
;

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
e : motive (Nat.bit ((Nat.bit b n).testBit 0) (Nat.bit b n >>> 1)) = motive (Nat.bit b n)
⊢ e ▸ bit ((Nat.bit b n).testBit 0) (Nat.bit b n >>> 1) (binaryRec zero bit (Nat.bit b n >>> 1)) =
    bit b n (binaryRec zero bit n)
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
e✝ : motive (Nat.bit b n) = motive (Nat.bit b n)
⊢ e✝ ▸ bit b n (binaryRec zero bit n) = bit b n (binaryRec zero bit n)

Tactic:
;

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
e✝ : motive (Nat.bit b n) = motive (Nat.bit b n)
⊢ e✝ ▸ bit b n (binaryRec zero bit n) = bit b n (binaryRec zero bit n)
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ SemiconjBy (a * b) x z

Tactic:
by
  unfold SemiconjBy
  rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x : G
⊢ a * x = a * x * a⁻¹ * a

Tactic:
;

Goal state after:
G : Type u_3
inst✝ : Group G
a x : G
⊢ a * x = a * x * a⁻¹ * a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ } =
    { one := one₁, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }

Tactic:
;

Goal state after:
case refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ } =
    { one := one₁, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case zero
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : 0 ≠ 0
⊢ npowRec (m + 0) a = npowRec m a * npowRec 0 a

pp: case succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a

Tactic:
;

Goal state after:
case zero
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : 0 ≠ 0
⊢ npowRec (m + 0) a = npowRec m a * npowRec 0 a

case succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec m a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
;

Goal state after:
case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec m a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m : M
⊢ npowRec' (2 * k) m = npowRec' k (m * m)

Tactic:
induction k using Nat.strongRecOn with

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
k0 : k ≠ 0
m : M
⊢ m * npowRec' k m = npowRec' k m * m

Tactic:
induction k using Nat.strongRecOn with

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m : M
⊢ npowRec (k + 1) m = 1 * npowRec' (k + 1) m

Tactic:
induction k using Nat.strongRecOn with

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl
α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ property✝ : p x
⊢ ⟨x, property✝¹⟩ = ⟨x, property✝⟩

Tactic:
;

Goal state after:
case refl
α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ property✝ : p x
⊢ ⟨x, property✝¹⟩ = ⟨x, property✝⟩
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
g : α → γ
h₁ : f ≍ g
⊢ f x = g x

Tactic:
;

Goal state after:
case refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
g : α → γ
h₁ : f ≍ g
⊢ f x = g x
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl.refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
⊢ f x = f x

Tactic:
;

Goal state after:
case refl.refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
⊢ f x = f x
Module: Mathlib.Logic.Basic

Goal state before:
pp: α γ : Sort u_1
a : α
c : γ
⊢ cast ⋯ a ≍ c ↔ a ≍ c

Tactic:
;

Goal state after:
α γ : Sort u_1
a : α
c : γ
⊢ cast ⋯ a ≍ c ↔ a ≍ c
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u_1
a : α
b : β
⊢ a ≍ cast ⋯ b ↔ a ≍ b

Tactic:
;

Goal state after:
α β : Sort u_1
a : α
b : β
⊢ a ≍ cast ⋯ b ↔ a ≍ b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
b : β
e : β = α
⊢ cast e b ≍ b

Tactic:
;

Goal state after:
α β : Sort u
b : β
e : β = α
⊢ cast e b ≍ b
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl
α : Sort u
a : α
e : α = α
⊢ a = cast e a

Tactic:
;

Goal state after:
case refl
α : Sort u
a : α
e : α = α
⊢ a = cast e a
Module: Mathlib.Logic.Basic

Goal state before:
pp: β : Sort u
b a : β
h : a = cast ⋯ b
⊢ a ≍ b

Tactic:
;

Goal state after:
β : Sort u
b a : β
h : a = cast ⋯ b
⊢ a ≍ b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x

Tactic:
;

Goal state after:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x

Tactic:
;

Goal state after:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : h₁
⊢ p True

Tactic:
by simpa only [H] using h₂

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : ¬h₁
⊢ p False

Tactic:
by simpa only [H] using h₂

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y

Tactic:
;

Goal state after:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f default ≍ Function.const α (f default) x✝¹

Tactic:
;

Goal state after:
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f default ≍ Function.const α (f default) x✝¹
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
a : α
⊢ β a = β' a

Tactic:
;

Goal state after:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
a : α
⊢ β a = β' a
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
y : α
x✝ : { x // y = x }
⊢ ⟨y, ⋯⟩ = ⟨y, ⋯⟩

Tactic:
;

Goal state after:
α : Sort u_1
y : α
x✝ : { x // y = x }
⊢ ⟨y, ⋯⟩ = ⟨y, ⋯⟩
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
a : α
⊢ (fun g ↦ g ∘ f) (fun x ↦ c) a = (fun g ↦ g ∘ f) (fun x ↦ if x = b₀ then c' else c) a

Tactic:
;

Goal state after:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
a : α
⊢ (fun g ↦ g ∘ f) (fun x ↦ c) a = (fun g ↦ g ∘ f) (fun x ↦ if x = b₀ then c' else c) a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b

Tactic:
;

Goal state after:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ a'₂ : α
ha' : a'₁ = a'₂
v₁ v₂ : β
hv : v₁ = v₂
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₂ v₂ a₂

Tactic:
;

Goal state after:
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ a'₂ : α
ha' : a'₁ = a'₂
v₁ v₂ : β
hv : v₁ = v₂
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₂ v₂ a₂
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ : α
v₁ v₂ : β
hv : v₁ = v₂
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₁ v₂ a₂

Tactic:
;

Goal state after:
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ : α
v₁ v₂ : β
hv : v₁ = v₂
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₁ v₂ a₂
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ : α
v₁ : β
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₁ v₁ a₂

Tactic:
;

Goal state after:
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ : α
v₁ : β
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₁ v₁ a₂
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ : α
v₁ : β
a₁ : α
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₁ v₁ a₁

Tactic:
;

Goal state after:
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ : α
v₁ : β
a₁ : α
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₁ v₁ a₁
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (¬∀ (x : α), ¬p x (update f a b x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)

Tactic:
forall_update_iff f fun a b ↦ ¬p a b

Goal state after:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)
Module: Mathlib.Data.FunLike.Basic

Goal state before:
pp: case refl
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f : F
⊢ ⇑f = ⇑f

Tactic:
;

Goal state after:
case refl
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f : F
⊢ ⇑f = ⇑f
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
x✝¹ : α
x✝ : β
⊢ Relation.Map r id id x✝¹ x✝ ↔ r x✝¹ x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
x✝¹ : α
x✝ : β
⊢ Relation.Map r id id x✝¹ x✝ ↔ r x✝¹ x✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inl.inl
α : Type u_1
r : α → α → Prop
a b : α
U : Relator.RightUnique r
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
ac : ReflTransGen r a b✝
IH : ReflTransGen r b✝ b✝
⊢ ReflTransGen r c✝ b✝ ∨ ReflTransGen r b✝ c✝

pp: case tail.inl.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
e : α
be : r b✝ e
ec : ReflTransGen r e c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
· exact Or.inr (single bd)

Goal state after:
case tail.inl.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
e : α
be : r b✝ e
ec : ReflTransGen r e c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) ↔ b = a

Tactic:
;

Goal state after:
α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) ↔ b = a
Module: Mathlib.Logic.Relation

Goal state before:
pp: case symm
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝

Tactic:
;

Goal state after:
case symm
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f

Tactic:
;

Goal state after:
α : Type u
f : α → α
m n : ℕ
⊢ (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: case mk
α : Sort u
β : Sort v
γ : Sort w
e₂ : α ≃ β
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
h₁ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun = e₂.toFun
h₂ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = e₂.invFun
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = e₂

Tactic:
;

Goal state after:
case mk
α : Sort u
β : Sort v
γ : Sort w
e₂ : α ≃ β
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
h₁ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun = e₂.toFun
h₂ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = e₂.invFun
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = e₂
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
x : α
⊢ f^[m + n] x = f^[m] (f^[n] x)

Tactic:
by
  rw [iterate_add f m n]
  rfl

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

Goal state before:
pp: case mk.mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : RightInverse invFun✝¹ toFun✝¹
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
h₁ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun
h₂ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : RightInverse invFun✝¹ toFun✝¹
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
h₁ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun
h₂ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u_1
x : α
⊢ (Equiv.cast ⋯) x = ((Equiv.cast ⋯).trans (Equiv.cast ⋯)) x

Tactic:
;

Goal state after:
α : Sort u_1
x : α
⊢ (Equiv.cast ⋯) x = ((Equiv.cast ⋯).trans (Equiv.cast ⋯)) x
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u_1
a b : α
⊢ (Equiv.cast ⋯) a = b ↔ a ≍ b

Tactic:
;

Goal state after:
α : Sort u_1
a b : α
⊢ (Equiv.cast ⋯) a = b ↔ a ≍ b
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: case mk
α : Sort u
β : Sort v
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ (Equiv.refl α).trans { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
;

Goal state after:
case mk
α : Sort u
β : Sort v
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ (Equiv.refl α).trans { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ((ab.equivCongr cd).symm x✝¹) x✝ = ((ab.symm.equivCongr cd.symm) x✝¹) x✝

Tactic:
;

Goal state after:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ((ab.equivCongr cd).symm x✝¹) x✝ = ((ab.symm.equivCongr cd.symm) x✝¹) x✝
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β✝ : Sort v
γ : Sort w
inst✝ : Unique α
β : α → Sort u_1
f : (i : α) → β i
i : α
⊢ uniqueElim ((fun f ↦ f default) f) i = f i

Tactic:
;

Goal state after:
α : Sort u
β✝ : Sort v
γ : Sort w
inst✝ : Unique α
β : α → Sort u_1
f : (i : α) → β i
i : α
⊢ uniqueElim ((fun f ↦ f default) f) i = f i
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: case refl
α : Sort u
β✝ : Sort v
γ : Sort w
inst✝ : Unique α
β : α → Sort u_1
f : (i : α) → β i
⊢ uniqueElim ((fun f ↦ f default) f) default = f default

Tactic:
;

Goal state after:
case refl
α : Sort u
β✝ : Sort v
γ : Sort w
inst✝ : Unique α
β : α → Sort u_1
f : (i : α) → β i
⊢ uniqueElim ((fun f ↦ f default) f) default = f default
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x✝¹ : α ≃ β
x✝ : α
⊢ ((fun f ↦ ofBijective ↑f ⋯) ((fun f ↦ ⟨⇑f, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x✝¹ : α ≃ β
x✝ : α
⊢ ((fun f ↦ ofBijective ↑f ⋯) ((fun f ↦ ⟨⇑f, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝