mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: n : Nat
⊢ bit (n.testBit 0) (n >>> 1) = n

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: n : Nat
b : Bool
⊢ bit b n ≠ 0 ↔ n = 0 → b = true

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: b : Bool
n : Nat
⊢ (bit b n).testBit 0 = b

Tactic:
by
  simp

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

Goal state before:
pp: G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -((n + 1) • a)

Tactic:
rw [← natCast_zsmul]

Goal state after:
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -(↑(n + 1) • a)
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
⊢ Nontrivial α

Tactic:
rcases hf x with ⟨x', hx'⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
⊢ Nontrivial α
Module: Mathlib.Logic.Function.Basic

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

Tactic:
simpa using congr_fun this b₀

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
⊢ c = c'

Tactic:
have ⟨a₁, a₂, eq, ne⟩ := not_inj

Goal state after:
α : 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₂
⊢ c = c'
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ab : ReflTransGen r a b
ac : ReflTransGen r a c
⊢ ReflTransGen r b c ∨ ReflTransGen r c b

Tactic:
by
  induction ab with
  | refl => exact Or.inl ac
  | tail _ bd IH =>
    rcases IH with (IH | IH)
    · rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
      · exact Or.inr (single bd)
      · cases U bd be
        exact Or.inl ec
    · exact Or.inr (IH.tail bd)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : Function.swap (TransGen r) i✝¹ i✝
⊢ TransGen (Function.swap r) i✝¹ i✝

Tactic:
induction h with
  | single h => exact TransGen.single h
  | tail _ hbc ih => exact ih.head hbc

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case trans
α : Type u_1
r : α → α → Prop
i✝¹ i✝ a✝ b✝ c✝ : α
h₁✝ : TransGen r a✝ b✝
h₂✝ : TransGen r b✝ c✝
h1 : EqvGen r a✝ b✝
h2 : EqvGen r b✝ c✝
⊢ EqvGen r a✝ c✝

Tactic:
exact _root_.trans h1 h2

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case trans
α : Type u_1
r : α → α → Prop
i✝¹ i✝ a✝ b✝ c✝ : α
h₁✝ : ReflTransGen r a✝ b✝
h₂✝ : ReflTransGen r b✝ c✝
h1 : EqvGen r a✝ b✝
h2 : EqvGen r b✝ c✝
⊢ EqvGen r a✝ c✝

Tactic:
exact _root_.trans h1 h2

Goal state after:
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 + 1 + k))

Tactic:
| succ n ihn =>

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

Goal state before:
pp: case succ
α : Type u
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
⊢ (f ∘ g)^[n + 1] = f^[n + 1] ∘ g^[n + 1]

Tactic:
| succ n ihn =>

Goal state after:
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
⊢ FaithfulSMul R S

Tactic:
by
  rw [faithfulSMul_iff_injective_smul_one]
  refine .of_comp (f := (· • (1 : T))) ?_
  simpa [Function.comp_def, one_smul, ← faithfulSMul_iff_injective_smul_one]

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
⊢ r • s • x = s • r • x

Tactic:
← one_smul G (s • x),

Goal state after:
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
⊢ r • 1 • s • x = s • r • x
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
o o' : Option α
x : α
⊢ (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
o o' : Option α
⊢ (o <|> o') = none ↔ o = none ∧ o' = none

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b

Tactic:
cases h : compare a b
  · simpa using le_of_lt <| compare_lt_iff_lt.1 h
  · simpa using le_of_eq <| compare_eq_iff_eq.1 h
  · simpa using compare_gt_iff_gt.1 h

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ f (x✝¹ ⊔ x✝) = if f x✝¹ ≤ f x✝ then f x✝ else f x✝¹

Tactic:
← max_def,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ f (x✝¹ ⊔ x✝) = Max.max (f x✝¹) (f x✝)
Module: Mathlib.Tactic.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
y : γ
x : β
hx : condβα (coeβα x, y).fst
hy : condδγ (coeβα x, y).snd
⊢ ∃ y_1, map coeβα coeδγ y_1 = (coeβα x, y)

Tactic:
rcases CanLift.prf (β := δ) y hy with ⟨y, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
x : β
y : δ
hx : condβα (coeβα x, coeδγ y).fst
hy : condδγ (coeβα x, coeδγ y).snd
⊢ ∃ y_1, map coeβα coeδγ y_1 = (coeβα x, coeδγ y)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
⊢ (Monotone fun n ↦ f (n + k)) ↔ MonotoneOn f {x | k ≤ x}

Tactic:
refine ⟨fun h x hx y hy hle ↦ ?_, fun h x y hle ↦ ?_⟩

Goal state after:
case refine_1
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : Monotone fun n ↦ f (n + k)
x : ℕ
hx : x ∈ {x | k ≤ x}
y : ℕ
hy : y ∈ {x | k ≤ x}
hle : x ≤ y
⊢ f x ≤ f y

case refine_2
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle : x ≤ y
⊢ (fun n ↦ f (n + k)) x ≤ (fun n ↦ f (n + k)) y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + ↑(n + 1).succ))

Tactic:
| succ n ihn =>

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
hba : b ⊓ a = a
hab : a ⊓ b = b
⊢ a = b

Tactic:
by rwa [← hba, inf_comm]

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s

Tactic:
disjoint_comm,

Goal state after:
α : Type u
s t : Set α
⊢ Disjoint t s ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
a b : α
⊢ Disjoint {a} {b} ↔ a ≠ b

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ Disjoint s (insert a t) ↔ ¬a ∈ s ∧ Disjoint s t

Tactic:
disjoint_comm,

Goal state after:
α : Type u_1
s t : Set α
a : α
⊢ Disjoint (insert a t) s ↔ ¬a ∈ s ∧ Disjoint s t
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
⊢ SemilatticeInf α

Tactic:
apply e.injective.semilatticeInf

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e y ≤ e x ↔ y ≤ x

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e y < e x ↔ y < x

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Option α ≃ Option β
h : e.symm none = none
⊢ e none = none

Tactic:
simpa using (congr_arg e h).symm

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ s \ {a} ⊆ t ↔ s ⊆ insert a t

Tactic:
by
  simp

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

Goal state before:
pp: α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ Surjective (Sigma.map f₁ f₂)

Tactic:
simp only [Surjective, Sigma.forall, h₁.forall]
  exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩

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

Goal state before:
pp: case inr
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ update f ⟨ia, ib⟩ x ⟨ja, jb⟩ =
    update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb

Tactic:
rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]
    · exact ha.symm
    · exact ha.symm

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z) = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)

Tactic:
inf_sup_left y

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z) = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ c ⊓ a \ b = (c ⊓ a) \ (c ⊓ b)

Tactic:
inf_sdiff_distrib_left

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⊓ y ⊔ x ⊓ yᶜ = x

Tactic:
← sdiff_eq,

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⊓ y ⊔ x \ y = x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ (x ⊓ yᶜ)ᶜ = y ⊔ xᶜ

Tactic:
compl_inf,

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊔ yᶜᶜ = y ⊔ xᶜ
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤

Tactic:
hnot_symmDiff_self

Goal state after:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ = ⊤
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
h : IsCompl a b
⊢ (￢b) ∆ b = ⊤

Tactic:
hnot_symmDiff_self

Goal state after:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
h : IsCompl a b
⊢ ⊤ = ⊤
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))

Tactic:
rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
compl_inf

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ univ ×ˢ univ = univ

Tactic:
by
  ext
  exact iff_of_eq (true_and _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Surjective f
⊢ f '' (s ∪ sᶜ) = univ

Tactic:
simp [image_univ_of_surjective H]

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

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

Tactic:
disjoint_comm,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ), x ∈ range m₁ ×ˢ range m₂ ↔ x ∈ range fun p ↦ (m₁ p.1, m₂ p.2)

Tactic:
simp [range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m₁ : α → γ
⊢ ∀ (x : γ × β), x ∈ range m₁ ×ˢ univ ↔ x ∈ range fun p ↦ (m₁ p.1, p.2)

Tactic:
simp [range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
m₂ : β → δ
⊢ ∀ (x : α × δ), x ∈ univ ×ˢ range m₂ ↔ x ∈ range fun p ↦ (p.1, m₂ p.2)

Tactic:
simp [range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)

Tactic:
refine (h₁.congr ?_).union_union (h₂.congr ?_)

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₁ (s.piecewise f₁ f₂) (s₁ ∩ s)

case refine_2
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₂ (s.piecewise f₁ f₂) (s₂ ∩ sᶜ)
Module: Mathlib.Data.Set.Image

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

Tactic:
exact mem_range_self _

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

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

Tactic:
exact mem_range_self _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : α → β
hf : Injective fun i ↦ f ↑i
⊢ ∃ f, InjOn f s

Tactic:
exact ⟨f, injOn_iff_injective.2 hf⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
⊢ BijOn f (s ∩ f ⁻¹' r) r

Tactic:
by
  refine ⟨inter_subset_right, hf.injOn.mono inter_subset_left, fun x hx ↦ ?_⟩
  obtain ⟨y, hy, rfl⟩ := hf.surjOn (hrt hx)
  exact ⟨y, ⟨hy, hx⟩, rfl⟩

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

Goal state before:
pp: case succ
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:
| succ n ihn =>

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ c * a / (c * b) = a / b

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
⊢ ↑a * ↑a⁻¹ = 1

Tactic:
mul_inv

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b✝ u a b : αˣ
⊢ ↑a * ↑a⁻¹ = 1

Tactic:
mul_inv

Goal state after:
α : Type u
inst✝ : Monoid α
a✝ b✝ u a b : αˣ
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b✝ u a b : αˣ
⊢ ↑b * ↑b⁻¹ = 1

Tactic:
mul_inv

Goal state after:
α : Type u
inst✝ : Monoid α
a✝ b✝ u a b : αˣ
⊢ 1 = 1
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> ((fun b a ↦ (a, b)) <$> b <*> a) = (fun b a ↦ f a b) <$> b <*> a

Tactic:
simp [map_seq, map_map]

Goal state after:
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun a ↦ (fun p ↦ f p.fst p.snd) ∘ fun a_1 ↦ (a_1, a)) <$> b <*> a = (fun b a ↦ f a b) <$> b <*> a
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: G : Type u_3
inst✝ : AddGroup G
g h : G
⊢ (-addConj g) h = -g + h + g

Tactic:
by
  simp

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

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

Tactic:
rw [Nat.binCast]

Goal state after:
case ind.succ
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case succ
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)

Tactic:
| succ n ihn =>

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

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

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0
  · simp
  · rw [sq, mul_assoc, mul_div_cancel_left₀ _ ha]

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
h : m ≤ n
⊢ ↑(n - m) + ↑m = ↑n

Tactic:
rw [← cast_add, Nat.sub_add_cancel h]

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(-[m+1] + -[n+1]) = ↑-[m+1] + ↑-[n+1]

Tactic:
by
    rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]

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

Goal state before:
pp: case succ
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
n : ℕ
ihn : f n = g n
⊢ f (n + 1) = g (n + 1)

Tactic:
| succ n ihn =>

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * x * x⁻¹ʳ = y

Tactic:
rw [mul_assoc, mul_inverse_cancel x h, mul_one]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑(n + 1)) x

Tactic:
| succ n ihn =>

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
⊢ f = g

Tactic:
ext (x | x)

Goal state after:
case ofNat
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (ofNat x) = g (ofNat x)

case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f -[x+1] = g -[x+1]
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective f✝
inst✝²⁰ : Add S✝
inst✝¹⁹ : Mul S✝
inst✝¹⁸ : Zero S✝
inst✝¹⁷ : One S✝
inst✝¹⁶ : Neg S✝
inst✝¹⁵ : Sub S✝
inst✝¹⁴ : SMul ℕ S✝
inst✝¹³ : SMul ℤ S✝
inst✝¹² : Pow S✝ ℕ
inst✝¹¹ : NatCast S✝
inst✝¹⁰ : IntCast S✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑(Int.negSucc n) = f (-↑(n + 1))

Tactic:
rw [intCast, neg, natCast, Int.cast_negSucc]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a = 2 * b + 1 ↔ a = 2 * b + 1

Tactic:
two_mul

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a = b + b + 1 ↔ a = b + b + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a + a + 1 + (2 * b + 1) = a + b + 1 + (a + b + 1)

Tactic:
two_mul

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a + a + 1 + (b + b + 1) = a + b + 1 + (a + b + 1)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b - c ≤ a + (b - c)

Tactic:
grw [tsub_le_iff_left, add_left_comm, ← le_add_tsub]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a

Tactic:
· exact mul_lt_mul_left (h.lt_of_ne h') a |>.ne

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ e.toEmbedding.trans e.symm.toEmbedding = Embedding.refl α

Tactic:
by
  simp

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ e.symm.toEmbedding.trans e.toEmbedding = Embedding.refl β

Tactic:
by
  simp

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
by rw [div_le_iff₀ hb, one_mul]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 4 * r ^ 2 ≤ (a + b) * (a + b)

Tactic:
grw [mul_le_mul_of_nonneg_left ht zero_le_four, ← mul_assoc, four_mul_le_sq_add a b, sq]

Goal state after: