harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_mono_right (b : Ordinal) {x y : Ordinal} (xy : x ≤ y) : log b x ≤ log b y

Proof state:
case inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
⊢ log b x ≤ log b y

Tactic:
obtain hb | hb := lt_or_le 1 b

Result:
case inr.inl
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ log b y

case inr.inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ log b y

Proof state:
case inl
b y : Ordinal.{u_1}
xy : 0 ≤ y
⊢ log b 0 ≤ log b y

Tactic:
simp_rw [log_zero_right, Ordinal.zero_le]

Result:
no goals

Proof state:
b x y : Ordinal.{u_1}
xy : x ≤ y
⊢ log b x ≤ log b y

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
b y : Ordinal.{u_1}
xy : 0 ≤ y
⊢ log b 0 ≤ log b y

case inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
⊢ log b x ≤ log b y

Proof state:
case inr.inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ log b y

Tactic:
rw [log_of_left_le_one hb, log_of_left_le_one hb]

Result:
no goals

Proof state:
case inr.inl
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ log b y

Tactic:
exact (opow_le_iff_le_log hb (hx.bot_lt.trans_le xy).ne').1 <|
  (opow_log_le_self _ hx).trans xy

Result:
no goals
-- Mathlib/Order/Filter/EventuallyConst.lean
theorem HasBasis.eventuallyConst_iff {ι : Sort*} {p : ι → Prop} {s : ι → Set α}
    (h : l.HasBasis p s) : EventuallyConst f l ↔ ∃ i, p i ∧ ∀ x ∈ s i, ∀ y ∈ s i, f x = f y :=
  (h.map f).subsingleton_iff.trans <| by simp only [Set.Subsingleton, forall_mem_image]

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
ι : Sort u_5
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (∃ i, p i ∧ (f '' s i).Subsingleton) ↔ ∃ i, p i ∧ ∀ x ∈ s i, ∀ y ∈ s i, f x = f y

Tactic:
simp only [Set.Subsingleton, forall_mem_image]

Result:
no goals
-- Mathlib/Topology/UniformSpace/AbstractCompletion.lean
theorem uniformContinuous_extend : UniformContinuous (pkg.extend f)

Proof state:
case pos
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (pkg.extend f)

Tactic:
rw [pkg.extend_def hf]

Result:
case pos
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)

Proof state:
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (if UniformContinuous f then ⋯.extend f else fun x => f (⋯.some x))

Tactic:
rw [if_neg hf]

Result:
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f (⋯.some x)

Proof state:
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f (⋯.some x)

Tactic:
exact uniformContinuous_of_const fun a b => by congr 1

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
a b : pkg.space
⊢ f (⋯.some a) = f (⋯.some b)

Tactic:
congr 1

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (pkg.extend f)

Tactic:
change UniformContinuous (ite _ _ _)

Result:
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (if UniformContinuous f then ⋯.extend f else fun x => f (⋯.some x))

Proof state:
case pos
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)

Tactic:
exact uniformContinuous_uniformly_extend pkg.isUniformInducing pkg.dense hf

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
⊢ UniformContinuous (pkg.extend f)

Tactic:
by_cases hf : UniformContinuous f

Result:
case pos
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (pkg.extend f)

case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (pkg.extend f)
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_approx_end' {n} {x a b : ℝ} (m : ℕ) (e₁ : n + 1 = m) (rm : ℝ) (er : ↑m = rm)
    (h : |x| ≤ 1) (e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)) :
    |exp x - expNear n x a| ≤ |x| ^ n / n.factorial * b

Proof state:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)
⊢ |rexp x - expNear n x a| ≤ |x| ^ n / ↑n.factorial * b

Tactic:
exact exp_approx_succ _ e₁ _ _ (by simpa using e) (exp_approx_end _ _ _ e₁ h)

Result:
no goals

Proof state:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)
⊢ |1 + x / ↑m * 0 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)

Tactic:
simpa using e

Result:
no goals

Proof state:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
rm : ℝ
er : ↑m = rm
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)
⊢ |rexp x - expNear n x a| ≤ |x| ^ n / ↑n.factorial * b

Tactic:
subst er

Result:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)
⊢ |rexp x - expNear n x a| ≤ |x| ^ n / ↑n.factorial * b
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem zpow_smul_eq_iff_period_dvd {j : ℤ} {g : G} {a : α} :
    g ^ j • a = a ↔ (period g a : ℤ) ∣ j

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
⊢ g ^ j • a = a ↔ ↑(period g a) ∣ j

Tactic:
rcases j with n | n

Result:
case ofNat
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
n : ℕ
⊢ g ^ Int.ofNat n • a = a ↔ ↑(period g a) ∣ Int.ofNat n

case negSucc
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
n : ℕ
⊢ g ^ Int.negSucc n • a = a ↔ ↑(period g a) ∣ Int.negSucc n

Proof state:
case negSucc
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
n : ℕ
⊢ g ^ Int.negSucc n • a = a ↔ ↑(period g a) ∣ Int.negSucc n

Tactic:
rw [Int.negSucc_coe, zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg,
  Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]

Result:
no goals

Proof state:
case ofNat
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
n : ℕ
⊢ g ^ Int.ofNat n • a = a ↔ ↑(period g a) ∣ Int.ofNat n

Tactic:
rw [Int.ofNat_eq_coe, zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem congr_right {a b c : α} : s(a, b) = s(a, c) ↔ b = c

Proof state:
α : Type u_1
a b c : α
⊢ s(a, b) = s(a, c) ↔ b = c

Tactic:
simp (config := {contextual := true})

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- Transfer reflection of limits along a natural isomorphism in the diagram. -/
lemma reflectsLimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [ReflectsLimit K₁ F] :
    ReflectsLimit K₂ F where
  reflects {c} t := ⟨by
    apply IsLimit.postcomposeInvEquiv h c (isLimitOfReflects F _)
    apply ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F :) _).symm t).ofIsoLimit _
    exact Cones.ext (Iso.refl _)⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ (Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c) ≅ F.mapCone ((Cones.postcompose h.inv).obj c)

Tactic:
exact Cones.ext (Iso.refl _)

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit c

Tactic:
apply IsLimit.postcomposeInvEquiv h c (isLimitOfReflects F _)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone ((Cones.postcompose h.inv).obj c))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone ((Cones.postcompose h.inv).obj c))

Tactic:
apply ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F :) _).symm t).ofIsoLimit _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ (Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c) ≅ F.mapCone ((Cones.postcompose h.inv).obj c)
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem frontier_cthickening_disjoint (A : Set α) :
    Pairwise (Disjoint on fun r : ℝ≥0 => frontier (cthickening r A)) := fun r₁ r₂ hr =>
  ((disjoint_singleton.2 <| by simpa).preimage _).mono (frontier_cthickening_subset _)
    (frontier_cthickening_subset _)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ≥0
hr : r₁ ≠ r₂
⊢ ENNReal.ofReal ↑r₁ ≠ ENNReal.ofReal ↑r₂

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem exists_push_of_size_pos {xs : Array α} (h : 0 < xs.size) :
    ∃ (ys : Array α) (a : α), xs = ys.push a

Proof state:
α : Type u_1
xs : Array α
h : xs ≠ #[]
⊢ ∃ ys a, xs = ys.push a

Tactic:
exact exists_push_of_ne_empty h

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
h : 0 < xs.size
⊢ ∃ ys a, xs = ys.push a

Tactic:
replace h : xs ≠ #[] := size_pos.mp h

Result:
α : Type u_1
xs : Array α
h : xs ≠ #[]
⊢ ∃ ys a, xs = ys.push a
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem anisotropic_of_pi [Fintype ι]
    {Q : ∀ i, QuadraticMap R (Mᵢ i) P} (h : (pi Q).Anisotropic) : ∀ i, (Q i).Anisotropic

Proof state:
case refine_2
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
this : x = 0
⊢ x = 0

Tactic:
exact this

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
this : Pi.single i x i = 0
⊢ x = 0

Tactic:
rw [Pi.single_eq_same] at this

Result:
case refine_2
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
this : x = 0
⊢ x = 0

Proof state:
case neg
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : ¬j = i
⊢ (Q j) (Pi.single i x j) = 0

Tactic:
rw [Pi.single_eq_of_ne hji, map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
    (h : (k == k') = false) : k' ∈ m.alter k f ↔ k' ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : (k == k') = false
⊢ k' ∈ m.alter k f ↔ k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_alter_of_beq_eq_false, h]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.le_one {a : A} (h : ∀ x ∈ spectrum R a, x ≤ 1) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.747067) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
h : ∀ x ∈ spectrum R a, x ≤ 1
ha : autoParam (p a) _auto✝
⊢ a ≤ 1

Tactic:
simpa using le_algebraMap_of_spectrum_le h

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem not_top_subset : ¬⊤ ⊆ s ↔ ∃ a, a ∉ s

Proof state:
α : Type u
s : Set α
⊢ ¬⊤ ⊆ s ↔ ∃ a, a ∉ s

Tactic:
simp [not_subset]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma smul_fin3 (P : Fin 3 → R) (u : R) : u • P = ![u * P x, u * P y, u * P z]

Proof state:
R : Type r
inst✝ : CommRing R
P : Fin 3 → R
u : R
⊢ u • P = ![u * P x, u * P y, u * P z]

Tactic:
simp [← List.ofFn_inj]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem continuousAt_of_comp_left {X : Type*} [TopologicalSpace X] {f : X → Z} {x : X}
    (e : Trivialization F proj) (hf_proj : ContinuousAt (proj ∘ f) x) (he : proj (f x) ∈ e.baseSet)
    (hf : ContinuousAt (e ∘ f) x) : ContinuousAt f x

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ f ⁻¹' e.source ∈ 𝓝 x

Tactic:
rw [e.source_eq, ← preimage_comp]

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 x

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt (↑e.toPartialHomeomorph ∘ f) x

Tactic:
exact hf

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 x

Tactic:
exact hf_proj.preimage_mem_nhds (e.open_baseSet.mem_nhds he)

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt f x

Tactic:
rw [e.continuousAt_iff_continuousAt_comp_left]

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt (↑e.toPartialHomeomorph ∘ f) x

B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ f ⁻¹' e.source ∈ 𝓝 x
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem toSubalgebra_mk (s : Submodule R A) (h1 hmul) :
    s.toSubalgebra h1 hmul =
      Subalgebra.mk ⟨⟨⟨s, @hmul⟩, h1⟩, s.add_mem, s.zero_mem⟩
        (by intro r; rw [Algebra.algebraMap_eq_smul_one]; apply s.smul_mem _ h1) :=
  rfl

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
⊢ ∀ (r : R),
    (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
intro r

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ r • 1 ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ r • 1 ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
apply s.smul_mem _ h1

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem insert_pi (i : ι) (s : Set ι) (t : ∀ i, Set (α i)) :
    pi (insert i s) t = eval i ⁻¹' t i ∩ pi s t

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
i : ι
s : Set ι
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ (insert i s).pi t ↔ x✝ ∈ eval i ⁻¹' t i ∩ s.pi t

Tactic:
simp [pi, or_imp, forall_and]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
i : ι
s : Set ι
t : (i : ι) → Set (α i)
⊢ (insert i s).pi t = eval i ⁻¹' t i ∩ s.pi t

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
i : ι
s : Set ι
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ (insert i s).pi t ↔ x✝ ∈ eval i ⁻¹' t i ∩ s.pi t
-- Mathlib/Logic/Basic.lean
theorem xor_not_not : Xor' (¬a) (¬b) ↔ Xor' a b

Proof state:
a b : Prop
⊢ Xor' (¬a) ¬b ↔ Xor' a b

Tactic:
simp [Xor', or_comm, and_comm]

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `y + X`
has Gaussian law with mean `μ + y` and variance `v`. -/
lemma gaussianReal_const_add {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (y : ℝ) :
    Measure.map (fun ω ↦ y + X ω) ℙ = gaussianReal (μ + y) v

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
⊢ Measure.map (fun ω => y + X ω) ℙ = gaussianReal (μ + y) v

Tactic:
simp_rw [add_comm y]

Result:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
⊢ Measure.map (fun ω => X ω + y) ℙ = gaussianReal (μ + y) v

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
y : ℝ
⊢ Measure.map (fun ω => X ω + y) ℙ = gaussianReal (μ + y) v

Tactic:
exact gaussianReal_add_const hX y

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem get!_eq_get!ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) [Inhabited (β a)] :
    get! m a = get!ₘ m a

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : Hashable α
m : Raw₀ α β
a : α
inst✝ : Inhabited (β a)
⊢ m.get! a = m.get!ₘ a

Tactic:
simp [get!, get!ₘ, get?ₘ, List.getValueCast!_eq_getValueCast?, bucket]

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
private lemma jacobiMatrix_comp_₁₂ : (Q.comp P).jacobiMatrix.toBlocks₁₂ = 0

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : DecidableEq (Q.comp P).rels
inst✝ : Fintype (Q.comp P).rels
⊢ (Q.comp P).jacobiMatrix.toBlocks₁₂ = 0

Tactic:
ext i j : 1

Result:
case a
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : DecidableEq (Q.comp P).rels
inst✝ : Fintype (Q.comp P).rels
i : Q.rels
j : P.rels
⊢ (Q.comp P).jacobiMatrix.toBlocks₁₂ i j = 0 i j

Proof state:
case a
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : DecidableEq (Q.comp P).rels
inst✝ : Fintype (Q.comp P).rels
i : Q.rels
j : P.rels
⊢ (Q.comp P).jacobiMatrix.toBlocks₁₂ i j = 0 i j

Tactic:
simp [Matrix.toBlocks₁₂, jacobiMatrix_comp_inl_inr]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
/-- The derivative of `klFun` at `x ≠ 0` is `log x`. -/
lemma hasDerivAt_klFun (hx : x ≠ 0) : HasDerivAt klFun (log x) x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt klFun (log x) x

Tactic:
convert ((hasDerivAt_mul_log hx).add (hasDerivAt_const x 1)).sub (hasDerivAt_id x) using 1

Result:
case h.e'_9
x : ℝ
hx : x ≠ 0
⊢ log x = log x + 1 + 0 - 1

Proof state:
case h.e'_9
x : ℝ
hx : x ≠ 0
⊢ log x = log x + 1 + 0 - 1

Tactic:
ring

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem Ici_iSup (f : ι → α) : Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
  ext fun _ => by simp only [mem_Ici, iSup_le_iff, mem_iInter]

Proof state:
α : Type u_1
ι : Sort u_5
inst✝ : CompleteLattice α
f : ι → α
x✝ : α
⊢ x✝ ∈ Ici (⨆ i, f i) ↔ x✝ ∈ ⋂ i, Ici (f i)

Tactic:
simp only [mem_Ici, iSup_le_iff, mem_iInter]

Result:
no goals
-- Mathlib/Data/Array/ExtractLemmas.lean
theorem extract_eq_of_size_le_end {l p : Nat} {a : Array α} (h : a.size ≤ l) :
    a.extract p l = a.extract p a.size

Proof state:
α : Type u
l p : Nat
a : Array α
h : a.size ≤ l
⊢ a.extract p l = a.extract p

Tactic:
simp only [extract, Nat.min_eq_right h, Nat.sub_eq, mkEmpty_eq, Nat.min_self]

Result:
no goals