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

Goal state before:
pp: case inl
n : Nat
h : n % 2 = 0
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
simpa [h] using Nat.div_add_mod n 2

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

Goal state before:
pp: case inr
n : Nat
h : n % 2 = 1
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
simpa [h] using Nat.div_add_mod n 2

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

Goal state before:
pp: motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)),
    e ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n

Tactic:
rw [testBit_bit_zero, bit_shiftRight_one]

Goal state after:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit b n) = motive (bit b n)), e ▸ h b n = h b n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
⊢ ∀ (e : motive (Nat.bit ((Nat.bit b n).testBit 0) (Nat.bit b n >>> 1)) = motive (Nat.bit b n)),
    e ▸ bit ((Nat.bit b n).testBit 0) (Nat.bit b n >>> 1) (binaryRec zero bit (Nat.bit b n >>> 1)) =
      bit b n (binaryRec zero bit n)

Tactic:
rw [testBit_bit_zero, bit_shiftRight_one]

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
⊢ ∀ (e : motive (Nat.bit b n) = motive (Nat.bit b n)),
    e ▸ bit b n (binaryRec zero bit n) = bit b n (binaryRec zero bit n)
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n ≠ 0
⊢ n = 0 → b = true

Tactic:
by simp [h]

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

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
a : M
⊢ SemiconjBy a 1 1

Tactic:
SemiconjBy,

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
a : M
⊢ a * 1 = 1 * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: M : Type u_2
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ SemiconjBy a y y

Tactic:
SemiconjBy,

Goal state after:
M : Type u_2
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ a * y = y * a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 3 = a * a * a

Tactic:
by rw [pow_succ, pow_two]

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

Goal state before:
pp: case refine_1
α : 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₀
⊢ ((fun g ↦ g ∘ f) fun x ↦ c) = (fun g ↦ g ∘ f) fun x ↦ if x = b₀ then c' else c

Tactic:
ext a

Goal state after:
case refine_1
α : 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₀
a : α
⊢ (fun g ↦ g ∘ f) (fun x ↦ c) a = (fun g ↦ g ∘ f) (fun x ↦ if x = b₀ then c' else c) a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
inst✝ : Nonempty α
g : β → γ
⊢ (Surjective fun x ↦ g ∘ x) ↔ Surjective g

Tactic:
by
  refine ⟨fun h c ↦ Nonempty.elim ‹_› fun a ↦ ?_, (·.comp_left)⟩
  have ⟨f, hf⟩ := h fun _ ↦ c
  exact ⟨f a, congr_fun hf _⟩

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

Goal state before:
pp: γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
⊢ extend (f₂₃ ∘ f₁₂) g e' = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e'

Tactic:
ext a

Goal state after:
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
⊢ Surjective fun f ↦ restrict p f

Tactic:
classical
  exact fun f ↦ ⟨fun x ↦ if h : p x then f ⟨x, h⟩ else Nonempty.some (ne x), by grind⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
· obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h
    · exact .single .refl
    · exact h.mono (fun _ _ ↦ .single) x y

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:
funext x
    simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∀ (b : β), p (e.symm b)) ↔ ∀ (b : β), q b

Tactic:
by simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∀ (b : β), p (e.symm b)) ↔ ∀ (b : β), q b

Tactic:
by simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∃ b, p (e.symm b)) ↔ ∃ b, q b

Tactic:
by simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∃ b, p (e.symm b)) ↔ ∃ b, q b

Tactic:
by simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∃! b, p (e.symm b)) ↔ ∃! b, q b

Tactic:
by simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∃! b, p (e.symm b)) ↔ ∃! b, q b

Tactic:
by simp [h]

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

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy x (r • a) (r • b)

Tactic:
SemiconjBy,

Goal state after:
M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ x * r • a = r • b * x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy (r • x) a b

Tactic:
SemiconjBy,

Goal state after:
M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • x * a = b * r • x
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ 0 ≠ a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
ne_comm,

Goal state after:
a b : ℤ
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ a * b ≠ 0 ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: a : ℕ
ha : 2 ≤ a
⊢ Injective fun x ↦ a ^ x

Tactic:
by
  simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_right ha]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a < b
hab : lt.Compares a b
⊢ o.Compares a b

Tactic:
rwa [ho.inj (h hab)]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a = b
hab : eq.Compares a b
⊢ o.Compares a b

Tactic:
rwa [ho.inj (h hab)]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : b < a
hab : gt.Compares a b
⊢ o.Compares a b

Tactic:
rwa [ho.inj (h hab)]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
h : r = ⊤
⊢ ∀ (a : α), r a a

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
h : r = ⊥
⊢ ∀ (a : α), ¬r a a

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
s✝ t u : Set α
p : α → Prop
s : Set { a // p a }
⊢ (fun s ↦ {a | ↑a ∈ ↑s}) ((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) s) = s

Tactic:
ext a

Goal state after:
α : Type u_1
s✝ t u : Set α
p : α → Prop
s : Set { a // p a }
a : { a // p a }
⊢ a ∈ (fun s ↦ {a | ↑a ∈ ↑s}) ((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) s) ↔ a ∈ s
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
⊢ SemilatticeInf α

Tactic:
let min := e.min
  let partialOrder := e.partialOrder
  apply e.injective.semilatticeInf <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⇨ bᶜ = b ⇨ aᶜ

Tactic:
by simp_rw [← himp_bot, himp_left_comm]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x = ⊥

Tactic:
inf_sdiff_self_right

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ⊥ = ⊥
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
⊢ Disjoint {a} s

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
⊢ (fun e ↦
        ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
            invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
          ⋯⟩)
      ((fun e ↦
          { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯, right_inv := ⋯ })
        e) =
    e

Tactic:
ext a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
a : Option α
⊢ ↑((fun e ↦
            ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
                invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
              ⋯⟩)
          ((fun e ↦
              { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                right_inv := ⋯ })
            e))
      a =
    ↑e a
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
⊢ (fun e ↦ { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯, right_inv := ⋯ })
      ((fun e ↦
          ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
              invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
            ⋯⟩)
        e) =
    e

Tactic:
ext a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : α
⊢ ↑(((fun e ↦
            { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
              right_inv := ⋯ })
          ((fun e ↦
              ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
                  invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
                ⋯⟩)
            e))
        a) =
    ↑(e a)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ⊓ y \ x ≤ z ⊓ y \ x

Tactic:
inf_sdiff_self_right

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ ⊥ ≤ z ⊓ y \ x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [sup_inf_sdiff, sup_inf_sdiff]

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
s : PUnit ⊕ PUnit
⊢ (fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit)) (Sum.elim (fun x ↦ false) (fun x ↦ true) s) = s

Tactic:
rcases s with (⟨⟨⟩⟩ | ⟨⟨⟩⟩)

Goal state after:
case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ (fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit))
      (Sum.elim (fun x ↦ false) (fun x ↦ true) (inl PUnit.unit)) =
    inl PUnit.unit

case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ (fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit))
      (Sum.elim (fun x ↦ false) (fun x ↦ true) (inr PUnit.unit)) =
    inr PUnit.unit
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < z

Tactic:
by
  rw [← sup_sdiff_cancel_right hxz]
  refine (sup_le_sup_left h.le _).lt_of_not_ge fun h' => h.not_ge ?_
  rw [← sdiff_idem]
  exact (sdiff_le_sdiff_of_sup_le_sup_left h').trans sdiff_le

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  rw [h.eq_hnot, hnot_symmDiff_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
a : α
⊢ {a} ×ˢ t = Prod.mk a '' t

Tactic:
by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ s ×ˢ {b} = (fun a ↦ (a, b)) '' s

Tactic:
by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Injective (preimage f) ↔ Surjective f

Tactic:
rw [← Injective.of_comp_iff Set.mem_injective, ← Injective.of_comp_iff' _ Set.ofPred_bijective]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ Injective ((Membership.mem ∘ preimage f) ∘ ofPred) ↔ Surjective f
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
⊢ x ∈ t

Tactic:
rcases hs hx with ⟨y, rfl⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
y : β
hx : f y ∈ s
⊢ f y ∈ t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ {y}
⊢ ∃ a, f a = y

Tactic:
rw [← hs] at this

Goal state after:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ f '' s
⊢ ∃ a, f a = y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ s = (fun x ↦ (x, f x)) '' Prod.fst '' s

Tactic:
image_image,

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ s = (fun x ↦ (x.1, f x.1)) '' s
Module: Mathlib.Data.Int.Init

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

Tactic:
| ofNat i =>

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : CommMagma M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
⊢ f (x * y) = f (y * x)

Tactic:
by rw [mul, mul, mul_comm]

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

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

Tactic:
by simp [h]

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

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

Tactic:
by simp [h]

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

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

Tactic:
by simp [h]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a / b = c

Tactic:
by simp [h]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = c / b
⊢ a * b = c

Tactic:
by simp [h]

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

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

Tactic:
Commute,

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
⊢ SemiconjBy ↑a ↑a⁻¹ ↑a⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
SemiconjBy,

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
⊢ ↑a * ↑a⁻¹ = ↑a⁻¹ * ↑a
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x = y /ₚ u ↔ x * ↑u = y

Tactic:
by
  rw [eq_comm, divp_eq_iff_mul_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
y : M
⊢ (fun x ↦ a * x) (↑h.unit⁻¹ * y) = y

Tactic:
by simp [← mul_assoc]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a * (1 / a) = 1

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ 1 / a * a = 1

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b a : α
h : IsUnit b
⊢ a * b * (1 / b) = a

Tactic:
by simp [h]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ = a⁻¹ * a⁻¹⁻¹

Tactic:
by simp [h]

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

Goal state before:
pp: G₀ : Type u
inst✝ : GroupWithZero G₀
b : G₀
h : b ≠ 0
a : G₀
⊢ a * (b * b⁻¹) = a

Tactic:
by simp [h]

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

Goal state before:
pp: G₀ : Type u
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
b : G₀
⊢ a * a⁻¹ * b = b

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p ((f ^ (n + 1))⁻¹ x) ↔ p x

Tactic:
exact pow_aux (inv_aux.1 hf)

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 = 1

Tactic:
by
  rw [cast_succ, Nat.cast_zero, zero_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ n.binCast = ↑n

Tactic:
induction n using Nat.strongRecOn with | ind k hk => ?_

Goal state after:
case ind
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k → m.binCast = ↑m
⊢ k.binCast = ↑k
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
by simp [h]

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

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

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a + 1 = a
⊢ a + 1 = a + 0

Tactic:
by simp [h]

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 = a * ↑u

Tactic:
Commute,

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ SemiconjBy (↑u) a a ↔ ↑u * a = a * ↑u
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
b a : G₀
h : b ≠ 0
⊢ a / b * b = a

Tactic:
by simp [h]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
have h1 : m - n + n = m := Nat.sub_add_cancel h
  have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]
  simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
by
  rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]

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

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
a x y : α
h : SemiconjBy a x y
m n : ℤ
⊢ SemiconjBy (↑m * a) (↑n * x) (↑n * y)

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Odd n
⊢ f^[n] = f

Tactic:
obtain ⟨m, rfl⟩ := hn
  rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]

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 < 4

Tactic:
by
  rw [← three_add_one_eq_four]
  exact lt_add_of_lt_of_nonneg zero_lt_three 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 : G₀
hb : 0 < b
⊢ 1 < a / b ↔ b < a

Tactic:
by rw [lt_div_iff₀ hb, one_mul]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
⊢ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
neg_nonpos

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
⊢ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
rw [← neg_nonneg, ← mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]
  simp only [neg_pos, neg_nonneg]

Goal state after: