mathlib-initiative/mathlib-tactics huggingface dataset:
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:
Nat.binaryRec_eq _ _ (Or.inl rfl),

Goal state after:
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))
      k' (bif b then m * n else m) (n * n) =
    m * npowRec' (Nat.bit b k') n
Module: Mathlib.Logic.ExistsUnique

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

Tactic:
simp only [existsUnique_iff_exists] at h₂
  apply h₂.elim
  exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
b c : α
h : b = c
a : α
⊢ a = b ↔ a = c

Tactic:
h

Goal state after:
α : Sort u_1
b c : α
h : b = c
a : α
⊢ a = c ↔ a = c
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
⊢ a = b

Tactic:
h

Goal state after:
α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
⊢ b = b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a✝ b : α
h : a✝ = b
a : α
⊢ a✝ = a ↔ b = a

Tactic:
h

Goal state after:
α : Sort u_1
a✝ b : α
h : a✝ = b
a : α
⊢ b = a ↔ b = a
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
a : α
b : β
e : β = α
⊢ a = cast e b → a ≍ b

Tactic:
rintro rfl; simp

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

Goal state before:
pp: α : 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⟩
s t : Set T
⊢ g s = g t → s = t

Tactic:
h

Goal state after:
α : 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⟩
s t : Set T
h : g s = g t
⊢ s = t
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ update f a' b a = if a = a' then b else f a

Tactic:
rcases Decidable.eq_or_ne a a' with rfl | hne <;> simp [*]

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

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ f x = f (f (f x))

Tactic:
h

Goal state after:
α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ f x = f x
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ C (g (f a)) ≍ C a

Tactic:
h

Goal state after:
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ C a ≍ C a
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : SymmGen r b a
⊢ SymmGen (Function.swap r) a b

Tactic:
induction h with

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

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
b : α
motive : (a : α) → ReflTransGen r a b → Prop
a : α
h : ReflTransGen r a b
refl : motive b ⋯
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯
⊢ motive a h

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
h : ReflTransGen r a b
refl : ∀ (a : α), motive ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive h

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inl.inr.refl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
be : r b✝ c✝
ec : ReflTransGen r c✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
exact Or.inl ec

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a i✝ : α
⊢ TransGen r a i✝ ≤ ReflTransGen r a i✝

Tactic:
h

Goal state after:
α : Type u_1
r : α → α → Prop
a i✝ : α
h : TransGen r a i✝
⊢ ReflTransGen r a i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a i✝ : α
h : TransGen r a i✝
⊢ ReflTransGen r a i✝

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
b : α
motive : (a : α) → TransGen r a b → Prop
a : α
h : TransGen r a b
single : ∀ {a : α} (h : r a b), motive a ⋯
head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯
⊢ motive a h

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
h : TransGen r a b
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive h

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ b, r a b ∧ ReflTransGen r b c

Tactic:
induction h with

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 : TransGen r x y
⊢ TransGen r y x

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
a b : α
h : TransGen r a b
⊢ r a b

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
⊢ Function.swap (TransGen r) i✝¹ i✝ ≤ TransGen (Function.swap r) i✝¹ i✝

Tactic:
h

Goal state after:
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : Function.swap (TransGen r) i✝¹ i✝
⊢ TransGen (Function.swap r) i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
i✝¹ i✝ b✝ c✝ : α
a✝ : TransGen r i✝ b✝
hbc : r b✝ c✝
ih : TransGen (Function.swap r) b✝ i✝
⊢ TransGen (Function.swap r) c✝ i✝

Tactic:
| tail _ hbc ih =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : Function.swap (TransGen r) i✝¹ i✝
⊢ TransGen (Function.swap r) i✝¹ i✝

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : IsTrans α r
a b : α
h : ReflTransGen r a b
⊢ r a b

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
⊢ Function.swap (ReflTransGen r) i✝¹ i✝ ≤ ReflTransGen (Function.swap r) i✝¹ i✝

Tactic:
h

Goal state after:
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : Function.swap (ReflTransGen r) i✝¹ i✝
⊢ ReflTransGen (Function.swap r) i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
i✝¹ i✝ b✝ c✝ : α
a✝ : ReflTransGen r i✝ b✝
hbc : r b✝ c✝
ih : ReflTransGen (Function.swap r) b✝ i✝
⊢ ReflTransGen (Function.swap r) c✝ i✝

Tactic:
| tail _ hbc ih =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : Function.swap (ReflTransGen r) i✝¹ i✝
⊢ ReflTransGen (Function.swap r) i✝¹ i✝

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ : α
⊢ EqvGen r i✝¹ i✝ ≤ EqvGen p i✝¹ i✝

Tactic:
h

Goal state after:
α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ : α
h : EqvGen r i✝¹ i✝
⊢ EqvGen p i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ : α
h : EqvGen r i✝¹ i✝
⊢ EqvGen p i✝¹ i✝

Tactic:
induction h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
⊢ TransGen r i✝¹ i✝ ≤ EqvGen r i✝¹ i✝

Tactic:
h

Goal state after:
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : TransGen r i✝¹ i✝
⊢ EqvGen r i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
⊢ ReflTransGen r i✝¹ i✝ ≤ EqvGen r i✝¹ i✝

Tactic:
h

Goal state after:
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : ReflTransGen r i✝¹ i✝
⊢ EqvGen r i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h✝ : Equivalence r
h : EqvGen r a b
⊢ r a b

Tactic:
induction h with

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
⊢ extend (⇑f) g e' b = g (f.symm b)

Tactic:
← f.apply_symm_apply b,

Goal state after:
α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
⊢ extend (⇑f) g e' (f (f.symm b)) = g (f.symm (f (f.symm b)))
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ (r • 1) • s • x = s • r • x

Tactic:
smul_comm,

Goal state after:
M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ s • (r • 1) • x = s • r • x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ (r • 1) • (s • 1) • x = s • r • 1 • x

Tactic:
smul_comm,

Goal state after:
A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ (s • 1) • (r • 1) • x = s • r • 1 • x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower N P Q
m : M
p : P
q : Q
⊢ (m • p) • q = m • p • q

Tactic:
rw [← smul_one_smul N m, smul_assoc, smul_one_smul]

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) → DivisionMonoid (f i)
a✝ b✝ : (i : I) → f i
⊢ a✝ * b✝ = 1 → a✝⁻¹ = b✝

Tactic:
h

Goal state after:
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) → DivisionMonoid (f i)
a✝ b✝ : (i : I) → f i
h : a✝ * b✝ = 1
⊢ a✝⁻¹ = b✝
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
⊢ (a, b₁) = (a, b₂) → b₁ = b₂

Tactic:
h

Goal state after:
α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
⊢ (fun a ↦ (a, b)) b₁ = (fun a ↦ (a, b)) b₂ → b₁ = b₂

Tactic:
h

Goal state after:
α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
h : (fun a ↦ (a, b)) b₁ = (fun a ↦ (a, b)) b₂
⊢ b₁ = b₂
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Tactic:
have := Nonempty.map f ‹_›

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this : Nonempty γ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Type u_1
a b : ULift α
h : a = b
⊢ a.down = b.down

Tactic:
h

Goal state after:
α : Type u_1
a b : ULift α
h : a = b
⊢ b.down = b.down
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Sort u_1
a b : PLift α
h : a = b
⊢ a.down = b.down

Tactic:
h

Goal state after:
α : Sort u_1
a b : PLift α
h : a = b
⊢ b.down = b.down
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
⊢ Injective (@toPreorder α)

Tactic:
by
  rintro ⟨⟩ ⟨⟩ ⟨⟩; congr

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y

Tactic:
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
    · exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_ge h.1⟩
    · exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_ge h.2⟩

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

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

Tactic:
not_lt,

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

Goal state before:
pp: m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ m ∣ n ↔ n✝ ∣ n

Tactic:
h

Goal state after:
m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n✝ ∣ n ↔ n✝ ∣ n
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n ∣ m ↔ n ∣ n✝

Tactic:
h

Goal state after:
m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n ∣ n✝ ↔ n ∣ n✝
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'
⊢ cmp x y = lt ↔ cmp x' y' = lt

Tactic:
h

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp x' y' = lt ↔ cmp x' y' = lt
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hac : r a c
⊢ r a c

pp: case inr.inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
hab : r a b
hbc : r b a
⊢ r a a

pp: case inr.inr
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c

Tactic:
· exact hac

Goal state after:
case inr.inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
hab : r a b
hbc : r b a
⊢ r a a

case inr.inr
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Bounded r s ↔ Unbounded r s

Tactic:
not_bounded_iff

Goal state after:
α : Type u
r : α → α → Prop
s : Set α
⊢ Unbounded r s ↔ Unbounded r s
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
⊢ x < y → (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
h

Goal state after:
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f (x ⊓ y) = f x

Tactic:
inf_eq_left.2 hxy

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f x = f x
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
⊢ LinearOrder α

Tactic:
apply e.injective.linearOrder <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ map e (map e.symm y) = y

Tactic:
convert! (congr_fun (EquivFunctor.map_trans' e.symm e) y).symm
    simp

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
x : f α
⊢ ⇑(k.trans h) <$> x = (Functor.map ⇑h ∘ Functor.map ⇑k) x

Tactic:
apply LawfulFunctor.comp_map k h x

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
⊢ (if a ≤ b then ⊥ else a) ≤ c ↔ a ≤ max b c

Tactic:
split_ifs with h
      · exact iff_of_true bot_le (le_sup_of_le_left h)
      · rw [le_sup_iff, or_iff_right h]

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

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

Tactic:
by rw [inf_sup_right, inf_comm x y, inf_inf_sdiff, sdiff_inf_sdiff, bot_sup_eq]

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
⊢ a = b ∧ f ≍ g

Tactic:
rcases ‹Nonempty γ› with ⟨i⟩

Goal state after:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
i : γ
⊢ a = b ∧ f ≍ g
Module: Mathlib.Order.BooleanAlgebra.Basic

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

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

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

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Sum.elim Subtype.val Subtype.val ((fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) a) = a

Tactic:
by
    dsimp
    split_ifs <;> rfl

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

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

Tactic:
h

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ z \ y ⊔ y ≤ z \ y ⊔ y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl x y

Tactic:
h

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl yᶜ y
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
h

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if j = j ∨ j ∈ s then f j else g j) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) j
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
⊢ Prod.snd '' s ×ˢ t = Prod.snd '' s₁ ×ˢ t₁

Tactic:
heq

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₁ = Prod.snd '' s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp.h₁
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ f ⁻¹' s ⊆ f ⁻¹' t

Tactic:
h

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

Goal state before:
pp: case mp.h₂
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ f ⁻¹' t ⊆ f ⁻¹' s

Tactic:
h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' s = f '' t → s = t

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ s = t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ f ⁻¹' f '' s = f ⁻¹' f '' t

Tactic:
h

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

pp: case refine_2
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂ → f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i

Tactic:
· constructor <;>
      · rintro i ⟨his, hpi⟩
        simpa [*] using h i

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂ → f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
⊢ f ⁻¹' (s ∪ t) = ⊤

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
⊢ f ⁻¹' ⊤ = ⊤