mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m

Tactic:
congr

Goal state after:
case e_a
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m = 1 * npowRec' k.succ m
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
by rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]

Goal state after:
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

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

case neg
α : Sort u_1
P : Prop
inst✝ : Decidable P
c : α
A : P → α
B : ¬P → α
h✝ : ¬P
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ { beq := beq1 } = inst2

Tactic:
congr

Goal state after:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ beq1 = BEq.beq
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a ↦ p a) a
he : ∀ (y : α), (fun a ↦ p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ ⟨b, hb⟩ = default

Tactic:
congr

Goal state after:
α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a ↦ p a) a
he : ∀ (y : α), (fun a ↦ p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ b = a
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ { default := x, uniq := h } = { default := y, uniq := uniq✝ }

Tactic:
congr

Goal state after:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
y : α
x✝ : { x // x = y }
x : α
hx : x = y
⊢ ⟨x, hx⟩ = ⟨y, ⋯⟩

Tactic:
congr

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
y : α
x✝ : { x // y = x }
⊢ ⟨y, ⋯⟩ = ⟨y, ⋯⟩

Tactic:
congr

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! x, p (f x)
x : α
hpx : (fun x ↦ p (f x)) x
hx : ∀ (y : α), (fun x ↦ p (f x)) y → y = x
y : β
hy : (fun y ↦ p y) y
z : α
hz : f z = y
⊢ (fun x ↦ p (f x)) z

Tactic:
simpa [hz]

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
h : g s = g t
⊢ cast hU (g s).snd = cast hU (g t).snd

Tactic:
congr

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
⊢ False

Tactic:
| intro U hU =>

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ (if h : ∃ a, f a = b then g (Classical.choose h) else e' b) =
    if h : ∃ a, f a = b then g (Classical.choose h) else e' b

Tactic:
congr

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

Goal state before:
pp: α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
x : α
⊢ ∀ ⦃y : α⦄, x ≠ y → ∃ f, f ∈ B ∧ f x ≠ f y

Tactic:
y

Goal state after:
α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
x y : α
⊢ x ≠ y → ∃ f, f ∈ B ∧ f x ≠ f y
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
n✝ n : ℕ
ihn : id^[n] = id
⊢ id^[n.succ] = id

Tactic:
iterate_succ,

Goal state after:
α : Type u
n✝ n : ℕ
ihn : id^[n] = id
⊢ id^[n] ∘ id = id
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[(m + n).succ] = f^[m] ∘ f^[n.succ]

Tactic:
iterate_succ,

Goal state after:
α : Type u
f : α → α
m n : ℕ
⊢ f^[m + n] ∘ f = f^[m] ∘ f^[n.succ]
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[m + n] ∘ f = f^[m] ∘ f^[n.succ]

Tactic:
iterate_succ,

Goal state after:
α : Type u
f : α → α
m n : ℕ
⊢ f^[m + n] ∘ f = f^[m] ∘ f^[n] ∘ f
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: case mk.mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : RightInverse invFun✝¹ toFun✝¹
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
h₁ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun
h₂ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ g ∘ f^[m + 1] = g

Tactic:
iterate_succ,

Goal state after:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ g ∘ f^[m] ∘ f = g
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
⊢ f^[n.succ] = f ∘ f^[n]

Tactic:
iterate_succ,

Goal state after:
α : Type u
f : α → α
n : ℕ
⊢ f^[n] ∘ f = f ∘ f^[n]
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_7
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : SMul P Q
inst✝³ : FaithfulSMul P Q
inst✝² : IsScalarTower M N Q
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
p : P
⊢ (m • n) • p = m • n • p

Tactic:
by simp_rw [← (smul_left_injective' (α := Q)).eq_iff, smul_assoc]

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d

Tactic:
· exact ⟨b, inr_injective h⟩

Goal state after:
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
G : Type u_9
P : Type u_10
inst✝¹ : Group G
inst✝ : MulAction G P
a : G
b c : P
h : a • b = a • c
⊢ b = c

Tactic:
by rw [← inv_smul_smul a b, h, inv_smul_smul]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β

Tactic:
isEmpty_pi,

Goal state after:
α : Sort u_1
β : Sort u_2
⊢ (∃ a, IsEmpty β) ↔ Nonempty α ∧ IsEmpty β
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ (∃ a, IsEmpty β) ↔ (∃ x, True) ∧ IsEmpty β

Tactic:
← exists_and_right,

Goal state after:
α : Sort u_1
β : Sort u_2
⊢ (∃ a, IsEmpty β) ↔ ∃ x, True ∧ IsEmpty β
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : β
c : γ
⊢ Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (inr i) c

Tactic:
simp only [Pi.mulSingle, Sum.elim_update_right, elim_one_one]

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

Goal state before:
pp: α : Type u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }

Tactic:
congr

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

Goal state before:
pp: α : Sort u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }

Tactic:
congr

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case refl
α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
⊢ { le := le✝, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff } =
    { le := le✝, lt := A_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }

Tactic:
congr

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ { toPreorder := toPreorder✝, le_antisymm := le_antisymm✝¹ } =
    { toPreorder := toPreorder✝, le_antisymm := le_antisymm✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case refl.refl
α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
this : A_compare = B_compare
⊢ { le := A_le, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := lt_iff_le_not_ge✝¹,
      le_antisymm := le_antisymm✝¹, min := A_min, max := A_max, compare := A_compare, le_total := le_total✝¹,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := A_min_def, max_def := A_max_def, compare_eq_compareOfLessAndEq := A_compare_canonical } =
    { le := A_le, lt := A_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := lt_iff_le_not_ge✝,
      le_antisymm := le_antisymm✝, min := A_min, max := A_max, compare := B_compare, le_total := le_total✝,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := B_min_def, max_def := B_max_def, compare_eq_compareOfLessAndEq := B_compare_canonical }

Tactic:
congr

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ { bot := a, bot_le := ha } = { bot := b, bot_le := hb }

Tactic:
congr

Goal state after:
α : Type u
β : Type v
inst✝ : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ a = b
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
⊢ { toOrderTop := toOrderTop✝¹, toOrderBot := toOrderBot✝¹ } = { toOrderTop := toOrderTop✝, toOrderBot := toOrderBot✝ }

Tactic:
congr

Goal state after:
case e_toOrderTop
α : Type u
β : Type v
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
⊢ toOrderTop✝¹ = toOrderTop✝

case e_toOrderBot
α : Type u
β : Type v
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
⊢ toOrderBot✝¹ = toOrderBot✝
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: a b c : ℕ
⊢ a / b / c = a / c / b

Tactic:
rw [Nat.div_div_eq_div_mul, Nat.mul_comm, ← Nat.div_div_eq_div_mul]

Goal state after:
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 : ℕ), Injective next
x : C n
⊢ ∀ ⦃a₂ : C n⦄, leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) a₂ → x = a₂

Tactic:
y

Goal state after:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x y : C n
⊢ leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) y → x = y
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x : C n
⊢ ∀ ⦃a₂ : C n⦄, leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) a₂ → x = a₂

Tactic:
y

Goal state after:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x y : C n
⊢ leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) y → x = y
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a * a ^ b

Tactic:
exact Nat.mul_le_mul_left a (Nat.lt_pow_self ha1)

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝¹ x✝ : α × β
a₁ : α
a₂ b₂ : β
hab : ¬Prod.Lex r s (a₁, a₂) (a₁, b₂)
hba : ¬Prod.Lex r s (a₁, b₂) (a₁, a₂)
⊢ (a₁, a₂) = (a₁, b₂)

Tactic:
obtain rfl := Std.Trichotomous.trichotomous a₂ b₂
      (mt (Prod.Lex.right a₁) hab) (mt (Prod.Lex.right a₁) hba)

Goal state after:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝¹ x✝ : α × β
a₁ : α
a₂ : β
hab hba : ¬Prod.Lex r s (a₁, a₂) (a₁, a₂)
⊢ (a₁, a₂) = (a₁, a₂)
Module: Mathlib.Order.PropInstances

Goal state before:
pp: P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
by_cases P

Goal state after:
case pos
P Q : Prop
h✝ : P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

case neg
P Q : Prop
h✝ : ¬P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
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 : α
⊢ ∀ ⦃b : α⦄, x < b → (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) b

Tactic:
y

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 : α
⊢ 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.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ s ∩ {a | p a} = s ∩ {x | x ∈ t ∧ p x}

Tactic:
← inter_ofPred_eq_sep t p,

Goal state after:
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ s ∩ {a | p a} = s ∩ (t ∩ {a | p a})
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mpr
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b

Tactic:
rintro ⟨c, rfl : _ = _ ⊔ _⟩

Goal state after:
case mpr
α : Type u
inst✝ : SemilatticeSup α
a c : α
⊢ a ≤ a ⊔ c
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mk.mk.refl
α : Type u_1
toPartialOrder✝ : PartialOrder α
sup✝¹ : α → α → α
le_sup_left✝¹ : ∀ (a b : α), a ≤ sup✝¹ a b
le_sup_right✝¹ : ∀ (a b : α), b ≤ sup✝¹ a b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝¹ a b ≤ c
sup✝ : α → α → α
le_sup_left✝ : ∀ (a b : α), a ≤ sup✝ a b
le_sup_right✝ : ∀ (a b : α), b ≤ sup✝ a b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝ a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ { toPartialOrder := toPartialOrder✝, sup := sup✝¹, le_sup_left := le_sup_left✝¹, le_sup_right := le_sup_right✝¹,
      sup_le := sup_le✝¹ } =
    {
      toPartialOrder :=
        { toPartialOrder := toPartialOrder✝, sup := sup✝¹, le_sup_left := le_sup_left✝¹, le_sup_right := le_sup_right✝¹,
            sup_le := sup_le✝¹ }.toPartialOrder,
      sup := sup✝, le_sup_left := le_sup_left✝, le_sup_right := le_sup_right✝, sup_le := sup_le✝ }

Tactic:
congr

Goal state after:
case e_sup
α : Type u_1
toPartialOrder✝ : PartialOrder α
sup✝¹ : α → α → α
le_sup_left✝¹ : ∀ (a b : α), a ≤ sup✝¹ a b
le_sup_right✝¹ : ∀ (a b : α), b ≤ sup✝¹ a b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝¹ a b ≤ c
sup✝ : α → α → α
le_sup_left✝ : ∀ (a b : α), a ≤ sup✝ a b
le_sup_right✝ : ∀ (a b : α), b ≤ sup✝ a b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝ a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ sup✝¹ = sup✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mk.mk.refl.refl
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
inf✝ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ { toSemilatticeSup := toSemilatticeSup✝, inf := inf✝, inf_le_left := inf_le_left✝¹, inf_le_right := inf_le_right✝¹,
      le_inf := le_inf✝¹ } =
    {
      toSemilatticeSup :=
        { toSemilatticeSup := toSemilatticeSup✝, inf := inf✝, inf_le_left := inf_le_left✝¹,
            inf_le_right := inf_le_right✝¹, le_inf := le_inf✝¹ }.toSemilatticeSup,
      inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝, le_inf := le_inf✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x : α
⊢ ∀ ⦃b : α⦄, x ≤ b → f x ≤ f b

Tactic:
y

Goal state after:
α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
⊢ x ≤ y → f x ≤ f y
Module: Mathlib.Order.GaloisConnection.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
⊢ (∀ (b : α) (a : β), u a ≤ b ↔ a ≤ l b) = ∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a

Tactic:
simp only [Iff.comm]

Goal state after:
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

Goal state after:
case le
α : 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
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : 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
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case min
α : 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
x✝ y✝ : α
⊢ e (x✝ ⊓ y✝) = Min.min (e x✝) (e y✝)

case max
α : 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
x✝ y✝ : α
⊢ e (x✝ ⊔ y✝) = Max.max (e x✝) (e y✝)

case compare
α : 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
x✝ y✝ : α
⊢ Ord.compare (e x✝) (e y✝) = Ord.compare x✝ y✝
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ b ≤ a ⇨ c

Tactic:
by rw [le_himp_iff, le_himp_iff']

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

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

Tactic:
rw [← disjoint_iff]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ Disjoint z (y \ x) ↔ z ≤ x
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
⊢ GeneralizedCoheytingAlgebra α

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

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

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

Tactic:
by rw [← sdiff_eq, sup_inf_sdiff _ _]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a \ b)ᶜ ⊓ (b \ a)ᶜ = a ⇔ b

Tactic:
compl_sdiff,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ (b ⇨ a) = a ⇔ b
Module: Mathlib.Order.SymmDiff

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

Tactic:
{ rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc] }

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

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage f^[n + 1] = (preimage f)^[n + 1]

Tactic:
iterate_succ,

Goal state after:
case succ
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage (f^[n] ∘ f) = (preimage f)^[n + 1]
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
⊢ preimage f^[n] = (preimage f)^[n]

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
⊢ f ⁻¹' s ⊆ t

Tactic:
rintro a ha

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
⊢ a ∈ 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:
rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
    image_empty]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
⊢ ∀ (y : α), y ∈ s₂ → f x ≠ f y

Tactic:
y

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
⊢ y ∈ s₂ → f x ≠ f y