mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑k

Tactic:
exact k.cast_nonneg'

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab : a ≤ b
c : α
hc : c ≠ 0
⊢ a * c ≤ b * c

Tactic:
obtain rfl | hab := hab.eq_or_lt

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b : α
n : ℕ
a c : α
hc : c ≠ 0
hab : a ≤ a
⊢ a * c ≤ a * c

case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab✝ : a ≤ b
c : α
hc : c ≠ 0
hab : a < b
⊢ a * c ≤ b * c
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case refine_3.inl
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y : αˣ
h : 0 < ↑y
⊢ ∃ a, 0 < a ∧ a < ↑y

Tactic:
obtain ⟨z, hz⟩ := exists_one_lt' (α := αˣ)
      exact ⟨(y * z⁻¹ : αˣ), by simp, Units.val_lt_val.mpr <| by simp [hz]⟩

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
⊢ DenselyOrdered (WithBot α) ↔ DenselyOrdered α

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
⊢ DenselyOrdered α

case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ DenselyOrdered (WithBot α)
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered (WithTop α) ↔ DenselyOrdered α

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
⊢ DenselyOrdered α

case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ DenselyOrdered (WithTop α)
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ f 1 = 0

Tactic:
← Units.mul_inv a,

Goal state after:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ f (↑a * ↑a⁻¹) = 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0

Tactic:
refine ⟨lt_imp_lt_of_le_imp_le (pow_nonneg · _), fun ha ↦ ?_⟩
  obtain ⟨k, rfl⟩ := hn
  rw [pow_succ]
  exact mul_neg_of_pos_of_neg ((even_two_mul _).pow_pos ha.ne) ha

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ a * a = b * b

Tactic:
← abs_mul_abs_self,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ |a| * |a| = b * b
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| < |b| ↔ a * a < b * b

Tactic:
← abs_mul_abs_self,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| < |b| ↔ |a| * |a| < b * b
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ a * a ≤ b * b

Tactic:
← abs_mul_abs_self,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ b * b
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if h : p i then update v j x (e ⟨i, h⟩) else w i) =
    update (fun i ↦ if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x i

Tactic:
simp only [h, update_apply]
    aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (s ∪ t) t

Tactic:
rintro a (has | hat)
  · exact hc has
  · exact ⟨a, hat, le_rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
⊢ y ∈ s → ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
hy

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
⊢ j = i ∨ Iio i = Iic j

Tactic:
rcases eq_or_lt_of_le (le_of_isLUB_Iio i hj) with hj_eq_i | hj_lt_i

Goal state after:
case inl
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_eq_i : j = i
⊢ j = i ∨ Iio i = Iic j

case inr
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
hb : 0 < b
⊢ 0 < a / b ↔ 0 < a

Tactic:
by
  simp only [div_eq_mul_inv, mul_pos_iff_of_pos_right (inv_pos.2 hb)]

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

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

Tactic:
refine ⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩

Goal state after:
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
⊢ a ≤ b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
rw [← neg_pos, ← inv_neg, inv_pos, neg_pos]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ f x✝ (f y✝ (foldr f b l₁✝)) = f x✝ (f y✝ (foldr f b l₂✝))

Tactic:
r b

Goal state after:
case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ f x✝ (f y✝ (foldr f b l₂✝)) = f x✝ (f y✝ (foldr f b l₂✝))
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (a_1 : α), count a_1 l = count a_1 (replicate m a ++ replicate n b)) ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
← Decidable.and_forall_ne a,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      ∀ (b_1 : α), b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ foldr (fun x y ↦ f (f₁ x) (f₂ x) * y) 1 l = foldr (fun x y ↦ f (f₁ x) (f₂ x) * y) (f 1 1) l

Tactic:
hf'

Goal state after:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ foldr (fun x y ↦ f (f₁ x) (f₂ x) * y) 1 l = foldr (fun x y ↦ f (f₁ x) (f₂ x) * y) 1 l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?

Tactic:
by rintro rfl _ _; rfl

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

Goal state before:
pp: case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ a * ((take n L).prod * (drop (n + 1) L).prod) = L.prod * (L[n]⁻¹ * a)

Tactic:
prod_drop_succ L n hn,

Goal state after:
case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ a * ((take n L).prod * (L[n]⁻¹ * (drop n L).prod)) = L.prod * (L[n]⁻¹ * a)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ den ^ n ≠ 0

Tactic:
by simp [Nat.pow_eq_zero, hd]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
x✝ : d ∣ 1
e : α
he : 1 = d * e
⊢ x = y * e

Tactic:
rw [hd, mul_assoc, ← he, mul_one]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a a' : R
p : a = a'
e : ℕ
hone : Nat.rawCast 1 = e
⊢ a = a' ^ e * Nat.rawCast 1

Tactic:
simp [← hone, *]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : Bool → α
⊢ ⨆ b, f b = f true ⊔ f false

Tactic:
rw [iSup, Bool.range_eq, sSup_pair, sup_comm]

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

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨆ i, ⨆ (hi : p i), u (f i hi)) = ⨆ i, ⨆ (hi : p i), f i hi

Tactic:
simp only [iSup_subtype', gi.l_iSup_u]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ ⨆ j, extend e f ⊥ j = ⨆ i, f i

Tactic:
rw [iSup_split _ fun j => ∃ i, e i = j]

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ (⨆ i, ⨆ (_ : ∃ i_1, e i_1 = i), extend e f ⊥ i) ⊔ ⨆ i, ⨆ (_ : ¬∃ i_1, e i_1 = i), extend e f ⊥ i = ⨆ i, f i
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → Set α
⊢ ⋂ x, ⋂ y, ⋂ (h : p y ∧ q x y), s x y h = ⋂ y, ⋂ (hy : p y), ⋂ x, ⋂ (hx : q x y), s x y ⋯

Tactic:
simp only [iInter_and, @iInter_comm _ ι]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨅ j, f i j = ⨅ g, ⨆ i, f i (g i)

Tactic:
refine le_antisymm iSup_iInf_le ?_
  rw [minAx.iInf_iSup_eq']
  refine iSup_le fun g => ?_
  have ⟨a, ha⟩ : ∃ a, ∀ b, ∃ f, ∃ h : a = g f, h ▸ b = f (g f) := by
    by_contra! h
    choose h hh using h
    have := hh _ h rfl
    contradiction
  refine le_trans ?_ (le_iSup _ a)
  refine le_iInf fun b => ?_
  obtain ⟨h, rfl, rfl⟩ := ha b
  exact iInf_le _ _

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : Lattice α
inst✝ : Fact (a ≤ b)
x y : ↑(Icc a b)
⊢ IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ ↑x ⊔ ↑y = b

Tactic:
rw [_root_.isCompl_iff, Icc.disjoint_iff, Icc.codisjoint_iff]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ sSup ∅ ≤ sSup t

Tactic:
rw [csSup_empty]

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ ⊥ ≤ sSup t
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
⊢ CompleteDistribLattice α

Tactic:
let completeLattice := e.completeLattice
  let biheytingAlgebra := e.biheytingAlgebra
  apply e.injective.completeDistribLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case mpr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.1.not_gt <| lt_min hfba hfbc⟩

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
⊢ CompleteAtomicBooleanAlgebra α

Tactic:
by
  let completeBooleanAlgebra := e.completeBooleanAlgebra
  apply e.injective.completeAtomicBooleanAlgebra <;> intros <;>
  first | rfl | 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 : α
hx : x ∈ s
y : α
⊢ y ∈ s → x ≤ y → Icc x y ⊆ s

Tactic:
hy

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 : α
hy : y ∈ s
⊢ x ≤ y → Icc x y ⊆ s
Module: Mathlib.Order.Antichain

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

Tactic:
hy

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : 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.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k + 1) ≤ (n + k + 1) ^ k * (n + k + 1)

Tactic:
exact Nat.mul_le_mul_right _
      (Nat.le_trans (ascFactorial_le_pow_add _ k) (Nat.pow_le_pow_left (le_succ _) _))

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1).ascFactorialBinary k

Tactic:
← ascFactorial_eq_ascFactorialBinary,

Goal state after:
case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1).ascFactorial k
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: k m : ℕ+
⊢ k ∣ m ↔ ↑k ∣ ↑m

Tactic:
constructor <;> intro h

Goal state after:
case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m

case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
y : R
hys : y ∈ s
h0 : 0 ≤ y - ↑⌊y⌋
h1 : y - ↑⌊y⌋ < 1
⊢ ∃ x ∈ s, fract x = y - ↑⌊y⌋

Tactic:
exact ⟨y, hys, rfl⟩

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
r : α
n d : ℕ
⊢ IsNNRat r n d → IsNat ⌈r⌉ (-(-↑n / ↑d)).toNat

Tactic:
by
  rintro ⟨inv, rfl⟩
  constructor
  simp only [invOf_eq_inv, ← div_eq_mul_inv]
  rw [← ceil_intCast_div_natCast n d, ← ceil_cast (α := α), Rat.cast_div,
    cast_intCast, cast_natCast, Int.cast_natCast,
    Int.natCast_toNat_eq_self.mpr (ceil_nonneg (div_nonneg n.cast_nonneg d.cast_nonneg))]

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

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, b * a ^ (Equiv.neg ℤ) x ∈ Ico c (c * a)

Tactic:
simpa only [Equiv.neg_apply, mem_Ico, zpow_neg, ← div_eq_mul_inv, le_div_iff_mul_le, one_mul,
      mul_comm c, div_lt_iff_lt_mul, mul_assoc] using existsUnique_zpow_near_of_one_lt' ha (b / c)

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ f (x + ↑n) = f x + n • b

Tactic:
rw [← map_add_zsmul f x n, zsmul_one]

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

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

Tactic:
calc
    b * a < b * (⌊a⌋ + 1) := by gcongr; apply lt_floor_add_one
    _ ≤ ⌊a⌋ := by
      rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le, le_floor]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
⊢ Subsingleton (FloorRing R)

Tactic:
by
  refine ⟨fun H₁ H₂ => ?_⟩
  have : H₁.floor = H₂.floor :=
    funext fun a => (H₁.gc_coe_floor.u_unique H₂.gc_coe_floor) fun _ => rfl
  have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil_coe.l_unique H₂.gc_ceil_coe) fun _ => rfl
  cases H₁; cases H₂; congr

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ countP (r x) (y ::ₘ s) = countP (r x) (b ::ₘ bs)

Tactic:
rw [countP_cons, countP_cons, ih hb2]

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a : α
⊢ ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t

Tactic:
rintro ⟨l₁⟩ ⟨l₂⟩; simp

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p (a ::ₘ s) (b ::ₘ t)

Tactic:
apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
    exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
H : l.Nodup
i : Fin l.length
⊢ idxOf (l.get i) l = ↑i

Tactic:
by
  simp [H]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].dedup = [] ↔ [] = []

Tactic:
exact Iff.rfl

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs.dedup)

Tactic:
dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h,

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ f x :: (map f xs).dedup = map f (x :: xs.dedup)
Module: Mathlib.Data.List.Dedup

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

Tactic:
hy

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (replicate (n + 2) x).dedup = [x]

Tactic:
by
    rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
      replicate_dedup n.succ_ne_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ t
h₂ : s ≤ u
⊢ s ≤ t ∩ u

Tactic:
by
  revert s u; refine @(Multiset.induction_on t ?_ fun a t IH => ?_) <;> intro s u h₁ h₂
  · simpa only [zero_inter] using h₁
  by_cases h : a ∈ u
  · rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
    exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)
  · rw [cons_inter_of_neg _ h]
    exact IH ((le_cons_of_notMem <| mt (mem_of_le h₂) h).1 h₁) h₂

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t

Tactic:
by
  simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t

Tactic:
refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩
    simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
ndinsert_of_notMem h

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : a ::ₘ s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t

Tactic:
simp [ndinter, mem_filter]

Goal state after: