mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y z : α
h : f z = g z
⊢ f z = g z

Tactic:
]

Goal state after:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y z : α
h : f z = g z
⊢ f z = g z
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ g y = g y

Tactic:
]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : Nontrivial α
b : β
⊢ ∃ a b_1, b = b ∧ a ≠ b_1

Tactic:
]

Goal state after:
α : Type u_4
β : Type u_5
inst✝ : Nontrivial α
b : β
⊢ ∃ a b_1, b = b ∧ a ≠ b_1
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : β → α
h : β → γ
i : γ → β
hf : LeftInverse f g
hh : LeftInverse h i
a : γ
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ = g₁

Tactic:
]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₂ = g₂

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : some (Classical.choose h') = some a
⊢ f a = b
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_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b

Tactic:
]

Goal state after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
this : v = v'
⊢ v = v'

Tactic:
]

Goal state after:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
this : v = v'
⊢ v = v'
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
⊢ (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
]

Goal state after:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
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
⊢ ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)

Tactic:
]

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.Logic.Function.Basic

Goal state before:
pp: case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ update (Pi.map f default) i (f i y) = update (Pi.map f default) i (f i y)

Tactic:
]

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

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
⊢ x = y

Tactic:
have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩
    replace h := @h (Function.update default i x) (Function.update default i y) ?_
    · simpa using congrFun h i
    rw [Pi.map_update, Pi.map_update, hxy]

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

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
]

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = g c

Tactic:
]

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = g c
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ e' (f₂₃ b) = e' (f₂₃ b)

pp: case neg.hb
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ ¬∃ a, (f₂₃ ∘ f₁₂) a = f₂₃ b

Tactic:
]

Goal state after:
case neg.hb
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ ¬∃ a, (f₂₃ ∘ f₁₂) a = f₂₃ b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ e' a = e' a

pp: case neg.hb
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ ¬∃ a_1, (f₂₃ ∘ f₁₂) a_1 = a

Tactic:
]

Goal state after:
case neg.hb
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ ¬∃ a_1, (f₂₃ ∘ f₁₂) a_1 = a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
h : ∃ e, g = e ∘ f
x✝¹ x✝ : α
hf : f x✝¹ = f x✝
⊢ Classical.choose h (f x✝) = Classical.choose h (f x✝)

Tactic:
]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f✝ : α → β
γ : Type u_4
inst✝ : Nontrivial γ
surj : Surjective fun g ↦ g ∘ f✝
c c' : γ
not_inj : ∃ x x_1 x_2, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g ↦ g ∘ f✝) f = fun x ↦ if x = a₂ then c else c'
h₁ : f (f✝ a₁) = c'
h₂ : f (f✝ a₂) = c
⊢ c = c

Tactic:
]

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

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ f x = f x

Tactic:
]

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

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ (if P then f x else x) = if P then f x else x

Tactic:
]

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

Goal state before:
pp: p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ P (f ?a)

pp: case a
p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ p

Tactic:
]

Goal state after:
p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ P (f ?a)

case a
p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ p
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective h.mp

Tactic:
by
  -- TODO: mathlib3 uses `eq_rec_on_bijective`, difference in elaboration here
  -- due to `@[macro_inline]` possibly?
  cases h
  exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ C a ≍ C a

Tactic:
]

Goal state after:
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: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
⊢ TransGen r = TransGen r

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
⊢ ReflGen r = ReflGen r

Tactic:
]

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ ⟦x⟧ = y

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ EqvGen r = EqvGen r

Tactic:
]

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ x = ⟦y⟧

Tactic:
]

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x y : Quotient s
⊢ x = y ↔ x = y

Tactic:
]

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i ↦ ⟦a i⟧
⊢ p fun i ↦ ⟦(f i).out⟧

Tactic:
]

Goal state after:
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i ↦ ⟦a i⟧
⊢ p fun i ↦ ⟦(f i).out⟧
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ gb' (f x) = gb' (f x)

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
⊢ gb x = gb x

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f x = f x

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
n✝ n : ℕ
ihn : id^[n] = id
⊢ id = id

Tactic:
]

Goal state after:
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.Function.Iterate

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

Tactic:
]

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

Goal state before:
pp: α : Type u
f : α → α
x : α
h : f x = x
n✝ n : ℕ
ihn : f^[n] x = x
⊢ x = x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
e : Perm α
⊢ id = id

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n : ℕ
⊢ g = g

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ g ∘ f = g

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ g ∘ f = g
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: case zero
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g k)

Tactic:
]

Goal state after:
case zero
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g k)
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))

Tactic:
]

Goal state after:
case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
⊢ g (f.symm b) = g (f.symm b)

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

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

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

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

Tactic:
]

Goal state after:
α : Type u
f : α → α
n : ℕ
x : α
⊢ (f ∘ f^[n]) x = f (f^[n] x)
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n] = f^[n]

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)

Tactic:
]

Goal state after:
α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f = g.symm

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

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

Tactic:
]

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

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f.symm = g

Tactic:
]

Goal state after:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f.symm = g
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[n + m] a = f^[n] a ↔ f^[n + m] a = f^[n] a

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m] a = f^[n] a

Tactic:
]

Goal state after:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m] a = f^[n] a
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x ↦ f b) a l = f^[l.length] a
a : α
⊢ f^[l.length] (f a) = f^[l.length] (f a)

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ f (f^[l.length] b) = f (f^[l.length] b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₂ • 1 * a = r₂ • 1 * a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₁

pp: G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ ∀ (a : α), (a₂⁻¹ * a₁) • a = a

Tactic:
]

Goal state after:
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ ∀ (a : α), (a₂⁻¹ * a₁) • a = a
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: R : Type u_4
S : Type u_5
T : Type u_6
inst✝⁸ : Monoid S
inst✝⁷ : MulOneClass T
inst✝⁶ : SMul R S
inst✝⁵ : SMul R T
inst✝⁴ : MulAction S T
inst✝³ : IsScalarTower R S S
inst✝² : IsScalarTower R T T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul R T
⊢ Injective fun r ↦ r • 1

Tactic:
]

Goal state after:
R : Type u_4
S : Type u_5
T : Type u_6
inst✝⁸ : Monoid S
inst✝⁷ : MulOneClass T
inst✝⁶ : SMul R S
inst✝⁵ : SMul R T
inst✝⁴ : MulAction S T
inst✝³ : IsScalarTower R S S
inst✝² : IsScalarTower R T T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul R T
⊢ Injective fun r ↦ r • 1
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
inst✝¹ : (i : ι) → One (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
h : mulSingle i x = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α✝ : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
M : Type u_9
α : Type u_10
inst✝¹ : CommMonoid M
inst✝ : MulAction M α
a a' : M
b : α
⊢ a' • a • b = a' • a • b

Tactic:
]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ n • MulOpposite.unop m • a = n • MulOpposite.unop m • a

Tactic:
]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ MulOpposite.unop n • m • a = MulOpposite.unop n • m • a

Tactic:
]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul M α
inst✝⁶ : SMul Mᵐᵒᵖ α
inst✝⁵ : IsCentralScalar M α
inst✝⁴ : SMul M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ MulOpposite.unop m • n • a = MulOpposite.unop m • n • a

Tactic:
]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁵ : SMul M α
inst✝⁴ : SMul M N
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • MulOpposite.unop n • a = m • MulOpposite.unop n • a

Tactic:
]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ a • c • b • d = a • c • b • d

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t ↦ rec fa fb t) ↔
    ∃ fa fb, p fun t ↦ rec fa fb t

Tactic:
]

Goal state after:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t ↦ rec fa fb t) ↔
    ∃ fa fb, p fun t ↦ rec fa fb t
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • (b * x) = r • (b * x)

Tactic:
]

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

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
x : α
⊢ (fun x ↦ a ^ n • x) x = a ^ n • x

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update f (inr i) x (inr j) = update f (inr i) x (inr j)

Tactic:
]

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ s • r • x = s • r • x

Tactic:
]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ r ^ (n + 1) • x ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)

Tactic:
]

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ a = a

Tactic:
]

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
⊢ a = a

Tactic:
]

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g • b
⊢ b = b

Tactic:
]

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g⁻¹ • b
⊢ b = b

Tactic:
]

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g • a = b
⊢ a = a

Tactic:
]

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

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ s • r • x = s • r • x

Tactic:
]

Goal state after: