mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : x ∈ s
⊢ s.piecewise f f x = f x

pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : ¬x ∈ s
⊢ s.piecewise f f x = f x

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : x ∈ s
⊢ s.piecewise f f x = f x

case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : ¬x ∈ s
⊢ s.piecewise f f x = f x
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
x : α
⊢ Sum.inl x ∈ range Sum.inl

pp: case inr
α : Type u_1
β : Type u_2
y : β
⊢ Sum.inr y ∈ range Sum.inr

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
x : α
⊢ Sum.inl x ∈ range Sum.inl

case inr
α : Type u_1
β : Type u_2
y : β
⊢ Sum.inr y ∈ range Sum.inr
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ s.piecewise f g x ∈ f '' s

pp: case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ s.piecewise f g x ∈ g '' sᶜ

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ s.piecewise f g x ∈ f '' s

case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ s.piecewise f g x ∈ g '' sᶜ
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ x ∈ s ∧ f x = s.piecewise f g x

pp: case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ x ∈ sᶜ ∧ g x = s.piecewise f g x

Tactic:
<;>

Goal state after:
case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ x ∈ s ∧ f x = s.piecewise f g x

case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ x ∈ sᶜ ∧ g x = s.piecewise f g x
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case mpr.inl
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ f x ∈ range (s.piecewise f g)

pp: case mpr.inr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ g x ∈ range (s.piecewise f g)

Tactic:
<;>

Goal state after:
case mpr.inl
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ f x ∈ range (s.piecewise f g)

case mpr.inr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ g x ∈ range (s.piecewise f g)
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ s.piecewise f g x = f x

pp: case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ s.piecewise f g x = g x

Tactic:
<;>

Goal state after:
case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ s.piecewise f g x = f x

case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ s.piecewise f g x = g x
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val✝ : α
⊢ Sum.inl val✝ ∈ Sum.elim f g ⁻¹' s ↔ Sum.inl val✝ ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val✝ : β
⊢ Sum.inr val✝ ∈ Sum.elim f g ⁻¹' s ↔ Sum.inr val✝ ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val✝ : α
⊢ Sum.inl val✝ ∈ Sum.elim f g ⁻¹' s ↔ Sum.inl val✝ ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val✝ : β
⊢ Sum.inr val✝ ∈ Sum.elim f g ⁻¹' s ↔ Sum.inr val✝ ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
i : α
ht : i ∈ t
hs : i ∈ s
⊢ s.piecewise f g i ∈ t' i

pp: case neg
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
i : α
ht : i ∈ t
hs : ¬i ∈ s
⊢ s.piecewise f g i ∈ t' i

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
i : α
ht : i ∈ t
hs : i ∈ s
⊢ s.piecewise f g i ∈ t' i

case neg
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
i : α
ht : i ∈ t
hs : ¬i ∈ s
⊢ s.piecewise f g i ∈ t' i
Module: Mathlib.Algebra.Group.Action.Pi

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h✝ : ∃ a, f a = x
⊢ r • g (Classical.choose ⋯) = r • g (Classical.choose h✝)

pp: case neg
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h✝ : ¬∃ a, f a = x
⊢ r • e x = r • e x

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h✝ : ∃ a, f a = x
⊢ r • g (Classical.choose ⋯) = r • g (Classical.choose h✝)

case neg
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h✝ : ¬∃ a, f a = x
⊢ r • e x = r • e x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mp.inl.inl
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h2 : ¬x.1 = x.2
h1 : x.2 ∈ s
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

pp: case mp.inl.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h2 : ¬x.1 = x.2
h1 : x.2 ∈ t
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

pp: case mp.inr.inl
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h2 : ¬x.1 = x.2
h1 : x.2 ∈ s
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

pp: case mp.inr.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h2 : ¬x.1 = x.2
h1 : x.2 ∈ t
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
<;>

Goal state after:
case mp.inl.inl
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h2 : ¬x.1 = x.2
h1 : x.2 ∈ s
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

case mp.inl.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h2 : ¬x.1 = x.2
h1 : x.2 ∈ t
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

case mp.inr.inl
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h2 : ¬x.1 = x.2
h1 : x.2 ∈ s
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

case mp.inr.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h2 : ¬x.1 = x.2
h1 : x.2 ∈ t
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mpr.inl.inl.inl
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ s
h2 : ¬x.1 = x.2
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

pp: case mpr.inl.inl.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ t
h2 : ¬x.1 = x.2
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

pp: case mpr.inl.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ t
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

pp: case mpr.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ s
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Tactic:
<;>

Goal state after:
case mpr.inl.inl.inl
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ s
h2 : ¬x.1 = x.2
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

case mpr.inl.inl.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ t
h2 : ¬x.1 = x.2
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

case mpr.inl.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ t
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

case mpr.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ s
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h✝ : IsEmpty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

pp: case inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h✝ : Nonempty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h✝ : IsEmpty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

case inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h✝ : Nonempty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case refine_1.left
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁

pp: case refine_1.right
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂

Tactic:
<;>

Goal state after:
case refine_1.left
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁

case refine_1.right
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ {i | i ∈ s ∧ p i}.pi t₁
ht₂ : f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
i : ι
his : i ∈ s
h✝ : p i
⊢ f i ∈ (fun i ↦ if p i then t₁ i else t₂ i) i

pp: case neg
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ {i | i ∈ s ∧ p i}.pi t₁
ht₂ : f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
i : ι
his : i ∈ s
h✝ : ¬p i
⊢ f i ∈ (fun i ↦ if p i then t₁ i else t₂ i) i

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ {i | i ∈ s ∧ p i}.pi t₁
ht₂ : f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
i : ι
his : i ∈ s
h✝ : p i
⊢ f i ∈ (fun i ↦ if p i then t₁ i else t₂ i) i

case neg
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ {i | i ∈ s ∧ p i}.pi t₁
ht₂ : f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
i : ι
his : i ∈ s
h✝ : ¬p i
⊢ f i ∈ (fun i ↦ if p i then t₁ i else t₂ i) i
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ¬f none ∈ range (f ∘ some)

Tactic:
simp only [mem_range, not_exists, (· ∘ ·)]
  refine
    ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, ?_⟩
  rintro ⟨h_some, h_none⟩ (_ | a) (_ | b) hab
  exacts [rfl, (h_none _ hab.symm).elim, (h_none _ hab).elim, congr_arg some (h_some hab)]

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
hf : f ∈ s.pi t
j : ι
hj : j ∈ s
y : α j
hy : y ∈ t j
⊢ update f j y j ∈ t j

pp: case inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
hji : j ≠ i
⊢ update f i y j ∈ t j

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
hf : f ∈ s.pi t
j : ι
hj : j ∈ s
y : α j
hy : y ∈ t j
⊢ update f j y j ∈ t j

case inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
hji : j ≠ i
⊢ update f i y j ∈ t j
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case zero
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
⊢ (⇑f)^[0] = ⇑(npowRec 0 f)

pp: case succ
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ (⇑f)^[n✝ + 1] = ⇑(npowRec (n✝ + 1) f)

Tactic:
<;>

Goal state after:
case zero
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
⊢ (⇑f)^[0] = ⇑(npowRec 0 f)

case succ
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ (⇑f)^[n✝ + 1] = ⇑(npowRec (n✝ + 1) f)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case zero
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
⊢ id = ⇑1

pp: case succ
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ ⇑(npowRec n✝ f) ∘ ⇑f = ⇑(npowRec n✝ f * f)

Tactic:
<;>

Goal state after:
case zero
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
⊢ id = ⇑1

case succ
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝ : MulOne M
f : Monoid.End M
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ ⇑(npowRec n✝ f) ∘ ⇑f = ⇑(npowRec n✝ f * f)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) t

Tactic:
by
  refine ⟨?_, h.rightInvOn_invFunOn⟩
  rintro _ ⟨y, hy, rfl⟩
  rw [h.rightInvOn_invFunOn hy]

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

Goal state before:
pp: case inl
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
a : M
⊢ a ^ 0 = 1 ↔ a = 1 ∨ 0 = 0

pp: case inr
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
<;>

Goal state after:
case inl
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
a : M
⊢ a ^ 0 = 1 ↔ a = 1 ∨ 0 = 0

case inr
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: case inl
G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a ^ 0 = 1 ↔ a = 1 ∨ 0 = 0

pp: case inr
G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
<;>

Goal state after:
case inl
G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a ^ 0 = 1 ↔ a = 1 ∨ 0 = 0

case inr
G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
⊢ (swap x b) x ∈ s ↔ x ∈ s

pp: case inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
⊢ (swap a b) x ∈ s ↔ x ∈ s

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
⊢ (swap x b) x ∈ s ↔ x ∈ s

case inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
⊢ (swap a b) x ∈ s ↔ x ∈ s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case inl.inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
x : α
ha hb : x ∈ s
⊢ (swap x x) x ∈ s ↔ x ∈ s

pp: case inl.inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
hxb : x ≠ b
⊢ (swap x b) x ∈ s ↔ x ∈ s

pp: case inr.inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a : α
ha : a ∈ s
x : α
hxa : x ≠ a
hb : x ∈ s
⊢ (swap a x) x ∈ s ↔ x ∈ s

pp: case inr.inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
hxb : x ≠ b
⊢ (swap a b) x ∈ s ↔ x ∈ s

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
x : α
ha hb : x ∈ s
⊢ (swap x x) x ∈ s ↔ x ∈ s

case inl.inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
hxb : x ≠ b
⊢ (swap x b) x ∈ s ↔ x ∈ s

case inr.inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a : α
ha : a ∈ s
x : α
hxa : x ≠ a
hb : x ∈ s
⊢ (swap a x) x ∈ s ↔ x ∈ s

case inr.inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
hxb : x ≠ b
⊢ (swap a b) x ∈ s ↔ x ∈ s
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
h✝ : p
⊢ a ^ b h✝ = a ^ b h✝

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
h✝ : ¬p
⊢ a ^ c h✝ = a ^ c h✝

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
h✝ : p
⊢ a ^ b h✝ = a ^ b h✝

case neg
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
h✝ : ¬p
⊢ a ^ c h✝ = a ^ c h✝
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
h✝ : p
⊢ a h✝ ^ c = a h✝ ^ c

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
h✝ : ¬p
⊢ b h✝ ^ c = b h✝ ^ c

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
h✝ : p
⊢ a h✝ ^ c = a h✝ ^ c

case neg
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
h✝ : ¬p
⊢ b h✝ ^ c = b h✝ ^ c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pos
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

pp: case neg
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

Tactic:
<;>

Goal state after:
case pos
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

case neg
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pos
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

pp: case neg
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

Tactic:
<;>

Goal state after:
case pos
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

case neg
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case mp
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 → b = 1

pp: case mpr
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1

Tactic:
<;>

Goal state after:
case mp
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 → b = 1

case mpr
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
mul_eq_right

Goal state after:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a = 1 ↔ a = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case ofNat
G : Type u_3
inst✝ : Group G
a : G
a✝ : ℕ
⊢ a ^ (Int.ofNat a✝).natAbs = 1 ↔ a ^ Int.ofNat a✝ = 1

pp: case negSucc
G : Type u_3
inst✝ : Group G
a : G
a✝ : ℕ
⊢ a ^ (Int.negSucc a✝).natAbs = 1 ↔ a ^ Int.negSucc a✝ = 1

Tactic:
<;>

Goal state after:
case ofNat
G : Type u_3
inst✝ : Group G
a : G
a✝ : ℕ
⊢ a ^ (Int.ofNat a✝).natAbs = 1 ↔ a ^ Int.ofNat a✝ = 1

case negSucc
G : Type u_3
inst✝ : Group G
a : G
a✝ : ℕ
⊢ a ^ (Int.negSucc a✝).natAbs = 1 ↔ a ^ Int.negSucc a✝ = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℤ
⊢ P (g ^ n)

Tactic:
by
  induction n with
  | zero => rwa [zpow_zero]
  | succ n ih =>
    rw [zpow_add_one]
    exact h_mul _ ih
  | pred n ih =>
    rw [zpow_sub_one]
    exact h_inv _ ih

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

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : IsMulCommutative M
inst✝ : IsMulCommutative N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).1 = (x✝ * x✝¹).1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : IsMulCommutative M
inst✝ : IsMulCommutative N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).2 = (x✝ * x✝¹).2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : IsMulCommutative M
inst✝ : IsMulCommutative N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).1 = (x✝ * x✝¹).1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : IsMulCommutative M
inst✝ : IsMulCommutative N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).2 = (x✝ * x✝¹).2