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

Goal state before:
pp: case pos
P Q R : Prop
inst✝ : Decidable P
p : P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

pp: case neg
P Q R : Prop
inst✝ : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
<;>

Goal state after:
case pos
P Q R : Prop
inst✝ : Decidable P
p : P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

case neg
P Q R : Prop
inst✝ : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

pp: case neg
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : ¬P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
<;>

Goal state after:
case pos
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

case neg
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : ¬P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
Module: Mathlib.Logic.Basic

Goal state before:
pp: case inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
⊢ x = y

pp: case inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
⊢ x = y

Tactic:
<;>

Goal state after:
case inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
⊢ x = y

case inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
⊢ x = y
Module: Mathlib.Logic.Basic

Goal state before:
pp: case inl.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : p y
⊢ x = y

pp: case inl.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : ¬p y
⊢ x = y

pp: case inr.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : p y
⊢ x = y

pp: case inr.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : ¬p y
⊢ x = y

Tactic:
<;>

Goal state after:
case inl.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : p y
⊢ x = y

case inl.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : ¬p y
⊢ x = y

case inr.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : p y
⊢ x = y

case inr.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : ¬p y
⊢ x = y
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
h : p
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
h : ¬p
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
h : p
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

case neg
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
h : ¬p
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
h : p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
h : ¬p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
h : p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

case neg
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
h : ¬p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ beq1 = BEq.beq

Tactic:
funext x y

Goal state after:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
x y : α
⊢ beq1 x y = (x == y)
Module: Mathlib.Logic.Unique

Goal state before:
pp: case left
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α

pp: case right
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Nonempty α

Tactic:
<;>

Goal state after:
case left
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α

case right
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Nonempty α
Module: Mathlib.Logic.Unique

Goal state before:
pp: case refine_1
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.LeftInverse default f

pp: case refine_2
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.RightInverse default f

Tactic:
<;>

Goal state after:
case refine_1
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.LeftInverse default f

case refine_2
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.RightInverse default f
Module: Mathlib.Logic.Unique

Goal state before:
pp: case refine_1
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : A
⊢ default (f x) = x

pp: case refine_2
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : B
⊢ f (default x) = x

Tactic:
<;>

Goal state after:
case refine_1
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : A
⊢ default (f x) = x

case refine_2
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : B
⊢ f (default x) = x
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case inl
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
b : β
a : α
⊢ update f a b a = if a = a then b else f a

pp: case inr
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
hne : a ≠ a'
⊢ update f a' b a = if a = a' then b else f a

Tactic:
<;>

Goal state after:
case inl
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
b : β
a : α
⊢ update f a b a = if a = a then b else f a

case inr
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
hne : a ≠ a'
⊢ update f a' b a = if a = a' then b else f a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case inl
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
j : ι
a : α j
⊢ Pi.map f (update g j a) j = update (Pi.map f g) j (f j a) j

pp: case inr
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
hij : j ≠ i
⊢ Pi.map f (update g i a) j = update (Pi.map f g) i (f i a) j

Tactic:
<;>

Goal state after:
case inl
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
j : ι
a : α j
⊢ Pi.map f (update g j a) j = update (Pi.map f g) j (f j a) j

case inr
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
hij : j ≠ i
⊢ Pi.map f (update g i a) j = update (Pi.map f g) i (f i a) j
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
⊢ curry (update f (a, a₂') b) a a' = update (curry f) (a, a₂').fst (update (curry f (a, a₂').fst) (a, a₂').snd b) a a'

pp: case inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
⊢ curry (update f (a, a₂') b) a a' = update (curry f) (a, a₂').fst (update (curry f (a, a₂').fst) (a, a₂').snd b) a a'

case inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case inl.inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
⊢ curry (update f (a, a') b) a a' = update (curry f) (a, a').fst (update (curry f (a, a').fst) (a, a').snd b) a a'

pp: case inl.inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
ha' : a' ≠ a₂'
⊢ curry (update f (a, a₂') b) a a' = update (curry f) (a, a₂').fst (update (curry f (a, a₂').fst) (a, a₂').snd b) a a'

pp: case inr.inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
ha : a ≠ a₂
⊢ curry (update f (a₂, a') b) a a' = update (curry f) (a₂, a').fst (update (curry f (a₂, a').fst) (a₂, a').snd b) a a'

pp: case inr.inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
ha' : a' ≠ a₂'
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
⊢ curry (update f (a, a') b) a a' = update (curry f) (a, a').fst (update (curry f (a, a').fst) (a, a').snd b) a a'

case inl.inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
ha' : a' ≠ a₂'
⊢ curry (update f (a, a₂') b) a a' = update (curry f) (a, a₂').fst (update (curry f (a, a₂').fst) (a, a₂').snd b) a a'

case inr.inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
ha : a ≠ a₂
⊢ curry (update f (a₂, a') b) a a' = update (curry f) (a₂, a').fst (update (curry f (a₂, a').fst) (a₂, a').snd b) a a'

case inr.inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
ha' : a' ≠ a₂'
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
Module: Mathlib.Data.FunLike.Equiv

Goal state before:
pp: case mp
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
a : α
⊢ inv e b = a → b = e a

pp: case mpr
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
a : α
⊢ b = e a → inv e b = a

Tactic:
<;>

Goal state after:
case mp
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
a : α
⊢ inv e b = a → b = e a

case mpr
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
a : α
⊢ b = e a → inv e b = a
Module: Mathlib.Data.FunLike.Basic

Goal state before:
pp: case pos
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
h✝ : P
⊢ (f h✝) x = (f h✝) x

pp: case neg
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
h✝ : ¬P
⊢ (g h✝) x = (g h✝) x

Tactic:
<;>

Goal state after:
case pos
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
h✝ : P
⊢ (f h✝) x = (f h✝) x

case neg
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
h✝ : ¬P
⊢ (g h✝) x = (g h✝) x
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b : α
⊢ b = b ∨ ∃ c, r b c ∧ ReflTransGen r c b

pp: case head
α : Type u_1
r : α → α → Prop
a b a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ a✝¹ = b ∨ ∃ c, r a✝¹ c ∧ ReflTransGen r c b

Tactic:
<;>

Goal state after:
case refl
α : Type u_1
r : α → α → Prop
a b : α
⊢ b = b ∨ ∃ c, r b c ∧ ReflTransGen r c b

case head
α : Type u_1
r : α → α → Prop
a b a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ a✝¹ = b ∨ ∃ c, r a✝¹ c ∧ ReflTransGen r c b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case trans
α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ a b c : α
a✝¹ : EqvGen r a b
a✝ : EqvGen r b c
hab : EqvGen p a b
hbc : EqvGen p b c
⊢ EqvGen p a c

Tactic:
| trans a b c _ _ hab hbc =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
⊢ EqvGen r ≤ EqvGen p

Tactic:
intro _ _ h
  induction h with
  | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
  | refl => exact EqvGen.refl _
  | symm a b _ ih => exact EqvGen.symm _ _ ih
  | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc

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

Goal state before:
pp: case zero
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
⊢ (Pi.map f)^[0] = Pi.map fun i ↦ (f i)^[0]

pp: case succ
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n✝ : ℕ
a✝ : (Pi.map f)^[n✝] = Pi.map fun i ↦ (f i)^[n✝]
⊢ (Pi.map f)^[n✝ + 1] = Pi.map fun i ↦ (f i)^[n✝ + 1]

Tactic:
<;>

Goal state after:
case zero
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
⊢ (Pi.map f)^[0] = Pi.map fun i ↦ (f i)^[0]

case succ
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n✝ : ℕ
a✝ : (Pi.map f)^[n✝] = Pi.map fun i ↦ (f i)^[n✝]
⊢ (Pi.map f)^[n✝ + 1] = Pi.map fun i ↦ (f i)^[n✝ + 1]
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: case inl
α : Type u
β : Type v
a val✝ : α
⊢ inl val✝ = inl a ↔ ∃ h, (inl val✝).getLeft h = a

pp: case inr
α : Type u
β : Type v
a : α
val✝ : β
⊢ inr val✝ = inl a ↔ ∃ h, (inr val✝).getLeft h = a

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
a val✝ : α
⊢ inl val✝ = inl a ↔ ∃ h, (inl val✝).getLeft h = a

case inr
α : Type u
β : Type v
a : α
val✝ : β
⊢ inr val✝ = inl a ↔ ∃ h, (inr val✝).getLeft h = a
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: case inl
α : Type u
β : Type v
b : β
val✝ : α
⊢ inl val✝ = inr b ↔ ∃ h, (inl val✝).getRight h = b

pp: case inr
α : Type u
β : Type v
b val✝ : β
⊢ inr val✝ = inr b ↔ ∃ h, (inr val✝).getRight h = b

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
b : β
val✝ : α
⊢ inl val✝ = inr b ↔ ∃ h, (inl val✝).getRight h = b

case inr
α : Type u
β : Type v
b val✝ : β
⊢ inr val✝ = inr b ↔ ∃ h, (inr val✝).getRight h = b
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ (inl a✝¹).isLeft = true ↔ (inl c✝).isLeft = true

pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ (inr b✝).isLeft = true ↔ (inr d✝).isLeft = true

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ (inl a✝¹).isLeft = true ↔ (inl c✝).isLeft = true

case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ (inr b✝).isLeft = true ↔ (inr d✝).isLeft = true
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ (inl a✝¹).isRight = true ↔ (inl c✝).isRight = true

pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ (inr b✝).isRight = true ↔ (inr d✝).isRight = true

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ (inl a✝¹).isRight = true ↔ (inl c✝).isRight = true

case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ (inr b✝).isRight = true ↔ (inr d✝).isRight = true
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: case ofNat
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
a✝ : ℕ
⊢ (g • a) ^ Int.ofNat a✝ = g ^ Int.ofNat a✝ • a ^ Int.ofNat a✝

pp: case negSucc
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
a✝ : ℕ
⊢ (g • a) ^ Int.negSucc a✝ = g ^ Int.negSucc a✝ • a ^ Int.negSucc a✝

Tactic:
<;>

Goal state after:
case ofNat
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
a✝ : ℕ
⊢ (g • a) ^ Int.ofNat a✝ = g ^ Int.ofNat a✝ • a ^ Int.ofNat a✝

case negSucc
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
a✝ : ℕ
⊢ (g • a) ^ Int.negSucc a✝ = g ^ Int.negSucc a✝ • a ^ Int.negSucc a✝
Module: Mathlib.Data.Option.Defs

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Option.elim' (f none) (f ∘ some) none = f none

pp: case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ Option.elim' (f none) (f ∘ some) (some val✝) = f (some val✝)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Option.elim' (f none) (f ∘ some) none = f none

case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ Option.elim' (f none) (f ∘ some) (some val✝) = f (some val✝)
Module: Mathlib.Data.Option.Defs

Goal state before:
pp: case none
α : Type u_3
β : Type u_4
b : β
f : α → β
⊢ Option.elim' b f none = none.elim b f

pp: case some
α : Type u_3
β : Type u_4
b : β
f : α → β
val✝ : α
⊢ Option.elim' b f (some val✝) = (some val✝).elim b f

Tactic:
<;>

Goal state after:
case none
α : Type u_3
β : Type u_4
b : β
f : α → β
⊢ Option.elim' b f none = none.elim b f

case some
α : Type u_3
β : Type u_4
b : β
f : α → β
val✝ : α
⊢ Option.elim' b f (some val✝) = (some val✝).elim b f
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ (x • y) • z = x • y • z

Tactic:
by rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]

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

Goal state before:
pp: case none
α : Type u_1
inst✝ : Inhabited α
⊢ none.getD default = none.iget

pp: case some
α : Type u_1
inst✝ : Inhabited α
val✝ : α
⊢ (some val✝).getD default = (some val✝).iget

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : Inhabited α
⊢ none.getD default = none.iget

case some
α : Type u_1
inst✝ : Inhabited α
val✝ : α
⊢ (some val✝).getD default = (some val✝).iget
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ none.casesOn' (f none) (f ∘ fun a ↦ some a) = f none

pp: case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ (some val✝).casesOn' (f none) (f ∘ fun a ↦ some a) = f (some val✝)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ none.casesOn' (f none) (f ∘ fun a ↦ some a) = f none

case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ (some val✝).casesOn' (f none) (f ∘ fun a ↦ some a) = f (some val✝)
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ none.casesOn' b f = none.elim b f

pp: case some
α : Type u_1
β : Type u_2
b : β
f : α → β
val✝ : α
⊢ (some val✝).casesOn' b f = (some val✝).elim b f

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ none.casesOn' b f = none.elim b f

case some
α : Type u_1
β : Type u_2
b : β
f : α → β
val✝ : α
⊢ (some val✝).casesOn' b f = (some val✝).elim b f
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ none.elim (f none) (f ∘ some) = f none

pp: case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ (some val✝).elim (f none) (f ∘ some) = f (some val✝)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ none.elim (f none) (f ∘ some) = f none

case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ (some val✝).elim (f none) (f ∘ some) = f (some val✝)
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
⊢ (none.elim (h x) fun j ↦ h (f j)) = h (none.elim x f)

pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
val✝ : γ
⊢ ((some val✝).elim (h x) fun j ↦ h (f j)) = h ((some val✝).elim x f)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
⊢ (none.elim (h x) fun j ↦ h (f j)) = h (none.elim x f)

case some
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
val✝ : γ
⊢ ((some val✝).elim (h x) fun j ↦ h (f j)) = h ((some val✝).elim x f)