harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
    (not_contains : (toInsert.map Prod.fst).contains k = false) :
    getKey? k (insertListConst l toInsert) = getKey? k l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getKey? k (insertListConst l toInsert) = getKey? k l

Tactic:
unfold insertListConst

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getKey? k (insertList l (List.map Prod.toSigma toInsert)) = getKey? k l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getKey? k (insertList l (List.map Prod.toSigma toInsert)) = getKey? k l

Tactic:
apply getKey?_insertList_of_contains_eq_false

Result:
case not_contains
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains k = false

Proof state:
case not_contains
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains k = false

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma map_stabilizer_le (f : G →* H) (s : Set G) :
    (stabilizer G s).map f ≤ stabilizer H (f '' s)

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
a : H
⊢ ∀ (x : G), x • s = s → f x = a → a • ⇑f '' s = ⇑f '' s

Tactic:
rintro a ha rfl

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
a : G
ha : a • s = s
⊢ f a • ⇑f '' s = ⇑f '' s

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
⊢ Subgroup.map f (stabilizer G s) ≤ stabilizer H (⇑f '' s)

Tactic:
rintro a

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
a : H
⊢ a ∈ Subgroup.map f (stabilizer G s) → a ∈ stabilizer H (⇑f '' s)

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
a : G
ha : a • s = s
⊢ f a • ⇑f '' s = ⇑f '' s

Tactic:
rw [← image_smul_distrib, ha]

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
a : H
⊢ a ∈ Subgroup.map f (stabilizer G s) → a ∈ stabilizer H (⇑f '' s)

Tactic:
simp only [Subgroup.mem_map, mem_stabilizer_iff, exists_prop, forall_exists_index, and_imp]

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
s : Set G
a : H
⊢ ∀ (x : G), x • s = s → f x = a → a • ⇑f '' s = ⇑f '' s
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.eventually_hasSum (hf : HasFPowerSeriesOnBall f p x r) :
    ∀ᶠ y in 𝓝 0, HasSum (fun n : ℕ => p n fun _ : Fin n => y) (f (x + y))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n => (p n) fun x => y) (f (x + y))

Tactic:
filter_upwards [EMetric.ball_mem_nhds (0 : E) hf.r_pos] using fun _ => hf.hasSum

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_inv_of_neg {x : ℝ} (h : x < 0) : arctan x⁻¹ = -(π / 2) - arctan x

Proof state:
x : ℝ
h : x < 0
this : arctan (-x)⁻¹ = π / 2 - arctan (-x)
⊢ arctan x⁻¹ = -(π / 2) - arctan x

Tactic:
rwa [inv_neg, arctan_neg, neg_eq_iff_eq_neg, neg_sub', arctan_neg, neg_neg] at this

Result:
no goals

Proof state:
x : ℝ
h : x < 0
⊢ arctan x⁻¹ = -(π / 2) - arctan x

Tactic:
have := arctan_inv_of_pos (neg_pos.mpr h)

Result:
x : ℝ
h : x < 0
this : arctan (-x)⁻¹ = π / 2 - arctan (-x)
⊢ arctan x⁻¹ = -(π / 2) - arctan x
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem of_a_eq_zero (ha : P.a = 0) : P.toPoly = C P.b * X ^ 2 + C P.c * X + C P.d

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ P.toPoly = C P.b * X ^ 2 + C P.c * X + C P.d

Tactic:
rw [toPoly, ha, C_0, zero_mul, zero_add]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem tendsto_norm' {x : E} : Tendsto (fun a => ‖a‖) (𝓝 x) (𝓝 ‖x‖)

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ Tendsto (fun a => ‖a‖) (𝓝 x) (𝓝 ‖x‖)

Tactic:
simpa using tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (1 : E)) _ _)

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem biUnionIndex_mem (hJ : J ∈ π.biUnion πi) : π.biUnionIndex πi J ∈ π

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ ⋯.choose ∈ π

Tactic:
exact (π.mem_biUnion.1 hJ).choose_spec.1

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J ∈ π

Tactic:
rw [biUnionIndex, dif_pos hJ]

Result:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ ⋯.choose ∈ π
-- Mathlib/CategoryTheory/Adjunction/Evaluation.lean
theorem NatTrans.mono_iff_mono_app' {F G : C ⥤ D} (η : F ⟶ G) : Mono η ↔ ∀ c, Mono (η.app c)

Proof state:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η → ∀ (c : C), Mono (η.app c)

Tactic:
intro h c

Result:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Mono η
c : C
⊢ Mono (η.app c)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η ↔ ∀ (c : C), Mono (η.app c)

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η → ∀ (c : C), Mono (η.app c)

case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Mono (η.app c)) → Mono η

Proof state:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Mono (η.app c)
⊢ Mono η

Tactic:
apply NatTrans.mono_of_mono_app

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Mono η
c : C
⊢ Mono (η.app c)

Tactic:
exact (inferInstance : Mono (((evaluation _ _).obj c).map η))

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Mono (η.app c)) → Mono η

Tactic:
intro _

Result:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Mono (η.app c)
⊢ Mono η
-- Mathlib/FieldTheory/CardinalEmb.lean
theorem iSup_adjoin_eq_top : ⨆ i : ι, E⟮<i⟯ = ⊤

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
⊢ range ⇑b ⊆ ↑(⨆ i, adjoin F (⇑b '' Iio (φ i)))

Tactic:
rintro _ ⟨i, rfl⟩

Result:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
⊢ b i ∈ ↑(⨆ i, adjoin F (⇑b '' Iio (φ i)))

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
⊢ ⨆ i, adjoin F (⇑b ∘ φ '' Iio i) = ⊤

Tactic:
simp_rw [adjoin_image_leastExt, eq_top_iff, ← adjoin_basis_eq_top, adjoin_le_iff]

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
⊢ range ⇑b ⊆ ↑(⨆ i, adjoin F (⇑b '' Iio (φ i)))

Proof state:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
⊢ b i ∈ ↑(⨆ i, adjoin F (⇑b '' Iio (φ i)))

Tactic:
refine le_iSup (α := IntermediateField F E) _ (i⁺) (subset_adjoin _ _ ⟨i, ?_, rfl⟩)

Result:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
⊢ i ∈ Iio (φ (i⁺))

Proof state:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
⊢ i ∈ Iio (φ (i⁺))

Tactic:
exact (lt_succ i).trans_le strictMono_leastExt.le_apply

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) :
    Tendsto (fun x => r * f x) l atTop ↔ 0 < r

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
x : β
hx : 0 ≤ f x
hrx : 0 < r * f x
⊢ False

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg hr hx).not_lt hrx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r

Tactic:
refine ⟨fun hrf => not_le.mp fun hr => ?_, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
⊢ False

Tactic:
rcases ((h.eventually_ge_atTop 0).and (hrf.eventually_gt_atTop 0)).exists with ⟨x, hx, hrx⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
x : β
hx : 0 ≤ f x
hrx : 0 < r * f x
⊢ False
-- Mathlib/Algebra/Order/Ring/Abs.lean
@[simp] lemma one_le_sq_iff_one_le_abs (a : α) : 1 ≤ a ^ 2 ↔ 1 ≤ |a|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a : α
⊢ 1 ≤ a ^ 2 ↔ 1 ≤ |a|

Tactic:
simpa only [one_pow, abs_one] using @sq_le_sq _ _ 1 a

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity {r : R}
    (hr : r ≠ 0) (I : { I : Ideal R | I ∈ normalizedFactors (Ideal.span ({r} : Set R)) }) :
    emultiplicity ((normalizedFactorsEquivSpanNormalizedFactors hr).symm I : R) r =
      emultiplicity (I : Ideal R) (Ideal.span {r})

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
x : ↑{d | d ∈ normalizedFactors r}
hx : (normalizedFactorsEquivSpanNormalizedFactors hr) x = I
⊢ emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (span {r})

Tactic:
obtain ⟨a, ha⟩ := x

Result:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
hx : (normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩ = I
⊢ emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (span {r})

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
⊢ emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (span {r})

Tactic:
obtain ⟨x, hx⟩ := (normalizedFactorsEquivSpanNormalizedFactors hr).surjective I

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
x : ↑{d | d ∈ normalizedFactors r}
hx : (normalizedFactorsEquivSpanNormalizedFactors hr) x = I
⊢ emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (span {r})

Proof state:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
hx : (normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩ = I
⊢ emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = emultiplicity (↑I) (span {r})

Tactic:
rw [hx.symm, Equiv.symm_apply_apply, Subtype.coe_mk,
  emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity hr ha]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem push_pull' (f : α → β) (F : Filter α) (G : Filter β) :
    map f (comap f G ⊓ F) = G ⊓ map f F

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (comap f G ⊓ F) = G ⊓ map f F

Tactic:
simp only [Filter.push_pull, inf_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_union_congr_of_subset {t₁ t₂ : Set α} (hs : s₁ ⊆ s₂) (hsμ : μ s₂ ≤ μ s₁)
    (ht : t₁ ⊆ t₂) (htμ : μ t₂ ≤ μ t₁) : μ (s₁ ∪ t₁) = μ (s₂ ∪ t₂)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ s₂ ≤ μ s₁
ht : t₁ ⊆ t₂
htμ : μ t₂ ≤ μ t₁
⊢ μ (⋃ b, bif b then s₁ else t₁) = μ (⋃ b, bif b then s₂ else t₂)

Tactic:
exact measure_iUnion_congr_of_subset (Bool.forall_bool.2 ⟨ht, hs⟩) (Bool.forall_bool.2 ⟨htμ, hsμ⟩)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ s₂ ≤ μ s₁
ht : t₁ ⊆ t₂
htμ : μ t₂ ≤ μ t₁
⊢ μ (s₁ ∪ t₁) = μ (s₂ ∪ t₂)

Tactic:
rw [union_eq_iUnion, union_eq_iUnion]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ s₂ ≤ μ s₁
ht : t₁ ⊆ t₂
htμ : μ t₂ ≤ μ t₁
⊢ μ (⋃ b, bif b then s₁ else t₁) = μ (⋃ b, bif b then s₂ else t₂)
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_pos_iff : 0 < krullDim α ↔ ∃ x y : α, x < y

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x y : α), ¬x < y

Tactic:
simp_rw [← isMax_iff_forall_not_lt, ← krullDim_nonpos_iff_forall_isMax]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ ¬0 < krullDim α ↔ ¬∃ x y, x < y

Tactic:
push_neg

Result:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x y : α), ¬x < y

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ 0 < krullDim α ↔ ∃ x y, x < y

Tactic:
rw [← not_iff_not]

Result:
α : Type u_1
inst✝ : Preorder α
⊢ ¬0 < krullDim α ↔ ¬∃ x y, x < y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_flatten {L : Vector (Vector α n) m} : a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l

Proof state:
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
l : Vector α n
h₁ : l ∈ L
h₂ : a ∈ l
⊢ a ∈ l.toArray

Tactic:
simpa using h₂

Result:
no goals

Proof state:
case mk.mp
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
⊢ (∃ l, (∃ a, a ∈ L ∧ a.toArray = l) ∧ a ∈ l) → ∃ l, l ∈ L ∧ a ∈ l

Tactic:
rintro ⟨_, ⟨l, h₁, rfl⟩, h₂⟩

Result:
case mk.mp.intro.intro.intro.intro
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
l : Vector α n
h₁ : l ∈ L
h₂ : a ∈ l.toArray
⊢ ∃ l, l ∈ L ∧ a ∈ l

Proof state:
case mk.mp.intro.intro.intro.intro
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
l : Vector α n
h₁ : l ∈ L
h₂ : a ∈ l.toArray
⊢ ∃ l, l ∈ L ∧ a ∈ l

Tactic:
exact ⟨l, h₁, by simpa using h₂⟩

Result:
no goals

Proof state:
case mk.mpr
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
⊢ (∃ l, l ∈ L ∧ a ∈ l) → ∃ l, (∃ a, a ∈ L ∧ a.toArray = l) ∧ a ∈ l

Tactic:
rintro ⟨l, h₁, h₂⟩

Result:
case mk.mpr.intro.intro
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
l : Vector α n
h₁ : l ∈ L
h₂ : a ∈ l
⊢ ∃ l, (∃ a, a ∈ L ∧ a.toArray = l) ∧ a ∈ l

Proof state:
case mk.mpr.intro.intro
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
l : Vector α n
h₁ : l ∈ L
h₂ : a ∈ l
⊢ ∃ l, (∃ a, a ∈ L ∧ a.toArray = l) ∧ a ∈ l

Tactic:
exact ⟨l.toArray, ⟨l, h₁, rfl⟩, by simpa using h₂⟩

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
a : α
L : Vector (Vector α n) m
⊢ a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l

Tactic:
rcases L with ⟨L, rfl⟩

Result:
case mk
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
⊢ a ∈ { toArray := L, size_toArray := ⋯ }.flatten ↔ ∃ l, l ∈ { toArray := L, size_toArray := ⋯ } ∧ a ∈ l

Proof state:
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
l : Vector α n
h₁ : l ∈ L
h₂ : a ∈ l.toArray
⊢ a ∈ l

Tactic:
simpa using h₂

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
⊢ (∃ l, (∃ a, a ∈ L ∧ a.toArray = l) ∧ a ∈ l) ↔ ∃ l, l ∈ L ∧ a ∈ l

Tactic:
constructor

Result:
case mk.mp
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
⊢ (∃ l, (∃ a, a ∈ L ∧ a.toArray = l) ∧ a ∈ l) → ∃ l, l ∈ L ∧ a ∈ l

case mk.mpr
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
⊢ (∃ l, l ∈ L ∧ a ∈ l) → ∃ l, (∃ a, a ∈ L ∧ a.toArray = l) ∧ a ∈ l

Proof state:
case mk
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
⊢ a ∈ { toArray := L, size_toArray := ⋯ }.flatten ↔ ∃ l, l ∈ { toArray := L, size_toArray := ⋯ } ∧ a ∈ l

Tactic:
simp [Array.mem_flatten]

Result:
case mk
α : Type u_1
n : Nat
a : α
L : Array (Vector α n)
⊢ (∃ l, (∃ a, a ∈ L ∧ a.toArray = l) ∧ a ∈ l) ↔ ∃ l, l ∈ L ∧ a ∈ l
-- Mathlib/Data/Nat/Init.lean
lemma leRec_succ_left {motive : (m : ℕ) → n ≤ m → Sort*}
    (refl le_succ_of_le) {m} (h1 : n ≤ m) (h2 : n + 1 ≤ m) :
    -- the `@` is needed for this to elaborate, even though we only provide explicit arguments!
    @leRec _ _ (le_succ_of_le (Nat.le_refl _) refl)
        (fun _ h ih => le_succ_of_le (le_of_succ_le h) ih) _ h2 =
      leRec (motive := motive) refl le_succ_of_le h1

Proof state:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
m : ℕ
h1 : n ≤ m
h2 : n + 1 ≤ m
⊢ leRec (le_succ_of_le ⋯ refl) (fun x h ih => le_succ_of_le ⋯ ih) h2 = leRec refl le_succ_of_le h1

Tactic:
rw [leRec_trans _ _ (le_succ n) h2, leRec_succ']

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem mem_diag : x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α × α
⊢ x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2

Tactic:
simp +contextual [diag]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem map_lt [LT α] [LT β]
    {l₁ l₂ : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) :
    map f l₁ < map f l₂

Proof state:
α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : LT α
inst✝ : LT β
l₁ l₂ : Vector α n
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ < l₂
⊢ map f l₁ < map f l₂

Tactic:
simpa using Array.map_lt w h

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
lemma BlockTriangular.charpoly {α : Type*} {b : n → α} [LinearOrder α] (h : M.BlockTriangular b) :
    M.charpoly = ∏ a ∈ image b univ, (M.toSquareBlock b a).charpoly

Proof state:
R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
α : Type u_5
b : n → α
inst✝ : LinearOrder α
h : M.BlockTriangular b
⊢ M.charpoly = ∏ a ∈ image b univ, (M.toSquareBlock b a).charpoly

Tactic:
simp only [Matrix.charpoly, h.charmatrix.det, charmatrix_toSquareBlock]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem empty_isBase_iff : M.IsBase ∅ ↔ M = loopyOn M.E

Proof state:
α : Type u_1
M : Matroid α
⊢ (∀ ⦃y : Set α⦄, M.Indep y → y = ∅) ↔ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)

Tactic:
exact ⟨fun h I _ ↦ ⟨@h _, fun hI ↦ by simp [hI]⟩, fun h I hI ↦ (h hI.subset_ground).1 hI⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
h : ∀ ⦃y : Set α⦄, M.Indep y → y = ∅
I : Set α
x✝ : I ⊆ M.E
hI : I = ∅
⊢ M.Indep I

Tactic:
simp [hI]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ↔ M = loopyOn M.E

Tactic:
simp only [isBase_iff_maximal_indep, Maximal, empty_indep, le_eq_subset, empty_subset,
  subset_empty_iff, true_implies, true_and, ext_iff_indep, loopyOn_ground,
  loopyOn_indep_iff]

Result:
α : Type u_1
M : Matroid α
⊢ (∀ ⦃y : Set α⦄, M.Indep y → y = ∅) ↔ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)
-- Mathlib/GroupTheory/Perm/DomMulAct.lean
lemma stabilizerEquiv_invFun_eq (g : ∀ i, Perm {a // f a = i}) {a : α} {i : ι} (h : f a = i) :
    stabilizerEquiv_invFun g a = g i ⟨a, h⟩

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
i : ι
h : f a = i
⊢ stabilizerEquiv_invFun g a = ↑((g i) ⟨a, h⟩)

Tactic:
subst h

Result:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ stabilizerEquiv_invFun g a = ↑((g (f a)) ⟨a, ⋯⟩)

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ stabilizerEquiv_invFun g a = ↑((g (f a)) ⟨a, ⋯⟩)

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma snd_zero : snd (0 : Kernel α (β × γ)) = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ snd 0 = 0

Tactic:
simp [snd]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_X_pow_eq_C_mul (n k : ℕ) :
    derivative^[k] (X ^ n : R[X]) = C (Nat.descFactorial n k : R) * X ^ (n - k)

Proof state:
R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ (⇑derivative)^[k] (X ^ n) = C ↑(n.descFactorial k) * X ^ (n - k)

Tactic:
rw [iterate_derivative_X_pow_eq_natCast_mul n k, C_eq_natCast]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem unbounded_lt_iff_unbounded_le [Preorder α] [NoMaxOrder α] :
    Unbounded (· < ·) s ↔ Unbounded (· ≤ ·) s

Proof state:
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ Unbounded (fun x1 x2 => x1 < x2) s ↔ Unbounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
simp_rw [← not_bounded_iff, bounded_le_iff_bounded_lt]

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem Commute.one_div_add_one_div (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
    1 / a + 1 / b = (a + b) / (a * b)

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + 1 / b = (a + b) / (a * b)

Tactic:
rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem succ_sub_sub_succ (n m k) : succ n - m - succ k = n - m - k

Proof state:
n m k : Nat
⊢ n.succ - m - k.succ = n - m - k

Tactic:
rw [Nat.sub_sub, Nat.sub_sub, add_succ, succ_sub_succ]

Result:
no goals