harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Ico_mul_Ioc_subset' (a b c d : α) : Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c < z
hzd : z ≤ d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ioo (a * c) (b * d)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
⊢ Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c < z
hzd : z ≤ d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ioo (a * c) (b * d)

Tactic:
exact ⟨mul_lt_mul_of_le_of_lt hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)

Tactic:
have := mulRightMono_of_mulRightStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.bot : ωScottContinuous (⊥ : α → β)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ ωScottContinuous ⊥

Tactic:
rw [← sSup_empty]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ ωScottContinuous (SupSet.sSup ∅)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ ωScottContinuous (SupSet.sSup ∅)

Tactic:
exact ωScottContinuous.sSup (by simp)

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ ∀ f ∈ ∅, ωScottContinuous f

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem mem_nhdsWithin {t : Set α} {a : α} {s : Set α} :
    t ∈ 𝓝[s] a ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
t : Set α
a : α
s : Set α
⊢ t ∈ 𝓝[s] a ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t

Tactic:
simpa only [and_assoc, and_left_comm] using (nhdsWithin_basis_open a s).mem_iff

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem toNNRat_lt_iff_lt_coe {p : ℚ≥0} (hq : 0 ≤ q) : toNNRat q < p ↔ q < ↑p

Proof state:
q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ q.toNNRat < p ↔ q < ↑p

Tactic:
rw [← coe_lt_coe, Rat.coe_toNNRat q hq]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem denom_zero : denom (0 : RatFunc K) = 1

Proof state:
K : Type u
inst✝ : Field K
⊢ denom 0 = 1

Tactic:
convert denom_div (0 : K[X]) one_ne_zero <;> simp

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Cardinality.lean
theorem Set.Countable.dense_compl
    {E : Type u} (𝕜 : Type*) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E]
    [Module 𝕜 E] [Nontrivial E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E]
    {s : Set E} (hs : s.Countable) : Dense sᶜ

Proof state:
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ False

Tactic:
apply lt_irrefl (ℵ₀ : Cardinal.{u})

Result:
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ ℵ₀ < ℵ₀

Proof state:
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
⊢ interior s = ∅

Tactic:
by_contra H

Result:
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ False

Proof state:
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
⊢ Dense sᶜ

Tactic:
rw [← interior_eq_empty_iff_dense_compl]

Result:
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
⊢ interior s = ∅

Proof state:
E : Type u
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ ℵ₀ < ℵ₀

Tactic:
calc
  (ℵ₀ : Cardinal.{u}) < 𝔠 := aleph0_lt_continuum
  _ ≤ #(interior s) :=
    continuum_le_cardinal_of_isOpen 𝕜 isOpen_interior (nmem_singleton_empty.1 H)
  _ ≤ #s := mk_le_mk_of_subset interior_subset
  _ ≤ ℵ₀ := le_aleph0 hs

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem euler_criterion {a : ZMod p} (ha : a ≠ 0) : IsSquare (a : ZMod p) ↔ a ^ (p / 2) = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a ↔ a ^ (p / 2) = 1

Tactic:
apply (iff_congr _ (by simp [Units.ext_iff])).mp (euler_criterion_units p (Units.mk0 a ha))

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, y ^ 2 = Units.mk0 a ha) ↔ IsSquare a

Proof state:
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a → ∃ y, ↑y * ↑y = a

Tactic:
rintro ⟨y, rfl⟩

Result:
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
⊢ ∃ y_1, ↑y_1 * ↑y_1 = y * y

Proof state:
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy) = y * y

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) ↔ IsSquare a

Tactic:
constructor

Result:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) → IsSquare a

case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a → ∃ y, ↑y * ↑y = a

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, y ^ 2 = Units.mk0 a ha) ↔ IsSquare a

Tactic:
simp only [Units.ext_iff, sq, Units.val_mk0, Units.val_mul]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) ↔ IsSquare a

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ Units.mk0 a ha ^ (p / 2) = 1 ↔ a ^ (p / 2) = 1

Tactic:
simp [Units.ext_iff]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
ha : 0 * 0 ≠ 0
⊢ False

Tactic:
simp [zero_pow, mul_zero, ne_eq, not_true] at ha

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
⊢ y ≠ 0

Tactic:
rintro rfl

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
ha : 0 * 0 ≠ 0
⊢ False

Proof state:
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
⊢ ∃ y_1, ↑y_1 * ↑y_1 = y * y

Tactic:
have hy : y ≠ 0 := by
  rintro rfl
  simp [zero_pow, mul_zero, ne_eq, not_true] at ha

Result:
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ y_1, ↑y_1 * ↑y_1 = y * y

Proof state:
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ y_1, ↑y_1 * ↑y_1 = y * y

Tactic:
refine ⟨Units.mk0 y hy, ?_⟩

Result:
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy) = y * y

Proof state:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) → IsSquare a

Tactic:
rintro ⟨y, hy⟩

Result:
case mp.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
y : (ZMod p)ˣ
hy : ↑y * ↑y = a
⊢ IsSquare a

Proof state:
case mp.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
y : (ZMod p)ˣ
hy : ↑y * ↑y = a
⊢ IsSquare a

Tactic:
exact ⟨y, hy.symm⟩

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem two_zsmul_oangle_of_parallel {p₁ p₂ p₃ p₄ p₅ p₆ : P}
    (h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]) (h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]) :
    (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₄ p₅ p₆

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}
h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆

Tactic:
exact two_zsmul_oangle_of_vectorSpan_eq h₁₂₄₅ h₃₂₆₅

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : affineSpan ℝ {p₁, p₂} ∥ affineSpan ℝ {p₄, p₅}
h₃₂₆₅ : affineSpan ℝ {p₃, p₂} ∥ affineSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆

Tactic:
rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq] at h₁₂₄₅ h₃₂₆₅

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}
h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
-- Mathlib/Logic/Equiv/Set.lean
theorem symm_image_subset {α β} (e : α ≃ β) (s : Set α) (t : Set β) :
    e.symm '' t ⊆ s ↔ t ⊆ e '' s

Proof state:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ ⇑e.symm '' t ⊆ s ↔ t ⊆ ⇑e '' s

Tactic:
rw [image_subset_iff, e.image_eq_preimage]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem not_disjoint_iff_nonempty_inter : ¬Disjoint s t ↔ (s ∩ t).Nonempty :=
  not_disjoint_iff.trans <| by simp [Finset.Nonempty]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a ∈ s, a ∈ t) ↔ (s ∩ t).Nonempty

Tactic:
simp [Finset.Nonempty]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem pow_eq_span_pow_set (n : ℕ) : M ^ n = span R ((M : Set A) ^ n)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
n : ℕ
⊢ M ^ n = span R (↑M ^ n)

Tactic:
rw [← span_pow, span_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem inr_pushoutZeroZeroIso_hom (X Y : C) [HasBinaryCoproduct X Y] :
    pushout.inr _ _ ≫ (pushoutZeroZeroIso X Y).hom = coprod.inr

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr 0 0 ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr ⋯,
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inr

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr 0 0 ≫ (pushoutZeroZeroIso X Y).hom = coprod.inr

Tactic:
dsimp [pushoutZeroZeroIso]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr 0 0 ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr ⋯,
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inr
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_closure_pair {A : Type*} [CommMonoid A] (a b c : A) :
    c ∈ Submonoid.closure ({a, b} : Set A) ↔ ∃ m n : ℕ, a ^ m * b ^ n = c

Proof state:
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
rw [← Set.singleton_union, Submonoid.closure_union, mem_sup]

Result:
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y ∈ closure {a}, ∃ z ∈ closure {b}, y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c

Proof state:
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y ∈ closure {a}, ∃ z ∈ closure {b}, y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
simp_rw [mem_closure_singleton, exists_exists_eq_and]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_modifyNth_eq (f : α → α) (n) (l : List α) :
    (modify f n l).get? n = f <$> l.get? n

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ (modify f n l).get? n = f <$> l.get? n

Tactic:
simp [getElem?_modify_eq]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem PartialHomeomorph.analyticAt_symm' (f : PartialHomeomorph E F) {a : E}
    {i : E ≃L[𝕜] F} (h0 : a ∈ f.source) (h : AnalyticAt 𝕜 f a) (h' : fderiv 𝕜 f a = i) :
    AnalyticAt 𝕜 f.symm (f a)

Proof state:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f) a = ↑i
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f) p a
this : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ AnalyticAt 𝕜 (↑f.symm) (↑f a)

Tactic:
exact (f.hasFPowerSeriesAt_symm h0 hp this).analyticAt

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f) a = ↑i
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f) p a
⊢ p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i

Tactic:
simp [← h', hp.fderiv_eq]

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f) a = ↑i
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f) p a
⊢ AnalyticAt 𝕜 (↑f.symm) (↑f a)

Tactic:
have : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i := by simp [← h', hp.fderiv_eq]

Result:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f) a = ↑i
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f) p a
this : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ AnalyticAt 𝕜 (↑f.symm) (↑f a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h : AnalyticAt 𝕜 (↑f) a
h' : fderiv 𝕜 (↑f) a = ↑i
⊢ AnalyticAt 𝕜 (↑f.symm) (↑f a)

Tactic:
rcases h with ⟨p, hp⟩

Result:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
h' : fderiv 𝕜 (↑f) a = ↑i
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt (↑f) p a
⊢ AnalyticAt 𝕜 (↑f.symm) (↑f a)
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_le_iff_le_mul (hb0 : b ≠ 0 ∨ c ≠ ∞) (hbt : b ≠ ∞ ∨ c ≠ 0) :
    a / b ≤ c ↔ a ≤ c * b

Proof state:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ⊤
hbt : b ≠ ⊤ ∨ c ≠ 0
⊢ a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹

Tactic:
refine (ENNReal.le_div_iff_mul_le ?_ ?_).symm <;> simpa

Result:
no goals

Proof state:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ⊤
hbt : b ≠ ⊤ ∨ c ≠ 0
this : a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
⊢ a / b ≤ c ↔ a ≤ c * b

Tactic:
simpa [div_eq_mul_inv]

Result:
no goals

Proof state:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ⊤
hbt : b ≠ ⊤ ∨ c ≠ 0
⊢ a / b ≤ c ↔ a ≤ c * b

Tactic:
suffices a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹ by simpa [div_eq_mul_inv]

Result:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ⊤
hbt : b ≠ ⊤ ∨ c ≠ 0
⊢ a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
-- Mathlib/RingTheory/Binomial.lean
theorem smeval_ascPochhammer_int_ofNat {R} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (r : R) :
    ∀ n : ℕ, smeval (ascPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) r
  | 0 => by
    simp only [ascPochhammer_zero, smeval_one]
  | n + 1 => by
    simp only [ascPochhammer_succ_right, smeval_mul]
    rw [smeval_ascPochhammer_int_ofNat r n]
    simp only [smeval_add, smeval_X, ← C_eq_natCast, smeval_C, natCast_zsmul, nsmul_eq_mul,
      Nat.cast_id]

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℤ (n + 1)).smeval r = (ascPochhammer ℕ (n + 1)).smeval r

Tactic:
simp only [ascPochhammer_succ_right, smeval_mul]

Result:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℤ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r

Tactic:
simp only [smeval_add, smeval_X, ← C_eq_natCast, smeval_C, natCast_zsmul, nsmul_eq_mul,
  Nat.cast_id]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℤ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r

Tactic:
rw [smeval_ascPochhammer_int_ofNat r n]

Result:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
⊢ (ascPochhammer ℤ 0).smeval r = (ascPochhammer ℕ 0).smeval r

Tactic:
simp only [ascPochhammer_zero, smeval_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem not_mem_range_self {n : Nat} : n ∉ range n

Proof state:
n : Nat
⊢ ¬n ∈ range n

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_congr [LawfulBEq α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
    get m a h' = get m b ((mem_congr h hab).1 h')

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
h : m.WF
a b : α
hab : (a == b) = true
h' : a ∈ m
⊢ get m a h' = get m b ⋯

Tactic:
simp_to_raw using Raw₀.Const.get_congr

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Ideal.lean
theorem mem_ideal_span_X_image {x : MvPolynomial σ R} {s : Set σ} :
    x ∈ Ideal.span (MvPolynomial.X '' s : Set (MvPolynomial σ R)) ↔
      ∀ m ∈ x.support, ∃ i ∈ s, (m : σ →₀ ℕ) i ≠ 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
have := @mem_ideal_span_monomial_image σ R _ x ((fun i => Finsupp.single i 1) '' s)

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun s => (monomial s) 1) '' ((fun i => Finsupp.single i 1) '' s)) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun s => (monomial s) 1) '' ((fun i => Finsupp.single i 1) '' s)) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
rw [Set.image_image] at this

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi
⊢ (∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
simp [Nat.one_le_iff_ne_zero]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
refine this.trans ?_

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi
⊢ (∀ xi ∈ x.support, ∃ si ∈ (fun i => Finsupp.single i 1) '' s, si ≤ xi) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_sub_sin : sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2) :=
  ofReal_injective <| by simp [sin_sub_sin]

Proof state:
x y : ℝ
⊢ ↑(sin x - sin y) = ↑(2 * sin ((x - y) / 2) * cos ((x + y) / 2))

Tactic:
simp [sin_sub_sin]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem measurable_join : Measurable (join : Measure (Measure α) → Measure α) :=
  measurable_of_measurable_coe _ fun s hs => by
    simp only [join_apply hs]; exact measurable_lintegral (measurable_coe hs)

Proof state:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => b.join s

Tactic:
simp only [join_apply hs]

Result:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (μ : Measure α), μ s ∂b

Proof state:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (μ : Measure α), μ s ∂b

Tactic:
exact measurable_lintegral (measurable_coe hs)

Result:
no goals