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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
⊢ binaryRec' zero bit 1 = bit true 0 binaryRec'_one._proof_1 zero

Tactic:
rw [binaryRec', binaryRec_one, dif_pos]

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

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

Tactic:
repeat rw [mul_assoc]

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ ∀ (x : α), (∃ h, q x h) → (∀ (y : α), (∃ h, q y h) → y = x) → b

Tactic:
exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩

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

Goal state before:
pp: α : Type u_1
⊢ Subsingleton α → ∀ (x y : α), x = y

Tactic:
by
    intro h
    exact Subsingleton.elim

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

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

Tactic:
Classical.choose_spec h,

Goal state after:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
h : ∃ e, g = e ∘ f
x✝¹ x✝ : α
hf : f x✝¹ = f x✝
⊢ (Classical.choose h ∘ f) x✝¹ = (Classical.choose h ∘ f) x✝
Module: Mathlib.Logic.Function.Basic

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

Tactic:
sometimes_eq

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

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

Goal state before:
pp: case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a b c : α
inst✝ : Std.Symm r
x y b✝ c✝ : α
a✝ : TransGen r x b✝
h₁ : r b✝ c✝
h₂ : TransGen r b✝ x
⊢ TransGen r c✝ x

Tactic:
| tail _ h₁ h₂ =>

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

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

Tactic:
by
  rw [Perm.subsingleton_eq_refl e, coe_refl]

Goal state after:
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), y * x • 1 = x • y
x : M
y z : N
⊢ x • (y * z) = y • (z * x • 1)

Tactic:
← H,

Goal state after:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ y * z * x • 1 = y • (z * x • 1)
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: a : Bool
⊢ (!a) = false → a = true

Tactic:
by decide +revert

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

Goal state before:
pp: a : Bool
⊢ (!a) = true → a = false

Tactic:
by decide +revert

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

Goal state before:
pp: m n : ℕ
⊢ ¬2 * n % 2 = 1 % 2

Tactic:
mul_mod_right,

Goal state after:
m n : ℕ
⊢ ¬0 = 1 % 2
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c

Tactic:
← H,

Goal state after:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ ¬Disjoint t s ↔ (s ∩ t).Nonempty

Tactic:
rw [not_disjoint_iff_nonempty_inter, inter_comm]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y < x ↔ ¬Disjoint y x

Tactic:
rw [lt_iff_le_and_ne, Ne, sdiff_eq_self_iff_disjoint, and_iff_right sdiff_le]

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

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
⊢ RightInverse
    (fun x ↦
      match x with
      | inl a => ⟨inl ↑a, ⋯⟩
      | inr b => ⟨inr ↑b, ⋯⟩)
    fun x ↦
    match x with
    | ⟨inl a, h⟩ => inl ⟨a, h⟩
    | ⟨inr b, h⟩ => inr ⟨b, h⟩

Tactic:
rintro (a | b) <;> rfl

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π i

Tactic:
rw [← f.2 i]

Goal state after:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π (↑f i).fst
Module: Mathlib.Data.Set.Prod

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

Tactic:
by
  ext ⟨x, y⟩
  simp only [← and_and_right, mem_inter_iff, mem_prod]

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

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

Tactic:
rw [inter_comm, preimage_inter_range]

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

Goal state before:
pp: α : 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 : α
⊢ i ∈ t → s.piecewise f g i ∈ t' i

Tactic:
ht

Goal state after:
α : 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
⊢ s.piecewise f g i ∈ t' i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t : (i : ι) → Set (α i)
⊢ (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t

Tactic:
simp [pi, or_imp, forall_and, ofPred_and]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' s ⊆ f '' (s ∩ t ∪ s \ t)

Tactic:
inter_union_sdiff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' s ⊆ f '' (s ∩ t) ∪ f '' (s \ t)

Tactic:
rw [← image_union, inter_union_sdiff]

Goal state after:
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
⊢ BijOn f (invFunOn f s '' t) t

Tactic:
refine h.invOn_invFunOn.bijOn ?_ (mapsTo_image _ _)
  rintro _ ⟨y, hy, rfl⟩
  rwa [h.rightInvOn_invFunOn hy]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f ((fun x ↦ a✝ * x) x✝¹) = f ((fun x ↦ a✝ * x) x✝)
⊢ x✝¹ = x✝

Tactic:
rw [mul, mul] at this

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
⊢ x✝¹ = x✝
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f ((fun x ↦ x * a✝) x✝¹) = f ((fun x ↦ x * a✝) x✝)
⊢ x✝¹ = x✝

Tactic:
rw [mul, mul] at this

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
⊢ x✝¹ = x✝
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b : G₀
h : a * b = 1
⊢ a⁻¹ = b

Tactic:
← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b : G₀
h : a * b = 1
⊢ a⁻¹ = a⁻¹ * (a * b)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 0 ^ n = 1

pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0

Tactic:
· rw [h, zpow_zero]

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case refine_2
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) (k + 1) m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯) l hl =
    Int.strongRec lt ge l

Tactic:
inductionOn'_add_one hmk

Goal state after:
case refine_2
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ (if hlm : l < m then lt l hlm
    else
      ge l ⋯ fun k_1 x ↦
        Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
          (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯)
          k_1 ⋯) =
    Int.strongRec lt ge l
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case nil
a b : Prop
h_chain : IsChain (fun x1 x2 ↦ x1 → x2) [a, b]
h_last : [].getLastD b → a
⊢ [a, b].TFAE

Tactic:
simp_all [tfae_cons_cons, iff_def]

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

Goal state before:
pp: α : Type u_3
inst✝ : Semiring α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

Tactic:
refine ⟨fun t ↦ ?_, fun h ↦ h.elim (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)⟩

Goal state after:
α : Type u_3
inst✝ : Semiring α
t : IsCancelMulZero α
⊢ IsDomain α ∨ Subsingleton α
Module: Mathlib.Logic.Nontrivial.Basic

Goal state before:
pp: I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)

Tactic:
exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u * (a * ↑u⁻¹) = a

Tactic:
rw [u.commute_iff_mul_inv_cancel, mul_assoc]

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

Goal state before:
pp: n : ℕ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1

Tactic:
by
  simpa only [← two_mul, exists_or, Odd, Even] using even_or_odd n

Goal state after:
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 ≤ a + c + (b - c)

Tactic:
by grw [add_assoc, ← le_add_tsub]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
by
  apply le_antisymm
  · rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
  · rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 2 + 1

Tactic:
exact lt_add_of_lt_of_nonneg zero_lt_two zero_le_one

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 c : G₀
hc : 0 < c
⊢ a < b * c⁻¹ ↔ a * c < b

Tactic:
rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

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 c : G₀
hc : 0 < c
⊢ b * c⁻¹ < a ↔ b < a * c

Tactic:
rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝⁶ : LE α✝
inst✝⁵ : LE β✝
inst✝⁴ : LE γ✝
inst✝³ : LE δ
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
x✝¹ x✝ : (α × β) × γ
fst✝¹ : α
snd✝³ : β
snd✝² : γ
fst✝ : α
snd✝¹ : β
snd✝ : γ
⊢ (Equiv.prodAssoc α β γ) ((fst✝¹, snd✝³), snd✝²) ≤ (Equiv.prodAssoc α β γ) ((fst✝, snd✝¹), snd✝) ↔
    ((fst✝¹, snd✝³), snd✝²) ≤ ((fst✝, snd✝¹), snd✝)

Tactic:
simp [Equiv.prodAssoc, and_assoc]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ ComplementedLattice β → ComplementedLattice α

Tactic:
intro; exact f.symm.complementedLattice

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
obtain h | h := le_total 1 a
  · simpa [mabs_of_one_le h] using (inv_le_one'.2 h).trans h
  · simp [mabs_of_le_one h]

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℕ
⊢ x.xgcd y = (x.gcdA y, x.gcdB y)

Tactic:
unfold gcdA gcdB

Goal state after:
x y : ℕ
⊢ x.xgcd y = ((x.xgcd y).1, (x.xgcd y).2)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a < a * c

Tactic:
apply lt_mul_of_one_lt_right'

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ b - a + a = max b a

Tactic:
tsub_add_eq_max

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ max b a = max b a
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ DenselyOrdered αˣ

Tactic:
refine ⟨fun x y h ↦ ?_⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x y : αˣ
h : x < y
⊢ ∃ a, x < a ∧ a < y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
⊢ DenselyOrdered α

Tactic:
refine ⟨fun x y h ↦ ?_⟩

Goal state after:
case refine_3
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
x y : α
h : x < y
⊢ ∃ a, x < a ∧ a < y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.zero.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ ↑a✝¹ ≤ ↑a✝¹ + ↑a✝

Tactic:
· rw [← coe_add, coe_le_coe]
      exact le_add_of_nonneg_right (h _)

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

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
m n : ℕ
hmn : m ≤ n
⊢ findGreatest P m ≤ findGreatest P n

Tactic:
induction hmn with
  | refl => simp
  | step hmk ih =>
    rw [findGreatest_succ]
    split_ifs
    · exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)
    · exact ih

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥)

Tactic:
by
  intro a b
  rcases (em (∃ i, e i = a)).symm with (ha | ⟨i, rfl⟩)
  · use b
    simp [Function.extend_apply' _ _ _ ha]
  rcases (em (∃ i, e i = b)).symm with (hb | ⟨j, rfl⟩)
  · use e i
    simp [Function.extend_apply' _ _ _ hb]
  rcases hf i j with ⟨k, hi, hj⟩
  use e k
  simp only [he.extend_apply, *, true_and]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
simp_rw [inverse_invertible, invOf_add_invOf]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Even n
h₀ : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0

Tactic:
by
  obtain ⟨k, rfl⟩ := hn; rw [pow_add, mul_self_pos, pow_ne_zero_iff (by simpa using h₀)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s

Tactic:
rw [strictAntiOn_insert_iff]
  have : ∀ b ∈ s, a < b → f b < f a := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
  tauto

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 < b ^ 2
hb : 0 ≤ b
⊢ |a| < b

Tactic:
by
  rwa [← abs_of_nonneg hb, ← sq_lt_sq]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ Relation.Fibration (fun x1 x2 ↦ x1 < x2) (fun x1 x2 ↦ x1 < x2) (toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2)

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

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ t ∩ s ∪ t \ s = t

Tactic:
inter_union_sdiff

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ t = t
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case pos.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}

Tactic:
exact subset_sdiff_singleton hc ha

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h'' : NeZero 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]
  apply Nat.cast_pos'.2
  simpa using! w

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 0 < -a ↔ a < 0

Tactic:
neg_pos

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a < 0 ↔ a < 0
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
x y : List α
n : ℕ
⊢ take n x = take n (x ++ y) ↔ y = [] ∨ n ≤ x.length

Tactic:
rw [Eq.comm]; apply take_eq_left_iff

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ (1 - 1 / a)⁻¹ ≤ 2

Tactic:
by
  -- Take inverses on both sides to obtain `2⁻¹ ≤ 1 - 1 / a`
  refine (inv_anti₀ (inv_pos.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))
  -- move `1 / a` to the left and `2⁻¹` to the right.
  rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]
  -- take inverses on both sides and use the assumption `2 ≤ a`.
  convert (one_div a).le.trans (inv_anti₀ zero_lt_two a2)
    -- show `1 - 1 / 2 = 1 / 2`.

  -- show `1 - 1 / 2 = 1 / 2`.
  rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]

Goal state after:
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: case inl
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length < n
⊢ a = b ∨ a ∈ l

Tactic:
rw [insertIdx_of_length_lt hn] at h

Goal state after:
case inl
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l
hn : l.length < n
⊢ a = b ∨ a ∈ l
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
l' : List α
h₁ : Forall₂ (flip r) l₃ l'
h₂ : l' ~ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
exact ⟨l', h₂.symm, h₁.flip⟩

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

Goal state before:
pp: α : Type u
x a : α
l : List α
h : x ∈ (a :: l).head?
⊢ a :: l = x :: (a :: l).tail

Tactic:
simp only [head?, Option.mem_def, Option.some_inj] at h

Goal state after:
α : Type u
x a : α
l : List α
h : a = x
⊢ a :: l = x :: (a :: l).tail
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ L.eval * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval

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

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.num * q₂.num =
    q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) *
      ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
refine (Int.ediv_mul_cancel ?_).symm

Goal state after:
q₁ q₂ : ℚ
⊢ ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) ∣ q₁.num * q₂.num
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mpr
q : ℚ
⊢ IsSquare q.num ∧ IsSquare q.den → IsSquare q

Tactic:
· rintro ⟨⟨nr, hnr⟩, ⟨dr, hdr⟩⟩
    refine ⟨nr / dr, ?_⟩
    rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]

Goal state after: