mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)

Tactic:
bihimp_assoc,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ (b ⇔ (c ⇔ d)) = a ⇔ (c ⇔ (b ⇔ d))
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ∆ b)ᶜ = a ⇔ b

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ∆ b)ᶜ = a ⇔ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ a ∆ b ⊔ a ∆ c

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ a ∆ b ⊔ a ∆ c
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s \ f ⁻¹' t) = f '' s \ t

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s \ f ⁻¹' t) = f '' s \ t
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Injective (codRestrict f s h) ↔ Injective f

Tactic:
by
  simp only [Injective, Subtype.ext_iff, val_codRestrict_apply]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
⊢ Surjective (codRestrict f (range f) ⋯)

Tactic:
by
  rintro ⟨b, ⟨a, rfl⟩⟩
  exact ⟨a, rfl⟩

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

Goal state before:
pp: case mp
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s → t ∈ 𝒫 s ∪ insert a '' 𝒫 s

pp: case mpr
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s → t ∈ 𝒫 insert a s

Tactic:
· intro h
    by_cases hs : a ∈ t
    · right
      refine ⟨t \ {a}, by grind⟩
    · grind

Goal state after:
case mpr
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s → t ∈ 𝒫 insert a s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
⊢ range f = {y} ↔ ∀ (x : ι), f x = y

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
⊢ range f = {y} ↔ ∀ (x : ι), f x = y
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : α), (∃ y, f y = x) ↔ x = y
x✝ : ι
⊢ f x✝ = y

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : α), (∃ y, f y = x) ↔ x = y
x✝ : ι
⊢ f x✝ = y
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x✝ : α
⊢ (∃ y, f y = x✝) ↔ x✝ = y

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x✝ : α
⊢ (∃ y, f y = x✝) ↔ x✝ = y
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t t' : Set α
h : EqOn f g (t ∩ s)
h' : EqOn f' g (t' ∩ sᶜ)
⊢ EqOn (s.piecewise f f') g (s.ite t t')

Tactic:
by
  simp [eqOn_piecewise, *]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
[

Goal state after:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Tactic:
[

Goal state after:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ ⟨x, hx⟩ ∈ range (Subtype.map f h) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' f '' {x | p x}

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ ⟨x, hx⟩ ∈ range (Subtype.map f h) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' f '' {x | p x}
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' pullbackDiagonal f ↔ ⟨(p₁, p₂), he⟩ ∈ pullbackDiagonal snd

Tactic:
[

Goal state after:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' pullbackDiagonal f ↔ ⟨(p₁, p₂), he⟩ ∈ pullbackDiagonal snd
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective (image f) ↔ Injective f

Tactic:
refine ⟨fun h x x' hx => ?_, Injective.image_injective⟩

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ x = x'
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
⊢ MapsTo g (p₁ '' s) (p₂ '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
⊢ g (p₁ a) ∈ p₂ '' t
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case negSucc.succ
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i n : ℕ
ih : motive (-↑n)
⊢ motive (-↑(n + 1))

Tactic:
simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using pred _ ih

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : M →* G
a b : M
⊢ (f (a * b))⁻¹ = (f a)⁻¹ * (f b)⁻¹

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : M →* G
a b : M
⊢ (f (a * b))⁻¹ = (f a)⁻¹ * (f b)⁻¹
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Group G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ ∀ (a b : G), a * b = b * a

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Group G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ ∀ (a b : G), a * b = b * a
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (a b : H), a * b = b * a

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (a b : H), a * b = b * a
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((↑m + 1 - 1) / (↑n + 1) + 1)

Tactic:
rw [Int.add_sub_cancel]

Goal state after:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -(↑m / (↑n + 1) + 1)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
⊢ ∃ u, u ⊆ s ∧ InjOn f u ∧ f '' u = t

Tactic:
exact ⟨range (fun a : t ↦ x a.2), by grind, fun _ ↦ by grind, by aesop⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
⊢ MapsTo (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) a) ∈ Subtype.val ∘ ⇑f '' t
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (Subtype.val ∘ ⇑f) (g a) = (g.extendDomain f) ((Subtype.val ∘ ⇑f) a)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (Subtype.val ∘ ⇑f) (g a) = (g.extendDomain f) ((Subtype.val ∘ ⇑f) a)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
⊢ SurjOn (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
a : α
ha : a ∈ t
⊢ (Subtype.val ∘ ⇑f) a ∈ ⇑(g.extendDomain f) '' Subtype.val ∘ ⇑f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) b) = (Subtype.val ∘ ⇑f) (g b)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) b) = (Subtype.val ∘ ⇑f) (g b)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
⊢ LeftInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
⊢ RightInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ (f₁ x.1, f₂ x.2) = (f₁ y.1, f₂ y.2) → x = y

Tactic:
[

Goal state after:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ (f₁ x.1, f₂ x.2) = (f₁ y.1, f₂ y.2) → x = y
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ (n - 1) * a = a ^ n

Tactic:
rw [← pow_succ, Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (x✝ ^ ↑x✝¹.succ) = unop (x✝ ^ ↑x✝¹ * x✝)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (x✝ ^ ↑x✝¹.succ) = unop (x✝ ^ ↑x✝¹ * x✝)
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : MulOne α
⊢ IsDedekindFiniteMonoid αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : MulOne α
⊢ IsDedekindFiniteMonoid αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ ↑n = a ^ ↑n * b ^ ↑n

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ ↑n = a ^ ↑n * b ^ ↑n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)

Tactic:
zpow_sub_one,

Goal state after:
case pred
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * (a ^ (-↑n) * a⁻¹)
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑(u₁ / u₂) = ↑u₁ * ↑u₂⁻¹

Tactic:
division_def,

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑(u₁ * u₂⁻¹) = ↑u₁ * ↑u₂⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case hf_swap
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ ∀ {a b : α}, p a ∧ p b → f a b * f b a = 1

Tactic:
[

Goal state after:
case hf_swap
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ ∀ {a b : α}, p a ∧ p b → f a b * f b a = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ f a c = f a b * f b c

Tactic:
by
  have : Std.Symm (p · ∧ p ·) := { symm _ _ := And.symm }
  apply multiplicative_of_symm_of_total (p · ∧ p ·) r f
  · simp_rw [and_imp]; exact @hswap
  · exact fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2
  exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]

Goal state after:
Module: Mathlib.Algebra.Group.Units.Equiv

Goal state before:
pp: G : Type u_6
inst✝ : Group G
x : Gˣ
⊢ toUnits ↑x = x

Tactic:
[

Goal state after:
G : Type u_6
inst✝ : Group G
x : Gˣ
⊢ toUnits ↑x = x
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> (pure f <*> y) = (pure fun x ↦ x ∘ f) <*> x <*> y

Tactic:
simp only [seq_assoc, seq_pure, ← comp_map]

Goal state after:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ ((fun h ↦ h f) ∘ Function.comp) <$> x <*> y = (pure fun x ↦ x ∘ f) <*> x <*> y
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case succ
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
ih : f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
⊢ f.subtypePerm hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm ⋯

Tactic:
[

Goal state after:
case succ
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
ih : f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
⊢ f.subtypePerm hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm ⋯
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case succ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ IsNilpotent (x ^ (n✝ + 1))

Tactic:
| succ =>

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case ind
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k → m.binCast = ↑m
⊢ k.binCast = ↑k

Tactic:
cases k with

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a

Tactic:
inv_mul_cancel₀ h,

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ 1 * a = a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b c : G₀
⊢ a / c * b = a * b / c

Tactic:
[

Goal state after:
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b c : G₀
⊢ a / c * b = a * b / c
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m✝ n m : ℕ
⊢ IsSquare m ↔ m.sqrt * m.sqrt = m

Tactic:
[

Goal state after:
m✝ n m : ℕ
⊢ IsSquare m ↔ m.sqrt * m.sqrt = m
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: m✝ n m : ℤ
⊢ IsSquare m ↔ sqrt m * sqrt m = m

Tactic:
[

Goal state after:
m✝ n m : ℤ
⊢ IsSquare m ↔ sqrt m * sqrt m = m
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case succ
i✝ : ℕ
a✝ : IsSquare (↑i✝).sign ↔ 0 ≤ ↑i✝
⊢ IsSquare (↑i✝ + 1).sign ↔ 0 ≤ ↑i✝ + 1

Tactic:
| succ =>

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: case zero
A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ f 0 = g 0

Tactic:
[

Goal state after:
case zero
A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ f 0 = g 0
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n✝ : ℕ
a✝ : a ^ n✝ ∣ b ^ n✝
⊢ a ^ (n✝ + 1) ∣ b ^ (n✝ + 1)

Tactic:
| succ =>

Goal state after:
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x * (b - x) = c

Tactic:
this

Goal state after:
α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x * (b - x) = x * (b - x)
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsLeftRegular r
r' : R
eq : r * r' = 0
⊢ r * r' = r * 0

Tactic:
[

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsLeftRegular r
r' : R
eq : r * r' = 0
⊢ r * r' = r * 0
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), r * x = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ r * x) r₁ = (fun x ↦ r * x) r₂
⊢ r * (r₁ - r₂) = 0

Tactic:
[

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), r * x = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ r * x) r₁ = (fun x ↦ r * x) r₂
⊢ r * (r₁ - r₂) = 0
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsRightRegular r
r' : R
eq : r' * r = 0
⊢ r' * r = 0 * r

Tactic:
[

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsRightRegular r
r' : R
eq : r' * r = 0
⊢ r' * r = 0 * r
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ x * r) r₁ = (fun x ↦ x * r) r₂
⊢ (r₁ - r₂) * r = 0

Tactic:
[

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ x * r) r₁ = (fun x ↦ x * r) r₂
⊢ (r₁ - r₂) * r = 0
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE

Tactic:
[

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
p : (g : G₀) → g ≠ 0 → Prop
⊢ (∃ g hg, p g hg) ↔ ∃ g hg, p ↑(mk0 g hg) ⋯

Tactic:
[

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
p : (g : G₀) → g ≠ 0 → Prop
⊢ (∃ g hg, p g hg) ↔ ∃ g hg, p ↑(mk0 g hg) ⋯