mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Translate.GuessName

Goal state before:
pp: x : String
s : List String
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (s.length + [].length, s.length)
    ([].length + (x :: s).length, [].length)

pp: pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h✝ : (pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂)
    ((List.drop 1 (s' ++ [pre]) ++ l).length + [].length, (List.drop 1 (s' ++ [pre]) ++ l).length)
    ((pre :: l).length + s'.length, (pre :: l).length)

pp: pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h✝ : ¬(pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (l.length + [].length, l.length)
    ((pre :: l).length + s'.length, (pre :: l).length)

pp: pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h✝ : ¬(pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (l.length + (s' ++ [pre]).length, l.length)
    ((pre :: l).length + s'.length, (pre :: l).length)

Tactic:
decreasing_by all_goals grind

Goal state after:
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
⊢ (if n0 : Nat.bit b n = 0 then ⋯ ▸ zero
    else
      have x := bit (1 &&& Nat.bit b n != 0) (Nat.bit b n >>> 1) (binaryRec zero bit (Nat.bit b n >>> 1));
      ⋯ ▸ x) =
    bit b n (binaryRec zero bit n)

Tactic:
dif_neg h'

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
⊢ (have x := bit (1 &&& Nat.bit b n != 0) (Nat.bit b n >>> 1) (binaryRec zero bit (Nat.bit b n >>> 1));
    ⋯ ▸ x) =
    bit b n (binaryRec zero bit n)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a * a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
ih n.succ_ne_zero

Goal state after:
case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec m a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case bit
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit b k' ≠ 0
⊢ Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y) (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x))
      (Nat.bit b k') m n =
    m * npowRec' (Nat.bit b k') n

Tactic:
| bit b k' k'0 ih =>

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ (a ^ m) ^ n = (a ^ n) ^ m

Tactic:
← pow_mul,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * n) = (a ^ n) ^ m
Module: Mathlib.Logic.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Subsingleton ι
P : ι → ι → Prop
⊢ (∀ (i j : ι), P i j) ↔ ∀ (i : ι), P i i

Tactic:
refine forall_congr' fun i ↦ ?_

Goal state after:
ι : Sort u_3
inst✝ : Subsingleton ι
P : ι → ι → Prop
i : ι
⊢ (∀ (j : ι), P i j) ↔ P i i
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

Tactic:
by_cases h : P <;> simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
⊢ dite P f g a = if h : P then f h a else g h a

Tactic:
by_cases h : P <;> simp [h]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α ∧ Nonempty α

Tactic:
constructor <;> exact inferInstance

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

Goal state before:
pp: case intro
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
⊢ False

Tactic:
have hg : Injective g := by
    intro s t h
    suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
    · congr

Goal state after:
case intro
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
hg : Injective g
⊢ False
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : (if h : ∃ a, f a = b then some (Classical.choose h) else none) = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b

Tactic:
dif_neg h'

Goal state after:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Relation.Map r id id = r

Tactic:
by ext; simp [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : 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 : α
h : ReflTransGen r x y
⊢ ReflTransGen r y x

Tactic:
induction h with
    | refl => rfl
    | tail _ b c => apply c.head <| symm b

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

Goal state before:
pp: α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
⊢ (Equiv.cast ⋯) x = ((Equiv.cast h).trans (Equiv.cast h2)) x

Tactic:
by subst h h2; rfl

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Monoid (f i)
n✝ : ℕ
x✝¹ : (i : I) → f i
x✝ : I
⊢ (x✝¹ ^ (n✝ + 1)) x✝ = (x✝¹ ^ n✝ * x✝¹) x✝

Tactic:
exact Monoid.npow_succ _ _

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: α α' : Sort u
β β' : Sort v
h : α = α'
h' : ∀ (a : α'), β = β'
⊢ (α → β) = (α' → β')

Tactic:
cases h
  change (∀ (x : α), (fun _ => β) x) = _
  rw [funext h']

Goal state after:
Module: Mathlib.Tactic.Push

Goal state before:
pp: p q : Prop
⊢ ¬p ∧ q ∨ ¬¬p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q

Tactic:
by rw [not_not, or_comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ f ⊤

Tactic:
rw [map_top]
      exact le_top _

Goal state after:
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
⊢ min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Tactic:
← le_bot_iff,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
⊢ min a b ≤ ⊥ ↔ a ≤ ⊥ ∨ b ≤ ⊥
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
← le_bot_iff,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y ≤ ⊥ ↔ x ≤ z
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x

Tactic:
rw [and_assoc]

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

Goal state before:
pp: α : Type u
s t : Set α
a b : α
p : α → Prop
inst✝ : Decidable (p a)
⊢ Decidable (a ∈ {a | p a})

Tactic:
by
  assumption

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ (fun x1 x2 ↦ x1 ⊓ x2) = minDefault

Tactic:
by
  ext x y
  unfold minDefault
  split_ifs with h'
  exacts [inf_of_le_left h', inf_of_le_right <| (total_of (· ≤ ·) x y).resolve_left h']

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

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

Tactic:
← sdiff_inf_self_right,

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

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

Tactic:
exact disjoint_sdiff_self_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
x y : α
heq : extend f g j (f x) = extend f g j (f y)
⊢ f x = f y

Tactic:
hf.extend_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
x y : α
heq : g x = extend f g j (f y)
⊢ f x = f y
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
⊢ range f ⊆ range g ↔ ∃ h, f = g ∘ h

Tactic:
by
  simp only [range_subset_iff, mem_range, Classical.skolem, funext_iff, (· ∘ ·), eq_comm]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
⊢ range f = ∅ ↔ IsEmpty ι

Tactic:
by
  rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s = range fun x ↦ f ↑x

Tactic:
by
  ext
  constructor
  · rintro ⟨x, h1, h2⟩
    exact ⟨⟨x, h1⟩, h2⟩
  · rintro ⟨⟨x, h1⟩, h2⟩
    exact ⟨x, h1, h2⟩

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

Goal state before:
pp: case mp.inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s ∅ → ∃ s', s' ⊆ s ∧ BijOn f s' ∅

pp: case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
· exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩

Goal state after:
case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
by_cases h : P <;> simp [h]

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

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

Tactic:
by_cases h : P <;> simp [h]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ (n - m) * a ^ m = a ^ n

Tactic:
by
  rw [← pow_add, Nat.sub_add_cancel h]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
k n : ℕ
⊢ (fun x ↦ x ^ k)^[n + 1] = fun x ↦ x ^ k ^ (n + 1)

Tactic:
ext; simp [pow_iterate, Nat.pow_succ', pow_mul]

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

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

Tactic:
← pow_mul,

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * Int.negSucc n) = ((a ^ m) ^ (n + 1))⁻¹

Tactic:
← pow_mul,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * Int.negSucc n) = (a ^ (m * (n + 1)))⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (Int.negSucc m * ↑n) = (a⁻¹ ^ (m + 1)) ^ n

Tactic:
← pow_mul,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (Int.negSucc m * ↑n) = a⁻¹ ^ ((m + 1) * n)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m.succ * ↑n.succ) = (a ^ (m + 1)) ^ (n + 1)

Tactic:
← pow_mul,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m.succ * ↑n.succ) = a ^ ((m + 1) * (n + 1))
Module: Mathlib.Control.Basic

Goal state before:
pp: case map_const
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

Tactic:
casesm Sum _ _

Goal state after:
case map_const
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case id_map
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e ⊕ α✝
⊢ id <$> x✝ = x✝

Tactic:
casesm Sum _ _

Goal state after:
case id_map.inl
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e
⊢ id <$> inl x✝ = inl x✝

case id_map.inr
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : α✝
⊢ id <$> inr x✝ = inr x✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case comp_map
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e ⊕ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝

Tactic:
casesm Sum _ _

Goal state after:
case comp_map.inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e
⊢ (h✝ ∘ g✝) <$> inl x✝ = h✝ <$> g✝ <$> inl x✝

case comp_map.inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : α✝
⊢ (h✝ ∘ g✝) <$> inr x✝ = h✝ <$> g✝ <$> inr x✝
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
y✝ : e ⊕ β✝
⊢ x✝ <* y✝ = Function.const β✝ <$> x✝ <*> y✝

Tactic:
casesm Sum _ _

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : e
⊢ inl x✝ <* y✝ = Function.const β✝ <$> inl x✝ <*> y✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : α✝
⊢ inr x✝ <* y✝ = Function.const β✝ <$> inr x✝ <*> y✝
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
y✝ : e ⊕ β✝
⊢ x✝ *> y✝ = Function.const α✝ id <$> x✝ <*> y✝

Tactic:
casesm Sum _ _

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : e
⊢ inl x✝ *> y✝ = Function.const α✝ id <$> inl x✝ <*> y✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : α✝
⊢ inr x✝ *> y✝ = Function.const α✝ id <$> inr x✝ <*> y✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : e
⊢ inl x✝ *> y✝ = Function.const α✝ id <$> inl x✝ <*> y✝

Tactic:
casesm Sum _ _

Goal state after:
case inl.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ y✝ : e
⊢ inl x✝ *> inl y✝ = Function.const α✝ id <$> inl x✝ <*> inl y✝

case inl.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e
y✝ : β✝
⊢ inl x✝ *> inr y✝ = Function.const α✝ id <$> inl x✝ <*> inr y✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : α✝
⊢ inr x✝ *> y✝ = Function.const α✝ id <$> inr x✝ <*> y✝

Tactic:
casesm Sum _ _

Goal state after:
case inr.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : α✝
y✝ : e
⊢ inr x✝ *> inl y✝ = Function.const α✝ id <$> inr x✝ <*> inl y✝

case inr.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : α✝
y✝ : β✝
⊢ inr x✝ *> inr y✝ = Function.const α✝ id <$> inr x✝ <*> inr y✝
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : e ⊕ α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝

Tactic:
casesm Sum _ _

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : e
⊢ (do
      let a ← inl x✝
      pure (f✝ a)) =
    f✝ <$> inl x✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : α✝
⊢ (do
      let a ← inr x✝
      pure (f✝ a)) =
    f✝ <$> inr x✝
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : e ⊕ (α✝ → β✝)
x✝ : e ⊕ α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    f✝ <*> x✝

Tactic:
casesm Sum _ _

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
f✝ : e
⊢ (do
      let x ← inl f✝
      x <$> x✝) =
    inl f✝ <*> x✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
f✝ : α✝ → β✝
⊢ (do
      let x ← inr f✝
      x <$> x✝) =
    inr f✝ <*> x✝
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
x✝ : e ⊕ α✝
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝

Tactic:
casesm Sum _ _

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
x✝ : e
⊢ inl x✝ >>= f✝ >>= g✝ = inl x✝ >>= fun x ↦ f✝ x >>= g✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
x✝ : α✝
⊢ inr x✝ >>= f✝ >>= g✝ = inr x✝ >>= fun x ↦ f✝ x >>= g✝
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ (x ^ n.succ) ^ N = 0

Tactic:
← pow_mul,

Goal state after:
n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ x ^ (n.succ * N) = 0
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
x : G₀'
hx : x ≠ 0
⊢ f (x * x⁻¹) = f 1

Tactic:
by
      rw [one, mul, inv, mul_inv_cancel₀ ((hf.ne_iff' zero).2 hx)]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ 0

Tactic:
by rw [← ZeroHomClass.map_zero f]; exact hf.ne NeZero.out

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

Goal state before:
pp: m n : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
⊢ ∀ (hn : m ≤ n), Int.strongRec lt ge n = ge n hn fun k x ↦ Int.strongRec lt ge k

Tactic:
refine m.strongRec (fun n hnm hmn ↦ (Int.not_lt.mpr hmn hnm).elim) (fun n _ ih hn ↦ ?_) n
  rw [Int.strongRec, dif_neg (Int.not_lt.mpr hn)]
  congr; revert ih
  refine n.inductionOn' m (fun _ ↦ ?_) (fun k hmk ih' ih ↦ ?_) (fun k hkm ih' _ ↦ ?_) <;> ext l hl
  · rw [inductionOn'_self, strongRec_of_lt hl]
  · rw [inductionOn'_add_one hmk]; split_ifs with hlm
    · rw [strongRec_of_lt hlm]
    · rw [ih' fun l hl ↦ ih l (Int.lt_trans hl k.lt_succ), ih _ hl]
  · rw [inductionOn'_sub_one hkm, ih']
    exact fun l hlk hml ↦ (Int.not_lt.mpr hkm <| Int.lt_of_le_of_lt hml hlk).elim

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ (a - 1) * b = a * b - b

Tactic:
by rw [sub_mul, one_mul]

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ (1 - a) * b = b - a * b

Tactic:
by rw [sub_mul, one_mul]

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

Goal state before:
pp: n : ℕ
⊢ n.sqrt ^ 2 ≤ n

Tactic:
by simpa [Nat.pow_two] using sqrt_le n

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ -1 * -1 = 1

Tactic:
rw [neg_mul_neg, one_mul]

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

Goal state before:
pp: case neg.inr
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]

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
⊢ x * (x⁻¹ʳ * y) = y

Tactic:
by
  rw [← mul_assoc, mul_inverse_cancel x h, one_mul]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1

Tactic:
exact mul_self_eq_one_iff

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

Goal state before:
pp: m n : ℕ
⊢ Even (m / n) ↔ m % (2 * n) / n = 0

Tactic:
even_iff_two_dvd,

Goal state after:
m n : ℕ
⊢ 2 ∣ m / n ↔ m % (2 * n) / n = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

Goal state before:
pp: α : Type u
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : Monoid α
inst✝¹ : ExistsMulOfLE α
inst✝ : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε

Tactic:
exact h _ (one_lt_of_lt_mul_right hxb)

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

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

Tactic:
contrapose h'

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬c * a = b * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : a * c = a * b
⊢ c = b

Tactic:
contrapose h'

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬a * c = a * b
Module: Mathlib.Algebra.Order.Group.Defs

Goal state before:
pp: case inl
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ a, 1 < a

pp: case inr
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ a, 1 < a

Tactic:
· exact ⟨y⁻¹, one_lt_inv'.mpr h⟩

Goal state after:
case inr
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ a, 1 < a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ a + (2 + b) ≤ a + (a + a * b)

Tactic:
by
      gcongr; exact le_mul_of_one_le_left b0 <| one_le_two.trans a2

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ c⁻¹ * b
hc : 0 < c
⊢ c * a ≤ b

Tactic:
rwa [le_inv_mul_iff₀ hc] at h

Goal state after: