mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:

Tactic:
s.nu d = ∏ p ∈ d.primeFactors, s.nu p := (prod_primeFactors_nu hdP).symm
    _ < ∏ p ∈ d.primeFactors, 1 := by
      apply prod_lt_prod_of_nonempty
      · intro p hp
        simp only [mem_primeFactors] at hp
        apply s.nu_pos_of_prime p hp.1 (hp.2.1.trans hdP)
      · intro p hpd; rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
        apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)
      · simp only [nonempty_primeFactors, show 1 < d by lia]
    _ = 1 := by
      simp

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case left
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
hnπ : q % π ∉ {p | v ↑p < 1 ∧ p ≠ 0}
this : v ↑(q % π) ≤ 1
⊢ v ↑(q % π) = 1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ ↑(f 0) ^ 2 + ↑(f 1) ^ 2 + ↑(f 2) ^ 2 + ↑(f 3) ^ 2 = ↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0
x : ℤ
hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x
⊢ ↑(f (σ 2) ^ 2 + f (σ 3) ^ 2) = 0

Tactic:
simpa only [Int.cast_pow, Int.cast_add, ZMod.pow_card] using! hσ.2

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this : Fact (Prime p)
a b c d : ℤ
k : ℕ
⊢ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: ⊢ { re := 0, im := 0 } = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case prime_mul
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Tactic:
obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)

Goal state after:
case prime_mul
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
x y : ℕ
hxy : n = x ^ 2 + y ^ 2
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (n + -1 * x ^ 2)
⊢ IsCoprime x n

Tactic:
exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn₀ : n > 0
x✝ : ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
q : ℕ
hq : q ∈ n.primeFactors
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
this : Fact (Prime q)
⊢ q ∣ b → q ∈ b.primeFactors

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
⊢ x ∈ span {a} ⊔ P ^ (i + 1)

Tactic:
← Submodule.span_singleton_le_iff_mem,

Goal state after:
case mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : S ∙ a ≤ P ^ i
a_notMem : ¬S ∙ a ≤ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
⊢ x ∈ span {a} ⊔ P ^ (i + 1)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case calc_1
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
P : ↥(factors (map f p)).toFinset
x✝ : P ∈ (factors (map f p)).toFinset.attach
⊢ e ↑P * p.inertiaDeg' ↑P = finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)

Tactic:
rw [Factors.finrank_pow_ramificationIdx]

Goal state after:
Module: Mathlib.Order.Category.OmegaCompletePartialOrder

Goal state before:
pp: J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
j : J
⊢ (ConcreteCategory.hom m) t j = (ConcreteCategory.hom (m ≫ (product f).π.app { as := j })) t

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Category.OmegaCompletePartialOrder

Goal state before:
pp: X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
x✝ : s.pt.carrier
⊢ (ConcreteCategory.hom
        ({ toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, monotone' := ⋯, map_ωSup' := ⋯ } ≫ (equalizer f g).ι))
      x✝ =
    (ConcreteCategory.hom s.ι) x✝

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
⊢ ∀ b ∈ Set.range fun e ↦ ↑e i, e i ≤ b

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
⊢ IsLUB s (sSup s)

Tactic:
by
  refine ⟨fun e he ↦ ?_, fun e h ↦ ?_⟩
  · by_contra! hs
    obtain ⟨a, ha⟩ := hs
    exact ha.2.not_ge (le_sSup_apply he fun j hj ↦ (ha.1 j hj).symm)
  · by_contra! hs
    obtain ⟨a, ha⟩ := hs
    refine ha.2.not_ge <| sSup_apply_le fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_
    simp_all

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
⊢ ⊥ ∈ L

Tactic:
by simpa using! L.sSupClosed' <| empty_subset _

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
lowerPolar_intent✝¹ : lowerPolar r (upperPolar r s₁) = s₁
lowerPolar_intent✝ :
  lowerPolar r
      (upperPolar r
        { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯,
            lowerPolar_intent := lowerPolar_intent✝¹ }.extent) =
    { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝¹ }.extent
⊢ { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝¹ } =
    {
      extent :=
        { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯,
            lowerPolar_intent := lowerPolar_intent✝¹ }.extent,
      intent :=
        upperPolar r
          { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯,
              lowerPolar_intent := lowerPolar_intent✝¹ }.extent,
      upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t₁ : Set β
upperPolar_extent✝¹ : upperPolar r (lowerPolar r t₁) = t₁
upperPolar_extent✝ :
  upperPolar r
      (lowerPolar r
        { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹,
            lowerPolar_intent := ⋯ }.intent) =
    { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹, lowerPolar_intent := ⋯ }.intent
⊢ { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹, lowerPolar_intent := ⋯ } =
    {
      extent :=
        lowerPolar r
          { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹,
              lowerPolar_intent := ⋯ }.intent,
      intent :=
        { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹,
            lowerPolar_intent := ⋯ }.intent,
      upperPolar_extent := upperPolar_extent✝, lowerPolar_intent := ⋯ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝² : CompleteLattice α
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hs : CountableSupClosed s
A : ι → α
hA : ∀ (n : ι), A n ∈ s
i₀ : ι := ⋯.some
⊢ {x | ∃ y, A y = x} ⊆ s

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : ∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨆ n, A n ∈ s
x : α
f : ℕ → α
hAs : range f ⊆ s
hA_ne : (range f).Nonempty
hAc : (range f).Countable
hx : IsLUB (range f) x
⊢ ∀ (n : ℕ), f n ∈ s

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : SemilatticeSup α
hs : CountableSupClosed s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ {a, b} ⊆ s

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ x ∈ c.left, x ≤ a) ↔ c ≤ principal a

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ x ∈ c.right, a ≤ x) ↔ c.intent ⊆ (principal a).intent

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
x : α
y : β
hxy : IsLUB (Prod.fst '' A) (x, y).1 ∧ IsLUB (Prod.snd '' A) (x, y).2
⊢ Prod.fst '' A ⊆ s

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
x : α
y : β
hxy : IsLUB (Prod.fst '' A) (x, y).1 ∧ IsLUB (Prod.snd '' A) (x, y).2
⊢ Prod.snd '' A ⊆ t

Tactic:
grind

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: α : Type u
a : α
r : α → α → Prop
h : Acc r a
⊢ ⋯.rank = ⨆ b, Order.succ ⋯.rank

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
x : α
hxs : x ∈ s
⊢ x ∈ s

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
B : ⦃a : α⦄ → a ∈ A → Set α
hB : ∀ ⦃a : α⦄ (a_1 : a ∈ A), B a_1 ⊆ s
hB_ne : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Nonempty
hBc : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Countable
hB_lub : ∀ ⦃a : α⦄ (a_1 : a ∈ A), IsLUB (B a_1) a
⊢ ∀ (i : α) (i_1 : i ∈ A), B ⋯ ⊆ s

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a✝ b : α
inst✝ : Preorder α
s A : Set α
hAc : A.Countable
x : α
hx : IsLUB A x
B : ⦃a : α⦄ → a ∈ A → Set α
hB : ∀ ⦃a : α⦄ (a_1 : a ∈ A), B a_1 ⊆ s
hB_ne : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Nonempty
hBc : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Countable
hB_lub : ∀ ⦃a : α⦄ (a_1 : a ∈ A), IsLUB (B a_1) a
a : α
ha : a ∈ A
⊢ ∃ i, ∃ (i_1 : i ∈ A), (B ⋯).Nonempty

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
this : CountableSupClosed (⋂₀ {t | s ⊆ t ∧ CountableSupClosed t})
⊢ s ⊆ ⋂₀ {t | s ⊆ t ∧ CountableSupClosed t}

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
this : CountableSupClosed (⋂₀ {t | s ⊆ t ∧ CountableSupClosed t})
⊢ CountableSupClosed (⋂₀ {t | s ⊆ t ∧ CountableSupClosed t})

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
a : α
inst✝ : Preorder α
⊢ a ∈ countableSupClosure s ↔ ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
u : Set α
hu : u ⊆ s
hu_ne : u.Nonempty
hu_c : u.Countable
hu_lub : IsLUB u a
v : Set β
hv : v ⊆ t
hv_ne : v.Nonempty
hv_c : v.Countable
hv_lub : IsLUB v b
⊢ u ×ˢ v ⊆ s ×ˢ t

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mp.univ
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ Set.univ

Tactic:
exact ⟨∅, ⟨empty_subset g, mk_eq_zero (∅ : Set <| Set α) ▸ IsRegular.nat_lt hreg 0, by simp⟩⟩

Goal state after:
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ sᶜ ∪ f ⁻¹' t ∈ l ↔ {x | x ∉ s ∨ x ∈ f ⁻¹' t} ∈ l

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : ↑n ≤ (⇑e '' s).chainHeight r'
a : Set β
ha₁ : a ⊆ ⇑e '' s
ha₂ : a.encard = ↑n
ha₃ : IsChain r' a
⊢ a ⊆ range ⇑e

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : ↑n ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain r a
⊢ ⇑e '' a ⊆ ⇑e '' s

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (1, 1).1 ≤ (1, 1).2

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (1, 2).1 ≤ (1, 2).2

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (1, 3).1 ≤ (1, 3).2

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (2, 2).1 ≤ (2, 2).2

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (2, 3).1 ≤ (2, 3).2

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (3, 3).1 ≤ (3, 3).2

Tactic:
grind

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
⊢ ∀ (a b : αs), (∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd) → (∃ (h : b.fst ≤ a.fst), π h a.snd = b.snd) → a = b

Tactic:
grind

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual (R.rightDual (R.leftDual J)) ⊆ R.leftDual J

pp: case a
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual J ⊆ R.leftDual (R.rightDual (R.leftDual J))

Tactic:
· apply R.gc_leftDual_rightDual.monotone_l; exact R.gc_leftDual_rightDual.le_u_l J

Goal state after:
case a
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual J ⊆ R.leftDual (R.rightDual (R.leftDual J))
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
⊢ ⨆ x ∈ P, x = ⨆ a ∈ ↑P, a

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ f a b

pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ f x b

Tactic:
· -- f a y ≤ f a b
      rw [← h]
      apply le_iSup₂ y hy

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ f x b
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
x✝ : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
p : α
hp : p ∈ P
q : α
hq : q ∈ Q
ha : a = p ⊓ q
⊢ a ≤ (p, q).1 ⊓ (p, q).2

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hxt : x ∈ t
⊢ t = P.partOf x

Tactic:
by
  ext y
  exact ⟨(⟨t, ht, hxt, ·⟩), fun ⟨s, hsP, hxs, hys⟩ ↦ (P.eq_of_mem_of_mem ht hsP hxt hxs) ▸ hys⟩

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

Goal state before:
pp: case refine_2.inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
h : a ≠ a → P.Rel a a
⊢ f a = f a

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h1 : ∀ (x : α), f a = f x ↔ a = x
⊢ f a = f b → (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel a b

Tactic:
grind

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

Goal state before:
pp: case inr
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h2 : ∀ (x : α), f a = f x ↔ P.Rel a x
⊢ f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel a b

Tactic:
grind

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

Goal state before:
pp: case inr
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun f
hg : P.IsRepFun g
x : α
hx : x ∉ u
⊢ f (g x) = f x

Tactic:
hg.apply_of_notMem hx,

Goal state after:
case inr
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun f
hg : P.IsRepFun g
x : α
hx : x ∉ u
⊢ f x = f x
Module: Mathlib.Order.Std

Goal state before:
pp: case isTrue.isFalse
α : Type u_1
args : OfStdArgs α
this✝⁵ : LE α := args.le
this✝⁴ : LT α := args.lt
this✝³ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝² :
  let this := args.le;
  Std.IsLinearOrder α
this✝¹ : DecidableLE α := args.decidableLE
this✝ : Std.LawfulOrderLeftLeaningMin α
this : Std.LawfulOrderLeftLeaningMax α
a b : α
h✝¹ : b ≤ a
h✝ : ¬a ≤ b
⊢ a = a

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : ↑t
ha : ↑a ∈ u
h : ∃ b, P.Rel ↑a ↑b
⊢ f₀ h.choose = f₀ a

Tactic:
exact h_eq _ _ h.choose_spec |>.symm

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

Goal state before:
pp: α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
⊢ ∃ f, P.IsRepFun f ∧ ∀ (x : ↑t), f ↑x = f₀ x

Tactic:
classical
  set f : α → α := fun a ↦ if ha : a ∈ u then
    (if hb : ∃ b : t, P.Rel a b then f₀ hb.choose else P.rep (P.partOf_mem ha)) else a with hfdef
  refine ⟨f, ⟨fun a ha ↦ by simp [hfdef, ha], fun a ha ↦ ?_, fun a b hab ↦ ?_⟩, fun a ↦ ?_⟩
  · simp only [hfdef, ha, ↓reduceDIte]
    split_ifs with h
    · exact h.choose_spec.trans <| h_mem h.choose h.choose_spec.right_mem
    push Not at h
    exact P.rep_rel (P.partOf_mem ha) (P.mem_partOf ha)
  · simp_rw [hfdef, dif_pos hab.left_mem, dif_pos hab.right_mem]
    split_ifs with h₁ h₂ h₂
    · exact h_eq _ _ <| (hab.symm.trans h₁.choose_spec).symm.trans h₂.choose_spec
    · exact h₂ ⟨_, hab.symm.trans h₁.choose_spec⟩ |>.elim
    · exact h₁ ⟨_, hab.trans h₂.choose_spec⟩ |>.elim
    congr 1
    rwa [← rel_iff_partOf_eq_partOf_of_mem _ hab.left_mem hab.right_mem]
  obtain (ha | ha) := em (a.1 ∈ u) |>.symm
  · simp [hfdef, ha, h_notMem _ ha]
  simp only [hfdef, ha, ↓reduceDIte]
  split_ifs with h
  · exact h_eq _ _ h.choose_spec |>.symm
  exact h ⟨a, rel_rfl_iff.mpr ha⟩ |>.elim

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: δ : Sort v
f : (α : Type u_1) → [LinearOrder α] → δ
c : ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_1) [inst_1 : LinearOrder β], type α = type β → f α = f β
γ : Type u_1
inst✝ : LinearOrder γ
⊢ (type γ).liftOn f c = f γ

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α : Type u
β : Type v
δ : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : (α : Type u) → [LinearOrder α] → (β : Type v) → [LinearOrder β] → δ
c :
  ∀ (α₁ : Type u) [inst : LinearOrder α₁] (β₁ : Type v) [inst_1 : LinearOrder β₁] (α₂ : Type u)
    [inst_2 : LinearOrder α₂] (β₂ : Type v) [inst_3 : LinearOrder β₂],
    type α₁ = type α₂ → type β₁ = type β₂ → f α₁ β₁ = f α₂ β₂
⊢ (type α).liftOn₂ (type β) f c = f α β

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ 0 = type PEmpty.{?u.36 + 1}

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ 0 = type PEmpty.{?u.42 + 1}

Tactic:
rfl

Goal state after: