harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem eq_adjoin_primitive_root {μ : CyclotomicField n K} (h : IsPrimitiveRoot μ n) :
    CyclotomicRing n A K = adjoin A ({μ} : Set (CyclotomicField n K))

Proof state:
n : ℕ+
A : Type u
K : Type w
inst✝² : CommRing A
inst✝¹ : Field K
inst✝ : Algebra A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ ↑n
⊢ CyclotomicRing n A K = ↥(adjoin A {μ})

Tactic:
rw [← IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h,
  IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots h]

Result:
n : ℕ+
A : Type u
K : Type w
inst✝² : CommRing A
inst✝¹ : Field K
inst✝ : Algebra A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ ↑n
⊢ CyclotomicRing n A K = ↥(adjoin A {b | ∃ a ∈ {n}, b ^ ↑a = 1})

Proof state:
n : ℕ+
A : Type u
K : Type w
inst✝² : CommRing A
inst✝¹ : Field K
inst✝ : Algebra A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ ↑n
⊢ CyclotomicRing n A K = ↥(adjoin A {b | ∃ a ∈ {n}, b ^ ↑a = 1})

Tactic:
simp [CyclotomicRing]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem image_snd_divisorsAntidiagonal : (divisorsAntidiagonal n).image Prod.snd = divisors n

Proof state:
n : ℕ
⊢ image (Prod.snd ∘ ⇑(Equiv.prodComm ℕ ℕ).toEmbedding) n.divisorsAntidiagonal = n.divisors

Tactic:
exact image_fst_divisorsAntidiagonal

Result:
no goals

Proof state:
n : ℕ
⊢ image Prod.snd n.divisorsAntidiagonal = n.divisors

Tactic:
rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]

Result:
n : ℕ
⊢ image (Prod.snd ∘ ⇑(Equiv.prodComm ℕ ℕ).toEmbedding) n.divisorsAntidiagonal = n.divisors
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem preimage_smul_ball (c : G) (x : X) (r : ℝ) : (c • ·) ⁻¹' ball x r = ball (c⁻¹ • x) r

Proof state:
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x => c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_ball]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem mul_iff_right [CommGroup β] [IsTopologicalGroup β] (hf : StronglyMeasurable f) :
    StronglyMeasurable (f * g) ↔ StronglyMeasurable g :=
  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv,
    fun h ↦ hf.mul h⟩

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
hf : StronglyMeasurable f
h : StronglyMeasurable (f * g)
⊢ g = f * g * f⁻¹

Tactic:
simp only [mul_inv_cancel_comm]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem le_zero {x : PGame} : x ≤ 0 ↔ ∀ i, ∃ j, (x.moveLeft i).moveRight j ≤ 0

Proof state:
x : PGame
⊢ x ≤ 0 ↔ ∀ (i : x.LeftMoves), ∃ j, (x.moveLeft i).moveRight j ≤ 0

Tactic:
rw [le_def]

Result:
x : PGame
⊢ ((∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ moveLeft 0 i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ 0) ∧
      ∀ (j : RightMoves 0), (∃ i, x ≤ (moveRight 0 j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ moveRight 0 j) ↔
    ∀ (i : x.LeftMoves), ∃ j, (x.moveLeft i).moveRight j ≤ 0

Proof state:
x : PGame
⊢ ((∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ moveLeft 0 i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ 0) ∧
      ∀ (j : RightMoves 0), (∃ i, x ≤ (moveRight 0 j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ moveRight 0 j) ↔
    ∀ (i : x.LeftMoves), ∃ j, (x.moveLeft i).moveRight j ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem memLp_top (f : 𝓢(E, F)) (μ : Measure E

Proof state:
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : autoParam (Measure E) _auto✝
⊢ MemLp ⇑f ⊤ μ

Tactic:
rcases f.decay 0 0 with ⟨C, _, hC⟩

Result:
case intro.intro
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : autoParam (Measure E) _auto✝
C : ℝ
left✝ : 0 < C
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
⊢ MemLp ⇑f ⊤ μ

Proof state:
case intro.intro
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : autoParam (Measure E) _auto✝
C : ℝ
left✝ : 0 < C
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
x : E
⊢ ‖f x‖ ≤ C

Tactic:
simpa using hC x

Result:
no goals

Proof state:
case intro.intro
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : autoParam (Measure E) _auto✝
C : ℝ
left✝ : 0 < C
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
⊢ MemLp ⇑f ⊤ μ

Tactic:
refine memLp_top_of_bound f.continuous.aestronglyMeasurable C (ae_of_all μ fun x ↦ ?_)

Result:
case intro.intro
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : autoParam (Measure E) _auto✝
C : ℝ
left✝ : 0 < C
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
x : E
⊢ ‖f x‖ ≤ C
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem mk_mem_col_iff {μ : YoungDiagram} {i j : ℕ} : (i, j) ∈ μ.col j ↔ (i, j) ∈ μ

Proof state:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ.col j ↔ (i, j) ∈ μ

Tactic:
simp [col]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem constAlterKey_eq_alterKey [BEq α] [LawfulBEq α] {β : Type v} {k : α}
    {f : Option β → Option β} {l : List ((_ : α) × β)} : Const.alterKey k f l = alterKey k f l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ Const.alterKey k f l = alterKey k f l

Tactic:
rw [alterKey, Const.alterKey, getValue?_eq_getValueCast?]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (match f (getValueCast? k l) with
    | none => eraseKey k l
    | some v => insertEntry k v l) =
    match f (getValueCast? k l) with
    | none => eraseKey k l
    | some v => insertEntry k v l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (match f (getValueCast? k l) with
    | none => eraseKey k l
    | some v => insertEntry k v l) =
    match f (getValueCast? k l) with
    | none => eraseKey k l
    | some v => insertEntry k v l

Tactic:
cases f (getValueCast? k l) <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem Lp.norm_const [NeZero μ] (hp_zero : p ≠ 0) :
    ‖Lp.const p μ c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ ‖(Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Tactic:
rw [← MemLp.toLp_const, Lp.norm_toLp, eLpNorm_const] <;> try assumption

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Tactic:
rw [ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
⊢ ‖(Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Tactic:
have := NeZero.ne μ

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ ‖(Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Proof state:
case hμ
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ μ ≠ 0

Tactic:
assumption

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma norm_natCast_cpow_of_pos {n : ℕ} (hn : 0 < n) (s : ℂ) :
    ‖(n : ℂ) ^ s‖ = (n : ℝ) ^ (s.re)

Proof state:
n : ℕ
hn : 0 < n
s : ℂ
⊢ ‖↑n ^ s‖ = ↑n ^ s.re

Tactic:
rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (Nat.cast_pos.mpr hn) _]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
@[simp]
lemma mem_inter : a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t :=
  ⟨fun h => ⟨mem_of_le inter_le_left h, mem_of_le inter_le_right h⟩, fun ⟨h₁, h₂⟩ => by
    rw [← cons_erase h₁, cons_inter_of_pos _ h₂]; apply mem_cons_self⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ s ∩ t

Tactic:
rw [← cons_erase h₁, cons_inter_of_pos _ h₂]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ s.erase a ∩ t.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ s.erase a ∩ t.erase a

Tactic:
apply mem_cons_self

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).getKey! k' =
      if k == k' then
        if k ∈ m then k else default
      else
        m.getKey! k'

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey! k' = if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey! k' = if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'

Tactic:
simp_to_raw using Raw₀.getKey!_modify

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem of_forall_eq_false (α : Sort u) (p : α → Prop) (h : (∀ x : α, p x) = False) : ∃ x : α, ¬ p x

Proof state:
α : Sort u
p : α → Prop
h : (∀ (x : α), p x) = False
⊢ ∃ x, ¬p x

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
lemma exists_eval_ne_zero_of_natDegree_lt_card (f : R[X]) (hf : f ≠ 0) (hfR : f.natDegree < #R) :
    ∃ r, f.eval r ≠ 0

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hfR : ↑f.natDegree < #R
hf : ∀ (r : R), eval r f = 0
⊢ f = 0

Tactic:
exact eq_zero_of_forall_eval_zero_of_natDegree_lt_card f hf hfR

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : f ≠ 0
hfR : ↑f.natDegree < #R
⊢ ∃ r, eval r f ≠ 0

Tactic:
contrapose! hf

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hfR : ↑f.natDegree < #R
hf : ∀ (r : R), eval r f = 0
⊢ f = 0
-- Mathlib/Tactic/NormNum/GCD.lean
theorem nat_gcd_helper_2 (d x y a b : ℕ) (hu : x % d = 0) (hv : y % d = 0)
    (h : x * a = y * b + d) : Nat.gcd x y = d

Proof state:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ (↑x).gcd ↑y = d

Tactic:
apply int_gcd_helper' a (-b)
  (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hu))
  (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hv))

Result:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a + ↑y * -↑b = ↑d

Proof state:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a + ↑y * -↑b = ↑d

Tactic:
rw [mul_neg, ← sub_eq_add_neg, sub_eq_iff_eq_add']

Result:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a = ↑y * ↑b + ↑d

Proof state:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a = ↑y * ↑b + ↑d

Tactic:
exact mod_cast h

Result:
no goals

Proof state:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ x.gcd y = d

Tactic:
rw [← Int.gcd_natCast_natCast]

Result:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ (↑x).gcd ↑y = d
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
lemma limsup_const_sub (F : Filter ι) (f : ι → ℝ≥0∞) {c : ℝ≥0∞} (c_ne_top : c ≠ ∞) :
    Filter.limsup (fun i ↦ c - f i) F = c - Filter.liminf f F

Proof state:
case inr
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
h✝ : F.NeBot
⊢ limsup (fun i => c - f i) F = c - liminf f F

Tactic:
exact (Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ c - x)
(fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c_ne_top).continuousAt).symm

Result:
no goals

Proof state:
case inl
ι : Type u_4
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
⊢ limsup (fun i => c - f i) ⊥ = c - liminf f ⊥

Tactic:
simp only [limsup_bot, bot_eq_zero', liminf_bot, le_top, tsub_eq_zero_of_le]

Result:
no goals

Proof state:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
⊢ limsup (fun i => c - f i) F = c - liminf f F

Tactic:
rcases F.eq_or_neBot with rfl | _

Result:
case inl
ι : Type u_4
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
⊢ limsup (fun i => c - f i) ⊥ = c - liminf f ⊥

case inr
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
h✝ : F.NeBot
⊢ limsup (fun i => c - f i) F = c - liminf f F
-- Mathlib/Order/Interval/Finset/Defs.lean
@[simp] lemma toFinset_Ioc (a b : α) [Fintype (Ioc a b)] : (Ioc a b).toFinset = Finset.Ioc a b

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioc a b)
⊢ (Ioc a b).toFinset = Finset.Ioc a b

Tactic:
ext

Result:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioc a b)
a✝ : α
⊢ a✝ ∈ (Ioc a b).toFinset ↔ a✝ ∈ Finset.Ioc a b

Proof state:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioc a b)
a✝ : α
⊢ a✝ ∈ (Ioc a b).toFinset ↔ a✝ ∈ Finset.Ioc a b

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Compactification/OnePointEquiv.lean
@[simp]
lemma equivProjectivization_apply_infinity :
    equivProjectivization K ∞ = mk K ⟨1, 0⟩ (by simp) :=
  rfl

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
⊢ (1, 0) ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma mul_prod_Ico_eq_prod_Icc (h : a ≤ b) : f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Proof state:
α : Type u_1
M : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid M
f : α → M
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
rw [Icc_eq_cons_Ico h, prod_cons]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem bot_covers (S : Sieve X) (f : Y ⟶ X) : (⊥ : GrothendieckTopology C).Covers S f ↔ S f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ ⊥.Covers S f ↔ S.arrows f

Tactic:
rw [covers_iff, bot_covering, ← Sieve.mem_iff_pullback_eq_top]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[reassoc (attr := simp)]
lemma resLE_map (i : U ≤ U') :
    f.resLE U V e ≫ Y.homOfLE i =
      f.resLE U' V (e.trans ((Opens.map f.base).map i.hom).le)

Proof state:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U ≤ U'
⊢ resLE f U V e ≫ Y.homOfLE i = resLE f U' V ⋯

Tactic:
simp_rw [← resLE_id, resLE_comp_resLE, Category.comp_id]

Result:
no goals
-- Mathlib/Order/InitialSeg.lean
theorem ext [IsIrrefl β s] [IsTrichotomous β s] {f g : r ≺i s} (h : ∀ x, f x = g x) : f = g

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f.toRelEmbedding = g.toRelEmbedding

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
x✝ : α
⊢ f.toRelEmbedding x✝ = g.toRelEmbedding x✝

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f = g

Tactic:
rw [← toRelEmbedding_inj]

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f.toRelEmbedding = g.toRelEmbedding

Proof state:
case h
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl β s
inst✝ : IsTrichotomous β s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
x✝ : α
⊢ f.toRelEmbedding x✝ = g.toRelEmbedding x✝

Tactic:
exact h _

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem unbounded_lt_inter_not_lt [SemilatticeSup α] (a : α) :
    Unbounded (· < ·) (s ∩ { b | ¬b < a }) ↔ Unbounded (· < ·) s

Proof state:
α : Type u_1
s : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Unbounded (fun x1 x2 => x1 < x2) (s ∩ {b | ¬b < a}) ↔ Unbounded (fun x1 x2 => x1 < x2) s

Tactic:
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]

Result:
α : Type u_1
s : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Bounded (fun x1 x2 => x1 < x2) (s ∩ {b | ¬b < a}) ↔ Bounded (fun x1 x2 => x1 < x2) s

Proof state:
α : Type u_1
s : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Bounded (fun x1 x2 => x1 < x2) (s ∩ {b | ¬b < a}) ↔ Bounded (fun x1 x2 => x1 < x2) s

Tactic:
exact bounded_lt_inter_not_lt a

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem setIntegral_eq [SigmaFiniteFiltration μ ℱ] (hf : Martingale f ℱ μ) {i j : ι} (hij : i ≤ j)
    {s : Set Ω} (hs : MeasurableSet[ℱ i] s) : ∫ ω in s, f i ω ∂μ = ∫ ω in s, f j ω ∂μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (x : Ω) in s, (μ[f j|↑ℱ i]) x ∂μ

Tactic:
refine setIntegral_congr_ae (ℱ.le i s hs) ?_

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → f i x = (μ[f j|↑ℱ i]) x

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f j ω ∂μ

Tactic:
rw [← setIntegral_condExp (ℱ.le i) (hf.integrable j) hs]

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (x : Ω) in s, (μ[f j|↑ℱ i]) x ∂μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → f i x = (μ[f j|↑ℱ i]) x

Tactic:
filter_upwards [hf.2 i j hij] with _ heq _ using heq.symm

Result:
no goals
-- Mathlib/Logic/Equiv/List.lean
theorem lower_raise' : ∀ l n, lower' (raise' l n) n = l
  | [], _ => rfl
  | m :: l, n => by simp [raise', lower', Nat.add_sub_cancel_right, lower_raise']

Proof state:
m : ℕ
l : List ℕ
n : ℕ
⊢ lower' (raise' (m :: l) n) n = m :: l

Tactic:
simp [raise', lower', Nat.add_sub_cancel_right, lower_raise']

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem ofFn_take_get {α : Type*} {m : ℕ} (l : List α) (h : m ≤ l.length) :
    List.ofFn (take m h l.get) = l.take m :=
  List.ext_get (by simp [h]) (fun n h1 h2 => by simp)

Proof state:
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
n : ℕ
h1 : n < (List.ofFn (take m h l.get)).length
h2 : n < (List.take m l).length
⊢ (List.ofFn (take m h l.get)).get ⟨n, h1⟩ = (List.take m l).get ⟨n, h2⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.ofFn (take m h l.get)).length = (List.take m l).length

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem sdiff_mem_sdiff [SDiff α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma \ mb ∈ a \ b

Proof state:
α : Type u_1
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 \ a = ma \ mb

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma \ mb ∈ a \ b

Tactic:
simp [sdiff_def]

Result:
α : Type u_1
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 \ a = ma \ mb
-- Mathlib/Topology/Algebra/OpenSubgroup.lean
theorem toSubgroup_injective : Function.Injective
    (fun H ↦ H.toOpenSubgroup.toSubgroup : OpenNormalSubgroup G → Subgroup G) :=
  fun A B h ↦ by
  ext
  dsimp at h
  rw [h]

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : OpenNormalSubgroup G
h : (fun H => ↑H.toOpenSubgroup) A = (fun H => ↑H.toOpenSubgroup) B
⊢ A = B

Tactic:
ext

Result:
case carrier.h
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : OpenNormalSubgroup G
h : (fun H => ↑H.toOpenSubgroup) A = (fun H => ↑H.toOpenSubgroup) B
x✝ : G
⊢ x✝ ∈ (↑A.toOpenSubgroup).carrier ↔ x✝ ∈ (↑B.toOpenSubgroup).carrier

Proof state:
case carrier.h
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : OpenNormalSubgroup G
h : ↑A.toOpenSubgroup = ↑B.toOpenSubgroup
x✝ : G
⊢ x✝ ∈ (↑A.toOpenSubgroup).carrier ↔ x✝ ∈ (↑B.toOpenSubgroup).carrier

Tactic:
rw [h]

Result:
no goals

Proof state:
case carrier.h
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : OpenNormalSubgroup G
h : (fun H => ↑H.toOpenSubgroup) A = (fun H => ↑H.toOpenSubgroup) B
x✝ : G
⊢ x✝ ∈ (↑A.toOpenSubgroup).carrier ↔ x✝ ∈ (↑B.toOpenSubgroup).carrier

Tactic:
dsimp at h

Result:
case carrier.h
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : OpenNormalSubgroup G
h : ↑A.toOpenSubgroup = ↑B.toOpenSubgroup
x✝ : G
⊢ x✝ ∈ (↑A.toOpenSubgroup).carrier ↔ x✝ ∈ (↑B.toOpenSubgroup).carrier