mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c

pp: case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c

pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c

Tactic:
· exact _root_.trans h₃ h₂

Goal state after:
case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c

case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c
Module: Mathlib.Algebra.Group.Commute.Defs

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

Tactic:
by
  rw [h.eq, mul_inv_cancel_right]

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
⊢ go (k + 1) m n = m * npowRec' (k + 1) n

Tactic:
unfold go
  generalize hk : k + 1 = k'
  replace hk : k' ≠ 0 := by lia
  induction k' using Nat.binaryRecFromOne generalizing n m with
  | zero => simp at hk
  | one => simp [npowRec']
  | bit b k' k'0 ih =>
    rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]
    cases b <;> simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]
    rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a⁻¹ * (a * b) = b

Tactic:
rw [← mul_assoc, inv_mul_cancel, one_mul]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b c : α
⊢ (P ∧ a = c ∨ ∃ h, b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c

Tactic:
exists_prop

Goal state after:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a b c : α
⊢ P ∧ a = c ∨ ¬P ∧ b = c ↔ P ∧ a = c ∨ ¬P ∧ b = c
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ (∃ h, a ≠ b) ↔ ¬P ∧ a ≠ b

Tactic:
exists_prop

Goal state after:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ ¬P ∧ a ≠ b ↔ ¬P ∧ a ≠ b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ (∃ h, a ≠ b) ↔ P ∧ a ≠ b

Tactic:
exists_prop

Goal state after:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ P ∧ a ≠ b ↔ P ∧ a ≠ b
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
by_cases p : P

Goal state after:
case pos
P Q R : Prop
inst✝ : Decidable P
p : P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

case neg
P Q R : Prop
inst✝ : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
by_cases p : P

Goal state after:
case pos
P Q R : Prop
inst✝ : Decidable P
p : P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

case neg
P Q R : Prop
inst✝ : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
Bool.eq_iff_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝ : Symm r
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Involutive f ∧ r = fun x1 x2 ↦ f x1 = x2

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨f, _, hf⟩ ↦ forall_existsUnique_iff'.2 ⟨f, hf⟩⟩

Goal state after:
α : Sort u_1
r : α → α → Prop
inst✝ : Symm r
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, Involutive f ∧ r = fun x1 x2 ↦ f x1 = x2
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✝ : IsTrans α r
a b c : α
h₁ : ReflGen r a b
h₂ : ReflGen r b c
⊢ ReflGen r a c

Tactic:
obtain (rfl | h₂) := h₂
    · exact h₁
    obtain (rfl | h₁) := h₁
    · exact single h₂
    exact single (trans_of r h₁ h₂)

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

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.trans g = Equiv.refl α ↔ f = g.symm

Tactic:
← Equiv.coe_inj,

Goal state after:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑(f.trans g) = ⇑(Equiv.refl α) ↔ f = g.symm
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g • b
⊢ g⁻¹ • a = b

Tactic:
by rw [h, inv_smul_smul]

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

Goal state before:
pp: α : Sort u_4
⊢ IsEmpty (PLift α) ↔ IsEmpty α

Tactic:
simp only [← not_nonempty_iff, nonempty_plift]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
⊢ x < y ↔ x ≤ y ∧ ∃ i, x i < y i

Tactic:
simp +contextual [lt_iff_le_not_ge, Pi.le_def]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
⊢ x = y ∨ y = z ∨ x = z

Tactic:
by_contra hne

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : ¬(x = y ∨ y = z ∨ x = z)
⊢ False
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: n m : Nat
h : n ≤ m
⊢ ofNat n ≤ ofNat m

Tactic:
simp only [ofNat, ne_eq, _root_.decide_not]

Goal state after:
n m : Nat
h : n ≤ m
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
⊢ Surjective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
intro x
    refine ⟨x, ?_⟩
    rw [leRecOn_self]

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : ↑(range f)
⊢ rangeFactorization f a = b ↔ f a = ↑b

Tactic:
rw [Set.rangeFactorization, ← b.coe_eta b.2, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
suffices h : ∀ a, ∀ a' ≤ a, ∀ b, Acc (· < ·) (a', b) from ⟨fun x => h x.1 x.1 le_rfl x.2⟩

Goal state after:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
⊢ ∀ (a a' : α), a' ≤ a → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
h : a ≤ c ⊔ b
hd : Disjoint a c
⊢ a ≤ b ⊔ c

Tactic:
rwa [sup_comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ (¬∃ a, a ∈ s) ↔ s = ∅

Tactic:
not_exists,

Goal state after:
α : Type u
s : Set α
⊢ (∀ (x : α), ¬x ∈ s) ↔ s = ∅
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
⊢ a ⊔ (a ⊔ b) = a ⊔ b

Tactic:
by rw [← sup_assoc, sup_idem]

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

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x

Tactic:
by
  simp_rw [Set.ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false, not_and]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b = b ⊔ a

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b ≤ b ⊔ a

case a
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ b ⊔ a ≤ a ⊔ b
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
s : Set α
⊢ (∃ x h x_1 x_2, ¬x = x_1) ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y

Tactic:
exists_prop

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

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

Tactic:
conv_rhs at i => rw [← inf_inf_sdiff x y, inf_comm]

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

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

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ

case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α : Type u_7
β : Type u_8
⊢ Injective toSigma

Tactic:
rintro ⟨a, b⟩ ⟨c, d⟩ h
  simp_all

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  rw [sdiff_symmDiff, sdiff_sup]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint (a ∆ b) c

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]
  exact (ha.sup_left hb).disjoint_sdiff_left

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

Goal state before:
pp: α : Sort u_11
α' : Sort u_12
β : Sort u_13
β' : Sort u_14
ε₁ : α ≃ α'
ε₂ : β' ≃ β
f : α → β
f' : α' → β'
⊢ f = (⇑ε₂ ∘ f') ∘ ⇑ε₁ ↔ f = ⇑ε₂ ∘ f' ∘ ⇑ε₁

Tactic:
Function.comp_assoc

Goal state after:
α : Sort u_11
α' : Sort u_12
β : Sort u_13
β' : Sort u_14
ε₁ : α ≃ α'
ε₂ : β' ≃ β
f : α → β
f' : α' → β'
⊢ f = ⇑ε₂ ∘ f' ∘ ⇑ε₁ ↔ f = ⇑ε₂ ∘ f' ∘ ⇑ε₁
Module: Mathlib.Data.Set.Image

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

Tactic:
disjoint_iff_inter_eq_empty,

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ t = t₁

Tactic:
←
      snd_image_prod h.1 t,

Goal state after:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ Prod.snd '' s ×ˢ t = t₁
Module: Mathlib.Data.Set.Image

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

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ s ∩ t = ∅
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
e : M ≃* N
f : N →* P
⊢ (fun f ↦ f.comp ↑e.symm) (f.comp ↑e) = f

Tactic:
by simp [MonoidHom.comp_assoc]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOne N
inst✝ : MulOne P
g : N →* P
f₁ f₂ : M →* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
by rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]

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

Goal state before:
pp: a b c : ℤ
⊢ a.gcd ↑(b.gcd c) = a.gcd ↑(c.gcd b)

Tactic:
gcd_comm b c

Goal state after:
a b c : ℤ
⊢ a.gcd ↑(c.gcd b) = a.gcd ↑(c.gcd b)
Module: Mathlib.Algebra.Group.Basic

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

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

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 = 1

Tactic:
by
  rwa [LeftCancelMonoid.eq_one_of_mul_right h, one_mul] at h

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

Goal state before:
pp: α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

Tactic:
constructor <;> ext i

Goal state after:
case left
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ fst✝¹ i = fst✝ i

case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

Tactic:
constructor <;> ext i

Goal state after:
case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // p a }
⊢ ↑(fst✝¹ i) = ↑(fst✝ i)

case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // ¬p a }
⊢ ↑(snd✝¹ i) = ↑(snd✝ i)
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
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
hn : m ≤ n
⊢ Int.strongRec lt ge n = ge n hn fun k x ↦ Int.strongRec lt ge k

Tactic:
Int.strongRec,

Goal state after:
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
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
hn : m ≤ n
⊢ (if hnm : n < m then lt n hnm
    else
      ge n ⋯
        (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n 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 ⋯)) =
    ge n hn fun k x ↦ Int.strongRec lt ge k
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case neg
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
hlm : ¬l < m
⊢ (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

Tactic:
· rw [ih' fun l hl ↦ ih l (Int.lt_trans hl k.lt_succ), ih _ hl]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
⊢ (a + b) * (a + b) = a * a + 2 * a * b + b * b

Tactic:
by
  simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f g : Multiplicative ℕ →* M
h : f (ofAdd 1) = g (ofAdd 1)
n : Multiplicative ℕ
⊢ f (ofAdd 1) ^ toAdd n = g n

Tactic:
g.apply_mnat,

Goal state after:
M : Type u_1
inst✝ : Monoid M
f g : Multiplicative ℕ →* M
h : f (ofAdd 1) = g (ofAdd 1)
n : Multiplicative ℕ
⊢ f (ofAdd 1) ^ toAdd n = g (ofAdd 1) ^ toAdd n
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]

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

Goal state before:
pp: R : Type u
inst✝ : Distrib R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a + b) x y

Tactic:
simp only [SemiconjBy, left_distrib, right_distrib, ha.eq, hb.eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : ℕ
a✝ b✝ : M
u✝ u₁ u₂ u : Mˣ
a b : M
hu : a * b = ↑u
hc : Commute a b
⊢ b * ↑u⁻¹ * a = 1

Tactic:
have : Commute a u := hu ▸ (Commute.refl _).mul_right hc

Goal state after:
M : Type u_1
inst✝ : Monoid M
n : ℕ
a✝ b✝ : M
u✝ u₁ u₂ u : Mˣ
a b : M
hu : a * b = ↑u
hc : Commute a b
this : Commute a ↑u
⊢ b * ↑u⁻¹ * a = 1
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case neg
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

Tactic:
simp [Ring.not_isUnit_iff_inverse_eq_zero.mp h]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
⊢ Commute (↑0) x

Tactic:
rw [Nat.cast_zero]; exact Commute.zero_left x

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

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

Tactic:
dvd_iff_mod_eq_zero,

Goal state after:
m n : ℕ
⊢ m / n % 2 = 0 ↔ m % (2 * n) / n = 0
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 α
⊢ c ≤ c - b + b

Tactic:
← le_tsub_add

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ c ≤ c
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:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a - c ≤ b - (a + c)

case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - a - c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c d : α
⊢ a / b ≤ c / d ↔ a * d ≤ c * b

Tactic:
by
  simpa only [div_eq_mul_inv] using mul_inv_le_mul_inv_iff'

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ min a b < max c d

Tactic:
simp_rw [min_lt_iff, lt_max_iff]

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ (a < c ∨ a < d) ∨ b < c ∨ b < d
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
s : Semiring α
⊢ OfNat.ofNat (0 + 1) = OfNat.ofNat 0 + 1

Tactic:
simp [zero_add]

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ^ (n + 1) < 1

Tactic:
rw [pow_succ']; exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one₀ h₀ h₁.le)

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
⊢ 0 < a ^ 2

Tactic:
simpa only [sq] using mul_pos ha ha

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : IsEmpty α
a✝ : α ↪ β
v : α
⊢ a✝ v = { toFun := fun a ↦ isEmptyElim a, inj' := ⋯ } v

Tactic:
exact isEmptyElim v

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : LinearOrder R
a b : R
inst✝ : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b

Tactic:
by
  have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0
  refine this.eq_or_lt'.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩
  simpa only [pow_one] using h 1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ≃r s
a b : β
⊢ r (f.symm a) (f.symm b) ↔ s a b

Tactic:
erw [← f.map_rel_iff, f.1.apply_symm_apply, f.1.apply_symm_apply]

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:
by intro; exact f.complementedLattice

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
n : ℕ
a : G
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
obtain ha | ha := le_total a 1
  · rw [mabs_of_le_one ha, ← mabs_inv, ← inv_pow, mabs_of_one_le]
    exact one_le_pow_of_one_le' (one_le_inv'.2 ha) n
  · rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]

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

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

Tactic:
cases ha.false

Goal state after: