mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c

Tactic:
by_cases P <;> simp [*, exists_prop_of_true, exists_prop_of_false]

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)

Tactic:
simp [-not_and, not_and_or]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
f' : β → γ
gc : γ → γ → γ
hf' : Semiconj₂ f' gb gc
hf : Semiconj₂ f ga gb
x y : α
⊢ (f' ∘ f) (ga x y) = gc ((f' ∘ f) x) ((f' ∘ f) y)

Tactic:
by simp only [hf'.eq, hf.eq, comp_apply]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Sort u_3
f : α → γ
g₁ g₂ : β → γ
hg : Sum.elim f g₁ = Sum.elim f g₂
b : β
⊢ g₁ b = g₂ b

Tactic:
by simpa using congr_fun hg (Sum.inr b)

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

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl

Tactic:
by
  cases n <;> simp [leRec, Or.by_cases, dif_neg]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False

Tactic:
cases not_or_intro xy yx (total_of _ _ _)

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False

Tactic:
cases not_or_intro xy yx (total_of _ _ _)

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ↔ x' ≤ y'

Tactic:
rw [← not_lt, ← not_lt]
  apply not_congr
  apply lt_iff_lt_of_cmp_eq_cmp
  rwa [cmp_eq_cmp_symm]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g a).fst < (Prod.map f g b).fst ∧ (Prod.map f g a).snd ≤ (Prod.map f g b).snd ∨
      (Prod.map f g a).fst ≤ (Prod.map f g b).fst ∧ (Prod.map f g a).snd < (Prod.map f g b).snd

Tactic:
exact Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
not_monotone_not_antitone_iff_exists_le_le,

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
    ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ IsCompl ↑a ↑b ↔ IsCompl a b

Tactic:
by
  simp_rw [isCompl_iff, disjoint_coe, codisjoint_coe]

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

Goal state before:
pp: n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
hg_anti : Antitone g
p : ℕ
hp : p ≤ f 1
hp' : ∀ (m : ℕ), p ≤ m → g m = g p
⊢ p + 1 ≤ n

Tactic:
by omega

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬s.Subsingleton ↔ s.Nontrivial

Tactic:
by
  simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall, exists_prop]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
rw [← le, map_inf, map_sup, map_sup, map_sup, map_inf]
    exact le_sup_inf

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ b = a ⇨ b

Tactic:
rw [sup_himp_distrib, himp_self, inf_top_eq]

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.17
β : Type ?u.16
s : α ⊕' β
⊢ Sum.elim PSum.inl PSum.inr ((fun s ↦ PSum.casesOn s inl inr) s) = s

Tactic:
cases s

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
α : Type ?u.17
β : Type ?u.16
val✝ : α
⊢ Sum.elim PSum.inl PSum.inr ((fun s ↦ PSum.casesOn s inl inr) (PSum.inl val✝)) = PSum.inl val✝

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
α : Type ?u.17
β : Type ?u.16
val✝ : β
⊢ Sum.elim PSum.inl PSum.inr ((fun s ↦ PSum.casesOn s inl inr) (PSum.inr val✝)) = PSum.inr val✝
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.17
β : Type ?u.16
s : α ⊕ β
⊢ (fun s ↦ PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr s) = s

Tactic:
cases s

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
α : Type ?u.17
β : Type ?u.16
val✝ : α
⊢ (fun s ↦ PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inl val✝)) = inl val✝

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
α : Type ?u.17
β : Type ?u.16
val✝ : β
⊢ (fun s ↦ PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inr val✝)) = inr val✝
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.15
s : α ⊕ β
⊢ (fun s ↦
        match s with
        | ⟨false, a⟩ => inl a
        | ⟨true, b⟩ => inr b)
      ((fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) s) =
    s

Tactic:
cases s

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
α β : Type ?u.15
val✝ : α
⊢ (fun s ↦
        match s with
        | ⟨false, a⟩ => inl a
        | ⟨true, b⟩ => inr b)
      ((fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) (inl val✝)) =
    inl val✝

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
α β : Type ?u.15
val✝ : β
⊢ (fun s ↦
        match s with
        | ⟨false, a⟩ => inl a
        | ⟨true, b⟩ => inr b)
      ((fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) (inr val✝)) =
    inr val✝
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
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x : { a // ¬p a } → β
x✝ : { a // ¬p a }
a : α
h : ¬p a
⊢ (if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩) = x ⟨a, h⟩

Tactic:
dif_neg h

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
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x : { a // ¬p a } → β
x✝ : { a // ¬p a }
a : α
h : ¬p a
⊢ x ⟨a, h⟩ = x ⟨a, h⟩
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
⊢ GeneralizedBooleanAlgebra α

Tactic:
apply e.injective.generalizedBooleanAlgebra

Goal state after:
case le
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ e ⊥ = ⊥

case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α₁ : Type u_11
β₁ : Type u_12
e : α₁ ≃ β₁
f : α₁ → α₁ → α₁
x y : α₁
⊢ e (f x y) = (e.arrowCongr e.conj) f (e x) (e y)

Tactic:
simp [arrowCongr]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
        { rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq] }

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

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Set α
⊢ id '' s = s

Tactic:
image_id

Goal state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Set α
⊢ s = s
Module: Mathlib.Data.Set.Image

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

Tactic:
exists_const,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
hβ : Nonempty β
⊢ range (const α) = {f | ∀ (x y : α), f x = f y}

Tactic:
by
  refine (range_eq_iff _ _).mpr ⟨fun _ _ _ ↦ rfl, fun f hf ↦ ?_⟩
  rcases isEmpty_or_nonempty α with h | ⟨⟨a⟩⟩
  · exact hβ.elim fun b ↦ ⟨b, Subsingleton.elim _ _⟩
  · exact ⟨f a, funext fun x ↦ hf _ _⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ id '' s = s

Tactic:
image_id

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ s = s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∀ (s : Set ↑t), p (val '' s)) ↔ ∀ (s : Set α), s ⊆ t → p s

Tactic:
by
  rw [← forall_subset_range_iff, range_coe]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ univ.pi (update (fun j ↦ univ) i s) = eval i ⁻¹' s

Tactic:
rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
hf : f ∈ s.pi t
j : ι
hj : j ∈ s
y : α j
hy : y ∈ t j
⊢ update f j y j ∈ t j

Tactic:
simp [*, hf _ hj]

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

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
hji : j ≠ i
⊢ update f i y j ∈ t j

Tactic:
simp [*, hf _ hj]

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

Goal state before:
pp: ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ ∀ (i_1 : ι), y i_1 ∈ update (fun j ↦ {x j}) i s i_1

Tactic:
forall_update_iff (p := fun x s => y x ∈ s)

Goal state after:
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ y i ∈ s ∧ ∀ (x_1 : ι), x_1 ≠ i → y x_1 ∈ {x x_1}
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ Prod.fst '' graphOn f s = s

Tactic:
simp [graphOn, image_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ¬∃ a, a ∈ s ∧ f a = b
⊢ (if h : ∃ a, a ∈ s ∧ f a = b then Classical.choose h else Classical.choice inst✝) = Classical.choice inst✝

Tactic:
dif_neg h

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ¬∃ a, a ∈ s ∧ f a = b
⊢ Classical.choice inst✝ = Classical.choice inst✝
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ (m % n)

Tactic:
by
  calc
    a ^ m = a ^ (m % n + n * (m / n)) := by rw [Nat.mod_add_div]
    _ = a ^ (m % n) := by simp [pow_add, pow_mul, ha]

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

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

Tactic:
by simp [mul_left_comm c]

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

Goal state before:
pp: case e_inv
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ i₁ = i₂

Tactic:
simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

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

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Bijective ⇑f
⊢ Bijective ⇑(map f)

Tactic:
refine ⟨map_injective hf.injective, ?_⟩
  rintro ⟨u, v, uv, vu⟩
  rcases hf.surjective u, hf.surjective v with ⟨⟨u, rfl⟩, ⟨v, rfl⟩⟩
  exact ⟨⟨u, v, hf.injective <| by simpa, hf.injective <| by simpa⟩, rfl⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
by
    rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → β
a : m (m α)
⊢ joinM (Functor.map f <$> a) = f <$> joinM a

Tactic:
by
  simp only [joinM, id, ← bind_pure_comp, bind_assoc, pure_bind]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m (m (m α))
⊢ joinM (joinM <$> a) = joinM (joinM a)

Tactic:
by
  simp only [joinM, id, ← bind_pure_comp, bind_assoc, pure_bind]

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

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

Tactic:
rw [mul_assoc, mul_inv_cancel₀ h, mul_one]

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

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
⊢ (a • if p then b else 0) = if p then a • b else 0

Tactic:
by split_ifs <;> simp

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0

Tactic:
rw [zpow_natCast, zero_pow]; simpa [Int.natCast_eq_zero] using h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 1 ↔ n = 1

Tactic:
by rw [← cast_one, cast_inj]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
inst✝ : Nontrivial β
h : 1 = 0
⊢ f 1 = 0

Tactic:
rw [h, map_zero]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a / b = c / d ↔ a / c = b / d

Tactic:
by
  conv_lhs => rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]
  conv_rhs => rw [← mul_left_inj' hc, div_mul_cancel₀ _ hc]
  rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
a b : α
u : αˣ
⊢ a + b /ₚ u = (a * ↑u + b) /ₚ u

Tactic:
by
  simp only [divp, add_mul, Units.mul_inv_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
a b : α
u : αˣ
⊢ a /ₚ u + b = (a + b * ↑u) /ₚ u

Tactic:
by
  simp only [divp, add_mul, Units.mul_inv_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u

Tactic:
by
  rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
⊢ ↑n = 1 ↔ n = 1

Tactic:
by rw [← cast_one, cast_inj]

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

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b

Tactic:
exact le_rfl

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

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a : α
inst✝ : MulLeftReflectLE α
c : α
h : a ≤ a * c
⊢ ∃ c_1, 1 ≤ c_1 ∧ a * c_1 = a * c

Tactic:
exact ⟨c, one_le_of_le_mul_right h, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 3

Tactic:
rw [← two_add_one_eq_three]
  exact add_nonneg zero_le_two zero_le_one

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

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

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

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

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + a ≤ 1 + c - (b + b * c)

Tactic:
le_sub_iff_add_le,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + a + (b + b * c) ≤ 1 + c
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a ≤ 1 + b - (c + b * c)

Tactic:
le_sub_iff_add_le,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a + (c + b * c) ≤ 1 + b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case pos
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : a * b < a * c
hbc : b ≤ c
ha : 0 < a
⊢ 0 < a

pp: case neg
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : a * b < a * c
hbc : b ≤ c
ha : a ≤ 0
⊢ 0 < a

Tactic:
· exact ha

Goal state after:
case neg
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : a * b < a * c
hbc : b ≤ c
ha : a ≤ 0
⊢ 0 < a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case pos
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
ha : 0 < a
⊢ 0 < a

pp: case neg
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
ha : a ≤ 0
⊢ 0 < a

Tactic:
· exact ha

Goal state after:
case neg
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
ha : a ≤ 0
⊢ 0 < a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a / b ≤ a / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]
  gcongr
  exacts [ha, hc]

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

Goal state before:
pp: α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : r ≍ s
h₂' : s ≍ t
x : α
⊢ ((RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x

Tactic:
subst h₁; rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]
  exact f.monotone ha.le_bot

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

Goal state before:
pp: case inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
simp [ha, hb, mabs_of_one_le, one_le_mul ha hb]

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ max a 1 * max a⁻¹ 1 = |a|ₘ

Tactic:
by
  symm
  rcases le_total 1 a with (ha | ha) <;> simp [ha]

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

Goal state before:
pp: z : ℤ
hz : z ≠ 0
⊢ |z.sign| = 1

Tactic:
rw [abs_eq_natAbs, natAbs_sign_of_ne_zero hz, Int.ofNat_one]

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

Goal state before:
pp: case ofNat
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * Int.ofNat k + 1) = -a ^ (2 * Int.ofNat k + 1)

Tactic:
rw [Int.ofNat_eq_natCast]

Goal state after:
case ofNat
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * ↑k + 1) = -a ^ (2 * ↑k + 1)