mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

Tactic:
have h_uniq (x) : ∃! i, x ∈ E i := by
    refine match mem_iUnion.mp (hEuniv <| mem_univ x) with
      | ⟨i, hi⟩ => ⟨i, hi, fun j hj ↦ hEdis.eq ?_⟩
    simpa [← Clopens.coe_disjoint, not_disjoint_iff] using! ⟨x, hj, hi⟩

Goal state after:
X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
h_uniq : ∀ (x : X), ∃! i, x ∈ E i
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace V
inst✝³ : TotallyDisconnectedSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
S : Set (V × V)
f : C(X, V)
inst✝ : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ∃ n U v, ∀ (x : X), (f x, ∏ n, (↑(U n)).mulIndicator (fun x ↦ v n) x) ∈ S

Tactic:
by
  obtain ⟨n, g, h, hg, hgh⟩ := exists_finite_approximation_of_mem_nhds_diagonal f hS
  refine ⟨n, fun i ↦ ⟨_, (isClopen_discrete {i}).preimage hg⟩, h, fun x ↦ ?_⟩
  convert! hgh x
  exact (Fintype.prod_eq_single _ fun i hi ↦ mulIndicator_of_notMem hi.symm _).trans
    (mulIndicator_of_mem rfl _)

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : d < 0
⊢ 0 < 1 + d * a.y ^ 2 + d * b.y ^ 2

Tactic:
· rw [(eq_zero_of_d_neg h a).resolve_left ha.ne', (eq_zero_of_d_neg h b).resolve_left hb.ne']
    simp

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 1 < (mk |x| |y| ⋯).x

Tactic:
x_mk,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 1 < |x|
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
hy : 0 < a.y
hx₁ : 1 < a.x
hyy : 0 ≤ (a * a₁⁻¹).y
x' : ℕ
hx' : ↑x' = (a * a₁⁻¹).x
hxx₁ : 0 < ↑x'
hxx₂ : ↑x' < a.x
n : ℕ
hn : a * a₁⁻¹ = a₁ ^ n
⊢ a = a₁ ^ (n + 1)

Tactic:
by rw [pow_succ', ← hn, mul_comm a, ← mul_assoc, mul_inv_cancel, one_mul]

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

Goal state before:
pp: case refine_1
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : v ↑πᵥ < 1 ∧ πᵥ ≠ 0
⊢ ¬∃ r, r ≠ 0 ∧ Polynomial.C r = πᵥ

Tactic:
intro ⟨a, ha0, ha⟩

Goal state after:
case refine_1
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : v ↑πᵥ < 1 ∧ πᵥ ≠ 0
a : K
ha0 : a ≠ 0
ha : Polynomial.C a = πᵥ
⊢ False
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ (2 * ((x - y) / 2)) ^ 2 + (2 * ((x + y) / 2)) ^ 2 = 2 * 2 * (((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2)

Tactic:
by nlinarith

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ k < m

Tactic:
by nlinarith

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

Goal state before:
pp: R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb' : LinearIndependent S (⇑f' ∘ b)
⊢ LinearIndependent K (⇑F ∘ b)

Tactic:
by
  contrapose hb' with hb
  -- Informally, if we have a nontrivial linear dependence with coefficients `g` in `K`,
  -- then we can find a linear dependence with coefficients `I.Quotient.mk g'` in `R/I`,
  -- where `I = ker (algebraMap R S)`.
  -- We make use of the same principle but stay in `R` everywhere.
  simp only [linearIndependent_iff', not_forall] at hb ⊢
  obtain ⟨s, g, eq, j', hj's, hj'g⟩ := hb
  use s
  obtain ⟨a, hag, j, hjs, hgI⟩ := Ideal.exist_integer_multiples_notMem hRS s g hj's hj'g
  choose g'' hg'' using hag
  let := Classical.propDecidable
  let g' i := if h : i ∈ s then g'' i h else 0
  have hg' : ∀ i ∈ s, algebraMap _ _ (g' i) = a * g i := by
    intro i hi; exact (congr_arg _ (dif_pos hi)).trans (hg'' i hi)
  -- Because `R/I` is nontrivial, we can lift `g` to a nontrivial linear dependence in `S`.
  have hgI : algebraMap R S (g' j) ≠ 0 := by
    simp only [FractionalIdeal.mem_coeIdeal, not_exists, not_and'] at hgI
    exact hgI _ (hg' j hjs)
  refine ⟨fun i => algebraMap R S (g' i), ?_, j, hjs, hgI⟩
  have eq : F (∑ i ∈ s, g' i • b i) = 0 := by
    rw [map_sum, ← smul_zero a, ← eq, Finset.smul_sum]
    refine Finset.sum_congr rfl ?_
    intro i hi
    rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_apply]
  simp only [IsScalarTower.algebraMap_smul, ← map_smul, ← map_sum,
    (F.map_eq_zero_iff hf).mp eq, map_zero, (· ∘ ·)]

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

Goal state before:
pp: case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b : (Submodule.mkQ (map f p)) x ∈ Submodule.span R (⇑(↑R (Submodule.mkQ (map f p))) '' Set.range b')
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map f p)

Tactic:
← Submodule.map_span

Goal state after:
case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b :
  (Submodule.mkQ (map f p)) x ∈ Submodule.map (↑R (Submodule.mkQ (map f p))) (Submodule.span R (Set.range b'))
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map f p)
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ ↑((norm a).natAbs * (norm b).natAbs) = ↑p * ↑p

Tactic:
← @norm_natCast (-1),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ ↑((norm a).natAbs * (norm b).natAbs) = (↑p).norm
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℂ[X]
s : ℂ
⊢ P f s = -(cexp s * ((cexp s)⁻¹ * eval s (sumIDeriv f))) + cexp s * eval 0 (sumIDeriv f)

Tactic:
mul_inv_cancel_left₀ (exp_ne_zero s),

Goal state after:
f : ℂ[X]
s : ℂ
⊢ P f s = -eval s (sumIDeriv f) + cexp s * eval 0 (sumIDeriv f)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) X ^ (p - 1) * eval (x • s) (map (algebraMap ℤ ℂ) f) ^ p‖ ≤ |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ^ p

Tactic:
eval_X,

Goal state after:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ ‖(x • s) ^ (p - 1) * eval (x • s) (map (algebraMap ℤ ℂ) f) ^ p‖ ≤ |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : (aeval x) f = 0
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0

Tactic:
← eval_map_algebraMap

Goal state after:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: 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 ≠ ⊥
⊢ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx' P * p.inertiaDeg' P = finrank K L

Tactic:
set e := ramificationIdx' p (S := S)
  calc
    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * inertiaDeg' p P =
        ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach,
          finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ e P) := ?_
    _ = finrank (R ⧸ p)
          (∀ P : (factors (map (algebraMap R S) p)).toFinset, S ⧸ (P : Ideal S) ^ e P) :=
      (finrank_pi_fintype (R ⧸ p)).symm
    _ = finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) := ?_
    _ = finrank K L := ?_
  · rw [← Finset.sum_attach]
    refine Finset.sum_congr rfl fun P _ => ?_
    rw [Factors.finrank_pow_ramificationIdx]
  · refine LinearEquiv.finrank_eq (Factors.piQuotientLinearEquiv S p ?_).symm
    rwa [Ne, Ideal.map_eq_bot_iff_le_ker, (RingHom.injective_iff_ker_eq_bot _).mp <|
      algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff]
  · exact finrank_quotient_map p K L

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
hx : Liouville x
p : ℝ
⊢ ∀ (x_1 : ℕ),
    (1 < x_1 ∧ ∃ a, x ≠ ↑a / ↑x_1 ∧ |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ ⌈p⌉₊) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < 1 / ↑x_1 ^ ↑⌈p⌉₊

Tactic:
rintro b ⟨_hb, a, hne, hlt⟩

Goal state after:
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ ∃ m, x ≠ ↑m / ↑b ∧ |x - ↑m / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊
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
⊢ m = { toFun := fun t j ↦ (ConcreteCategory.hom (s.π.app { as := j })) t, monotone' := ⋯, map_ωSup' := ⋯ }

Tactic:
ext t

Goal state after:
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
⊢ (ConcreteCategory.hom m) t =
    (ConcreteCategory.hom
        { toFun := fun t j ↦ (ConcreteCategory.hom (s.π.app { as := j })) t, monotone' := ⋯, map_ωSup' := ⋯ })
      t
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' x y
hx : x ∈ c'.intent
⊢ y ∈ upperPolar r' c'.extent

Tactic:
exact fun z hz ↦ _root_.trans (rel_extent_intent hz hx) hy

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
⊢ (rcomap r (rcomap s l)).sets = (rcomap (r.comp s) l).sets

Tactic:
ext t

Goal state after:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ t ∈ (rcomap r (rcomap s l)).sets ↔ t ∈ (rcomap (r.comp s) l).sets
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂

Tactic:
rw [rtendsto_def]

Goal state after:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
⊢ pmap (PFun.res f s) l = map f (l ⊓ 𝓟 s)

Tactic:
ext t

Goal state after:
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
⊢ s.chainHeight r ≤ t.chainHeight r

Tactic:
refine forall_natCast_le_iff_le.mp fun n hn ↦ ?_

Goal state after:
α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
n : ℕ
hn : ↑n ≤ s.chainHeight r
⊢ ↑n ≤ t.chainHeight r
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ y ⊓ z ≤ y ⊔ z

Tactic:
by simpa [inf_assoc] using inf_le_of_right_le inf_le_sup

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n m : Nucleus X
x y : X
f g : Nucleus X
h : (fun x ↦ x.toFun) f = (fun x ↦ x.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f; congr!

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
ha : a ∈ u
hab : f a = f b
⊢ P.Rel (f a) b

Tactic:
rw [hab, P.rel_comm]

Goal state after:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
ha : a ∈ u
hab : f a = f b
⊢ P.Rel b (f b)
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_1
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
a : α
ha : a ∈ u
b : α
⊢ f a = f b ↔ P.Rel a b

Tactic:
hf.apply_eq_apply_iff_rel ha

Goal state after:
case refine_1
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
a : α
ha : a ∈ u
b : α
⊢ P.Rel a b ↔ P.Rel a b
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
ha : a ∈ u
⊢ f a = f (f a)

Tactic:
hf.apply_eq_apply_iff_rel ha

Goal state after:
case inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
ha : a ∈ u
⊢ P.Rel a (f a)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ ∀ t ∈ {s | ∃ A, MeasurableSet A ∧ s = {⊥} ×ˢ A} ∪ {s | ∃ i A, MeasurableSet A ∧ s = Set.Ioi i ×ˢ A}, MeasurableSet t

Tactic:
rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ({⊥} ×ˢ A)

case inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
⊢ ∀ t ∈ {s | ∃ A, MeasurableSet A ∧ s = {⊥} ×ˢ A} ∪ {s | ∃ i A, MeasurableSet A ∧ s = Set.Ioi i ×ˢ A}, MeasurableSet t

Tactic:
rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)

Goal state after:
case inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ({⊥} ×ˢ A)

case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
i : ι
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ Measurable fun x ↦ (↑x.1, x.2)

Tactic:
rw [measurable_iff_comap_le]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ MeasurableSpace.comap (fun x ↦ (↑x.1, x.2)) 𝓕.predictable ≤ Subtype.instMeasurableSpace.prod (↑𝓕 i)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
hji : j ≤ i
⊢ MeasurableSet ((fun x ↦ (↑x.1, x.2)) ⁻¹' Set.Ioi j ×ˢ A)

Tactic:
(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A
        = (Subtype.val ⁻¹' (Set.Ioc j i)) ×ˢ A)

Goal state after:
case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
hji : j ≤ i
⊢ MeasurableSet ((Subtype.val ⁻¹' Set.Ioc j i) ×ˢ A)
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
⊢ hittingBtwn u s n m ω ≤ m

Tactic:
simp only [hittingBtwn]

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) ≤ m
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
h : τ a ≤ ↑i ∧ ∀ (x : Ω), τ x < ↑i → ¬τ a ≤ τ x
⊢ τ a = ↑i

Tactic:
exact h.1.eq_or_lt.resolve_right fun h_lt => h.2 a h_lt le_rfl

Goal state after:
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
hmn : m ≤ n
h : m < n
⊢ hittingBtwn u s n m ω = m

Tactic:
· exact hittingBtwn_of_lt h

Goal state after:
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
⊢ n ≤ hittingBtwn u s n m ω

Tactic:
simp only [hittingBtwn]

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
⊢ n ≤ if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ upperCrossingTime a b f N N ω = N

Tactic:
by_cases hN' : N < Nat.find (exists_upperCrossingTime_eq f N ω hab)
  · refine le_antisymm upperCrossingTime_le ?_
    have hmono : StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
        (Set.Iic (Nat.find (exists_upperCrossingTime_eq f N ω hab)).pred) := by
      refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_
      rw [Nat.lt_pred_iff] at hm
      convert! Nat.find_min _ hm
    convert! StrictMonoOn.Iic_id_le hmono N (Nat.le_sub_one_of_lt hN')
  · rw [not_lt] at hN'
    exact upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i') i'
hi'_eq_i : i' = i
⊢ MeasurableSet {ω | τ ω < ↑i'}

Tactic:
exact hτ.measurableSet_lt_of_isLUB i' hi'_lub

Goal state after:
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : N = 0
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
subst hN
    rw [upcrossingsBefore_zero]

Goal state after: