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

Goal state before:
pp: case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
a✝ : α
⊢ e (￢a✝) = ￢e a✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
⊢ Pairwise (Disjoint on extend e f ⊥)

Tactic:
intro b₁ b₂ hne

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) b₁ b₂
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊤ = ⊤

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊥ = ⊥

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ : α
⊢ e (￢a✝) = ￢e a✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := ⋯
booleanAlgebra : BooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := ⋯
booleanAlgebra : BooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ : α
⊢ e (￢a✝) = ￢e a✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
⊢ x ∈ s → ∀ y ∈ s, x ≤ y → Icc x y ⊆ s

Tactic:
hx

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
⊢ ∀ y ∈ s, x ≤ y → Icc x y ⊆ s
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : Std.Refl r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ a ∈ c, r (f b) (f a)

Tactic:
exact ⟨b, hb, refl _⟩

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
⊢ x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
hx

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
⊢ ∀ ⦃y : α⦄, y ∈ s → x = y
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ≤ ↑c

Tactic:
· exact (Subtype.mono_coe (· ∈ s)).csInf_image_le hct ⟨B, hB⟩

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
by
  rw [← cast_lt (K := K), cast_natCast]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
by
  rw [← cast_lt (K := K), cast_natCast]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
by
  rw [← cast_lt (K := K), cast_natCast]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
by
  rw [← cast_lt (K := K), cast_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑k = ↑(k * n) / ↑n

Tactic:
Int.cast_mul,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑k = ↑k * ↑n / ↑n
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ n < n !

Tactic:
have hn : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)

Goal state after:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n < n !
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
a b : ℕ+
h : b < a
⊢ ↑(↑a - ↑b).toPNat' = ↑a - ↑b

pp: case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(↑a - ↑b).toPNat' = 1

Tactic:
· exact toPNat'_coe (tsub_pos_of_lt h)

Goal state after:
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(↑a - ↑b).toPNat' = 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : fract a = fract b
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)

Tactic:
unfold fract at h; rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑q + -↑m₀ / ↑n) = fract (↑m₁ / ↑n)

Tactic:
← mul_div_cancel_right₀ (q : k) hn.ne',

Goal state after:
case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑q * ↑n / ↑n + -↑m₀ / ↑n) = fract (↑m₁ / ↑n)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
⊢ ↑q.num < (q - fract q + 1) * ↑q.den

Tactic:
suffices (q.num : ℚ) < q.num + (1 - fract q) * q.den by
    have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den := by
      calc
        (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
        _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
        _ = q.num + (1 - fract q) * q.den := by simp
    rwa [this]

Goal state after:
q : ℚ
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉ < b * a

Tactic:
rw [← sub_pos] at hb
    calc
      ⌈a⌉ < a + 1 := ceil_lt_add_one _
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ p /ₛ p = 1

Tactic:
by
  rw [← one_mul (p /ₛ p), ← smul_sdiv_assoc, smul_sdiv]

Goal state after:
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ List.count a _l ↔ replicate n a ≤ ↑_l

Tactic:
exact replicate_sublist_iff.symm.trans replicate_le_coe.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ range (map f) = {l | ∀ (x : β), x ∈ l → x ∈ range f}

Tactic:
refine antisymm (range_subset_iff.2 fun l => forall_mem_map.2 fun y _ => mem_range_self _)
      fun l hl => ?_
  induction l with
  | nil => exact ⟨[], rfl⟩
  | cons a l ihl =>
    rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩
    rcases hl a mem_cons_self with ⟨a, rfl⟩
    exact ⟨a :: l, map_cons⟩

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ map f s = 0 ↔ s = 0

Tactic:
← Multiset.card_eq_zero,

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ (map f s).card = 0 ↔ s = 0
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case e_tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
⊢ x ∈ l → elem x (take n l) = elem x (b :: List.filter (fun a ↦ elem a (take n l)) l)

Tactic:
hx

Goal state after:
case e_tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
⊢ elem x (take n l) = elem x (b :: List.filter (fun a ↦ elem a (take n l)) l)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
⊢ map f (s.erase x) = (map f s).erase (f x)

Tactic:
induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_
  by_cases hxy : y = x
  · cases hxy
    simp
  · rw [s.erase_cons_tail hxy, map_cons, map_cons, (s.map f).erase_cons_tail (hf.ne hxy), ih]

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr f x s)

Tactic:
induction s using Multiset.induction with
  | empty => simpa
  | cons a s ihs =>
    simp only [forall_mem_cons, foldr_cons] at q_s ⊢
    exact hpqf _ _ q_s.1 (ihs q_s.2)

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ (a :: l).dedup = if a ∈ l then l.dedup else a :: l.dedup

Tactic:
by
  simpa using dedup_cons' a l

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
a : α
⊢ a ∈ xs → a ∈ ys.dedup → False

Tactic:
hx

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
a : α
hx : a ∈ xs
⊢ a ∈ ys.dedup → False
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
by
  by_cases h : a ∈ s <;> simp [h]

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
rw [← coe_eq_singleton]

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ ↑s = {a} ∨ s.Nontrivial
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
s : Finset α
hs : s.Nonempty
⊢ motive s hs

Tactic:
induction s using Finset.cons_induction with
  | empty => exact (not_nonempty_empty hs).elim
  | cons a t ha h =>
    obtain rfl | ht := t.eq_empty_or_nonempty
    · exact singleton a
    · exact cons a t ha ht (h ht)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
ι : Type u_4
s : Set ι
f : ι → Finset α
⊢ s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Tactic:
simp [Set.PairwiseDisjoint, Set.Pairwise, not_imp_comm (a := _ = _),
    not_disjoint_iff_nonempty_inter]

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a ↦ insert a s) ↑sᶜ

Tactic:
by
  rw [coe_compl]
  exact s.insert_inj_on

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
⊢ x ∈ map f.toEmbedding s → x ∈ t

Tactic:
hx

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : x ∈ map f.toEmbedding s
⊢ x ∈ t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
⊢ x ∈ s → x ∈ map f.symm.toEmbedding t

Tactic:
hx

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ x ∈ map f.symm.toEmbedding t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.hf
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.MapsTo f' ↑s ↑t

pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.InjOn f' ↑s

Tactic:
· aesop (add safe unfold Set.MapsTo)

Goal state after:
case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.InjOn f' ↑s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : ↑t ⊆ f '' ↑s
⊢ #t ≤ #s

Tactic:
exact (card_le_card (mod_cast hf)).trans card_image_le

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
⊢ x ∈ ↑s → ∀ ⦃x₂ : α⦄, x₂ ∈ ↑s → f x = f x₂ → x = x₂

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
hx : x ∈ ↑s
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ ↑s → f x = f x₂ → x = x₂
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ ↑(last n - i) = ↑i.rev

Tactic:
rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
this : b.castLT ⋯ ≤ a.castLT ha
⊢ ↑(a.castLT ha - b.castLT ⋯) = ↑(a - b)

Tactic:
simp [sub_val_of_le, h, this]

Goal state after: