mathlib-initiative/mathlib-tactics huggingface dataset:
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''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker f)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : f (g' j) ≠ 0
i : ι
hi : i ∈ s
⊢ F (g' i • b i) = a • g i • (⇑F ∘ b) i

Tactic:
map_smul,

Goal state after:
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''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker f)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : f (g' j) ≠ 0
i : ι
hi : i ∈ s
⊢ g' i • F (b i) = a • g i • (⇑F ∘ b) i
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
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'))
y : S
y_mem : y ∈ Submodule.span R (Set.range b')
y_eq : (↑R (Submodule.mkQ (map f p))) y = (Submodule.mkQ (map f p)) x
this : y + -(y - x) ∈ ?m.426
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map f p)

Tactic:
by simpa

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
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
inst✝¹ : IsLocalRing S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
⊢ p.ramificationIdx' (IsLocalRing.maximalIdeal S) * p.inertiaDeg' (IsLocalRing.maximalIdeal S) = finrank K L

Tactic:
have := FaithfulSMul.of_field_isFractionRing R S K L

Goal state after:
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
inst✝¹ : IsLocalRing S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
this : FaithfulSMul R S
⊢ p.ramificationIdx' (IsLocalRing.maximalIdeal S) * p.inertiaDeg' (IsLocalRing.maximalIdeal S) = finrank K L
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (↑a).val ∈ Ico 1 (p - 1).succ

Tactic:
mem_Ico,

Goal state after:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (↑a).val ∧ (↑a).val < (p - 1).succ
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ∈ Ico 1 (p - 1).succ
⊢ ∃ a, ∃ (_ : a ∈ univ), (↑a).val = b

Tactic:
mem_Ico,

Goal state after:
case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : 1 ≤ b ∧ b < (p - 1).succ
⊢ ∃ a, ∃ (_ : a ∈ univ), (↑a).val = b
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 ↦ x1 < x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 ↦ x1 < x2) s

Tactic:
by
  rw [← bounded_le_iff_bounded_lt, ← bounded_le_iff_bounded_lt]
  exact bounded_le_inter_lt a

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

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑m / ↑n + ↑r

Tactic:
by simpa

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
b : A
hb : b ∈ {b | orderOf b = n}
⊢ orderOf (a⁻¹ * b)⁻¹ = n

Tactic:
mul_inv_rev,

Goal state after:
case refine_1
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
b : A
hb : b ∈ {b | orderOf b = n}
⊢ orderOf (b⁻¹ * a⁻¹⁻¹) = n
Module: Mathlib.Order.CompleteLattice.SetLike

Goal state before:
pp: X : Type u_1
L : Sublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
by simp [← mem_subtype]

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

Goal state before:
pp: X : Type u_1
L : Sublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Tactic:
by simp [← mem_subtype]

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

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
by simp [← mem_subtype]

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

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
𝒮 : Set ↥L
x : X
⊢ x ∈ sInf 𝒮 ↔ ∀ T ∈ 𝒮, x ∈ T

Tactic:
by simp [← mem_subtype]

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

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
I : Sort u_2
f : I → ↥L
x : X
⊢ x ∈ ⨅ i, f i ↔ ∀ (i : I), x ∈ f i

Tactic:
by simp [← mem_subtype]

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

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
x : X
⊢ x ∈ ⊤

Tactic:
by simp [← mem_subtype]

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

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Tactic:
by simp [← mem_subtype]

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

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
𝒮 : Set ↥L
x : X
⊢ x ∈ sSup 𝒮 ↔ ∃ T ∈ 𝒮, x ∈ T

Tactic:
by simp [← mem_subtype]

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

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
I : Sort u_2
f : I → ↥L
x : X
⊢ x ∈ ⨆ i, f i ↔ ∃ i, x ∈ f i

Tactic:
by simp [← mem_subtype]

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

Goal state before:
pp: X : Type u_1
L : CompleteSublattice (Set X)
x : X
⊢ x ∉ ⊥

Tactic:
by simp [← mem_subtype]

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
c : Concept α β r
h : c.extent ⊆ s
⊢ c ≤ ofObjects r s

Tactic:
simpa using! (lowerPolar_anti r).comp (upperPolar_anti r) h

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
a b : DedekindCut α
h : a < b
c : α
hac : a < principal c
hcb : principal c ≤ b
d : α
had : a ≤ principal d
hdc : d < c
u : α
left✝ : d < u
right✝ : u < c
⊢ principal d < principal u

Tactic:
by simpa

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
a b : DedekindCut α
h : a < b
c : α
hac : a < principal c
hcb : principal c ≤ b
d : α
had : a ≤ principal d
hdc : d < c
u : α
left✝ : d < u
right✝ : u < c
⊢ principal u < principal c

Tactic:
by simpa

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
a b : DedekindCut α
h : a < b
c : α
hac : a < principal c
hcb : principal c ≤ b
d : α
had : a ≤ principal d
hdc : d < c
u : α
left✝ : d < u
right✝ : u < c
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨principal u, had.trans_lt (by simpa), hcb.trans_lt' (by simpa)⟩

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).Nonempty

Tactic:
by simpa

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).Nonempty

Tactic:
by simpa

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

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
biInter_eq_iInter

Goal state after:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
⊢ Filter α

Tactic:
refine .ofCardinalInter {s | sᶜ ∈ l} hc (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
  · rw [mem_ofPred_eq, compl_sInter]
    apply hUnion (compl '' S) (lt_of_le_of_lt mk_image_le hSc)
    intro s hs
    rw [mem_image] at hs
    rcases hs with ⟨t, ht, rfl⟩
    apply hSp ht
  · rw [mem_ofPred_eq]
    rw [← compl_subset_compl] at hsub
    exact hmono sᶜ ht tᶜ hsub

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅
p : Nat.Primes
hE₂ : E =ᵐ[μ] C ↑p
h_qmp : Measure.QuasiMeasurePreserving (fun x ↦ -u p +ᵥ x) μ μ
⊢ u p +ᵥ C ↑p =ᵐ[μ] C ↑p

Tactic:
rw [hC]

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), #↑(T s a) < c
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ g

Tactic:
by simpa

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : ↑n ≤ s.chainHeight r
h' : ¬n = 0
⊢ ∃ t ⊆ s, IsChain r t ∧ ↑n ≤ t.encard

Tactic:
by
      contrapose! h
      refine iSup_lt_iff.mpr ⟨n - 1, ?_, fun m ↦ ENat.le_sub_one_of_lt <| h m.1 m.2.1 m.2.2⟩
      exact_mod_cast Nat.sub_one_lt h'

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
s : Set X
⊢ rangeFactorization (⇑n) (sSup s) = sSup (rangeFactorization ⇑n '' s)

Tactic:
n.giAux.gc.l_sSup,

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
s : Set X
⊢ ⨆ a ∈ s, rangeFactorization (⇑n) a = sSup (rangeFactorization ⇑n '' s)
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
x✝³ : Set α
x✝² : (Set β)ᵒᵈ
h : (⇑toDual ∘ R.leftDual) x✝³ ≤ x✝²
x✝¹ : α
ha : x✝¹ ∈ x✝³
x✝ : β
hb : x✝ ∈ ofDual x✝²
⊢ x✝ ∈ x✝²

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
x✝³ : Set α
x✝² : (Set β)ᵒᵈ
h : x✝³ ⊆ (R.rightDual ∘ ⇑ofDual) x✝²
x✝¹ : β
hb : x✝¹ ∈ x✝²
x✝ : α
ha : x✝ ∈ x✝³
⊢ x✝ ∈ x✝³

Tactic:
by simpa

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

Goal state before:
pp: case refine_1
α : Type u_1
s t x✝ y✝ z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q✝ P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
x' : α
hx' : x' ∈ P
hyx' : y ≤ x'
⊢ x ∈ Q

Tactic:
obtain rfl := P.pairwiseDisjoint.eq_of_le h hx' (P.ne_bot_of_mem h) (hxy.trans hyx')

Goal state after:
case refine_1
α : Type u_1
s t x✝ y✝ z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q✝ P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
hx' : x ∈ P
hyx' : y ≤ x
⊢ x ∈ Q
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
this : sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup ↑P ⊓ sSup ↑Q
⊢ sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = s

Tactic:
by simpa

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
hx : ↑(S.restrictAux x) ≤ x
⊢ Subtype.val '' {s | x ≤ ↑s} ⊆ ↑S

Tactic:
by simp +contextual [Set.subset_def]

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a b : X
s : ↥S
⊢ Sublocale.restrictAux✝ S a ⊓ Sublocale.restrictAux✝ S b ≤ s ↔ Sublocale.restrictAux✝ S (a ⊓ b) ≤ s

Tactic:
calc
      _ ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s := by simp
      _ ↔ S.restrictAux b ≤ a ⇨ s := by rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
      _ ↔ b ≤ a ⇨ s := by
        set c : S := ⟨a ⇨ s, S.himp_mem s.coe_prop⟩
        change Sublocale.restrictAux S b ≤ c.val ↔ b ≤ c
        rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]
      _ ↔ S.restrictAux (a ⊓ b) ≤ s := by simp [inf_comm, S.giAux.gc.le_iff_le]

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
x : X
⊢ n.toSublocale.restrict x = ⟨n x, ⋯⟩

Tactic:
ext
  simpa [Sublocale.restrict, sInf_image, le_antisymm_iff (a := iInf _)] using
    ⟨iInf₂_le_of_le ⟨n x, x, rfl⟩ n.le_apply le_rfl, fun y hxy ↦ by simpa using n.monotone hxy⟩

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
⊢ Set.Iio ↑i = ⋃ j, {k | k ≤ ↑(seq j)}

Tactic:
ext1 k

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
⊢ k ∈ Set.Iio ↑i ↔ k ∈ ⋃ j, {k | k ≤ ↑(seq j)}
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (n + 1) ω)) ω -
      stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N n ω)) ω =
    0

Tactic:
by
  have : N ≤ upperCrossingTime a b f N n ω := by
    rw [upcrossingsBefore] at hn
    rw [← not_lt]
    exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)
  simp [stoppedValue, upperCrossingTime_stabilize' (Nat.le_succ n) this,
    lowerCrossingTime_stabilize' le_rfl (le_trans this upperCrossingTime_le_lowerCrossingTime)]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
hs : ∀ (i : ℕ), MeasurableSet (s i) ∧ ∀ (i_1 : ι), MeasurableSet (s i ∩ {ω | τ ω ≤ ↑i_1})
⊢ MeasurableSet (⋃ i, s i) ∧ ∀ (i : ι), MeasurableSet ((⋃ i, s i) ∩ {ω | τ ω ≤ ↑i})

Tactic:
refine ⟨MeasurableSet.iUnion fun i ↦ (hs i).1, fun i ↦ ?_⟩

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
hs : ∀ (i : ℕ), MeasurableSet (s i) ∧ ∀ (i_1 : ι), MeasurableSet (s i ∩ {ω | τ ω ≤ ↑i_1})
i : ι
⊢ MeasurableSet ((⋃ i, s i) ∩ {ω | τ ω ≤ ↑i})
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ hτ.measurableSpace ⊓ ⋯.measurableSpace = hτ.measurableSpace ⊓ ↑f i

Tactic:
measurableSpace_const

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ hτ.measurableSpace ⊓ ↑f i = hτ.measurableSpace ⊓ ↑f i
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝¹ : LinearOrder ι
inst✝ : Zero β
s : Set Ω
i : ι
⊢ stoppedProcess (fun i ↦ s.indicator (u i)) τ i = s.indicator (stoppedProcess u τ i)

Tactic:
by
  ext ω
  by_cases hω : ω ∈ s <;> simp [stoppedProcess, hω]

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ ∀ (j : ℕ), ⊥ ≤ j → f j ω ∉ Set.Ici ↑i

Tactic:
simp [hib]

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun f μ
hij : i < j
⊢ Disjoint {j} {k | k ≤ i}

Tactic:
by simpa

Goal state after:
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : IsZeroOrProbabilityMeasure 0
⊢ centralMoment X 1 0 = 0

pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ centralMoment X 1 μ = 0

Tactic:
· simp [centralMoment]

Goal state after:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ centralMoment X 1 μ = 0