harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} :
    ⟦go aig input, assign⟧ = ⟦aig.mkGate input, assign⟧

Proof state:
case h_2.h_5
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝³ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝³ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝² x✝¹ : Decl α
linv✝ rinv✝ : Bool
heq✝² : aig.decls[input.lhs.ref.gate] = Decl.const true
heq✝¹ : input.lhs.inv = false
heq✝ : input.rhs.inv = false
x✝ : aig.decls[input.rhs.ref.gate] = Decl.const false → False
⊢ ⟦assign,
      { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ },
        ref := { gate := input.rhs.ref.gate, hgate := ⋯ } }⟧ =
    ⟦assign, aig.mkGate input⟧

Tactic:
next heq _ _ _ =>
simp_all [denote_idx_const heq]

Result:
no goals

Proof state:
case h_2.h_9.isFalse.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝¹⁰ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝⁹ x✝⁸ : Decl α
linv✝ rinv✝ : Bool
x✝⁷ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = true → False
x✝⁶ : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = false → False
x✝⁵ : aig.decls[input.rhs.ref.gate] = Decl.const true → input.rhs.inv = true → False
x✝⁴ : aig.decls[input.rhs.ref.gate] = Decl.const false → input.rhs.inv = false → False
x✝³ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = false → input.rhs.inv = false → False
x✝² : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = true → input.rhs.inv = false → False
x✝¹ : aig.decls[input.rhs.ref.gate] = Decl.const true → input.lhs.inv = false → input.rhs.inv = false → False
x✝ : aig.decls[input.rhs.ref.gate] = Decl.const false → input.lhs.inv = false → input.rhs.inv = true → False
h✝¹ : ¬(input.lhs.ref.gate == input.rhs.ref.gate && input.lhs.inv == false && input.rhs.inv == false) = true
h✝ : ¬(input.lhs.ref.gate == input.rhs.ref.gate && input.lhs.inv == !input.rhs.inv) = true
⊢ ⟦assign,
      {
        aig :=
          { decls := aig.decls.push (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
            cache :=
              Cache.insert aig.decls aig.cache
                (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
            invariant := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } }⟧ =
    ⟦assign, aig.mkGate input⟧

Tactic:
simp [mkGate, denote]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem finset_inf_coe {ι} (s : Finset ι) (p : ι → Submodule R M) :
    (↑(s.inf p) : Set M) = ⋂ i ∈ s, ↑(p i)

Proof state:
case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(∅.inf p) = ⋂ i ∈ ∅, ↑(p i)

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑((insert i s).inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Tactic:
rw [Finset.inf_insert, inf_coe, ih]

Result:
case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑(p i) ∩ ⋂ i ∈ s, ↑(p i) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
⊢ ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)

Tactic:
letI := Classical.decEq ι

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)

Proof state:
case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑(p i) ∩ ⋂ i ∈ s, ↑(p i) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)

Tactic:
refine s.induction_on ?_ fun i s _ ih ↦ ?_

Result:
case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(∅.inf p) = ⋂ i ∈ ∅, ↑(p i)

case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑((insert i s).inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_map : (map f p).vars ⊆ p.vars

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
⊢ ((map f) p).vars ⊆ p.vars

Tactic:
classical simp [vars_def, Multiset.subset_of_le degrees_map_le]

Result:
no goals

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
⊢ ((map f) p).vars ⊆ p.vars

Tactic:
simp [vars_def, Multiset.subset_of_le degrees_map_le]

Result:
no goals
-- Mathlib/Analysis/Fourier/Inversion.lean
lemma tendsto_integral_gaussian_smul' (hf : Integrable f) {v : V} (h'f : ContinuousAt f v) :
    Tendsto (fun (c : ℝ) ↦
      ∫ w : V, ((π * c : ℂ) ^ (finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * c * ‖v - w‖ ^ 2)) • f w)
    atTop (𝓝 (f v))

Proof state:
case h'φ
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
⊢ π ^ (↑(finrank ℝ V) / 2 + (↑1 - ↑2) * (↑(finrank ℝ V) / 2)) = 1

Tactic:
ring_nf

Result:
case h'φ
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
⊢ π ^ 0 = 1

Proof state:
case h.e'_3.h
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w => π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun k =>
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x => x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w => π ^ 2 * ‖w‖ ^ 2) k)
    (cobounded V) (𝓝 0)
x : V
⊢ ‖x‖ ^ ↑(finrank ℝ V) * π ^ (↑(finrank ℝ V) / 2) * rexp (-(π ^ ↑2 * ‖x‖ ^ ↑2)) =
    π ^ (-↑(finrank ℝ V) / 2) * (π ^ ↑2 * ‖x‖ ^ ↑2) ^ (↑(finrank ℝ V) / 2) * rexp (-(π ^ ↑2 * ‖x‖ ^ ↑2))

Tactic:
congr 1

Result:
case h.e'_3.h.e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w => π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun k =>
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x => x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w => π ^ 2 * ‖w‖ ^ 2) k)
    (cobounded V) (𝓝 0)
x : V
⊢ ‖x‖ ^ ↑(finrank ℝ V) * π ^ (↑(finrank ℝ V) / 2) =
    π ^ (-↑(finrank ℝ V) / 2) * (π ^ ↑2 * ‖x‖ ^ ↑2) ^ (↑(finrank ℝ V) / 2)
-- Mathlib/Topology/Algebra/IsOpenUnits.lean
/-- If `R` has the `I`-adic topology where `I` is contained in the jacobson radical
(e.g. when `R` is complete or local), then `Rˣ` is an open subspace of `R`. -/
lemma IsOpenUnits.of_isAdic {R : Type*} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    {I : Ideal R}
    (hR : IsAdic I) (hI : I ≤ Ideal.jacobson ⊥) :
    IsOpenUnits R

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
⊢ 𝓝 1 ≤
    Filter.map (⇑(Units.coeHom R))
      (Filter.comap (⇑(Units.embedProduct R)) (𝓝 ((Units.embedProduct R) 1).1 ×ˢ 𝓝 ((Units.embedProduct R) 1).2))

Tactic:
simp only [Units.embedProduct_apply, Units.val_one, inv_one, MulOpposite.op_one,
  Prod.mk_one_one, Prod.fst_one, Prod.snd_one]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
⊢ 𝓝 1 ≤ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H✝ : (𝓝 1).HasBasis (fun _n => True) fun n => (fun y => 1 + y) '' ↑(I ^ n)
this :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i => True) fun i =>
    ((fun x => -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' ((fun x => -1 + x) ⁻¹' ↑(I ^ i.2)))
n₁ n₂ : ℕ
H : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
u : Rˣ
h₁ : -1 + ↑u ∈ I ^ (n₁ ⊔ n₂ ⊔ 1)
h₂ : -1 + ↑u⁻¹ ∈ I ^ (n₁ ⊔ n₂ ⊔ 1)
⊢ n₂ ≤ n₁ ⊔ n₂ ⊔ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive]
lemma prod_le_prod_of_rel_le (h : s.Rel (· ≤ ·) t) : s.prod ≤ t.prod

Proof state:
case cons
α : Type u_2
inst✝ : OrderedCommMonoid α
s t : Multiset α
a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x1 x2 => x1 ≤ x2) as✝ bs✝
rt : as✝.prod ≤ bs✝.prod
⊢ (a✝¹ ::ₘ as✝).prod ≤ (b✝ ::ₘ bs✝).prod

Tactic:
rw [prod_cons, prod_cons]

Result:
case cons
α : Type u_2
inst✝ : OrderedCommMonoid α
s t : Multiset α
a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x1 x2 => x1 ≤ x2) as✝ bs✝
rt : as✝.prod ≤ bs✝.prod
⊢ a✝¹ * as✝.prod ≤ b✝ * bs✝.prod

Proof state:
case zero
α : Type u_2
inst✝ : OrderedCommMonoid α
s t : Multiset α
⊢ prod 0 ≤ prod 0

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_2
inst✝ : OrderedCommMonoid α
s t : Multiset α
a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x1 x2 => x1 ≤ x2) as✝ bs✝
rt : as✝.prod ≤ bs✝.prod
⊢ a✝¹ * as✝.prod ≤ b✝ * bs✝.prod

Tactic:
exact mul_le_mul' rh rt

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OrderedCommMonoid α
s t : Multiset α
h : Rel (fun x1 x2 => x1 ≤ x2) s t
⊢ s.prod ≤ t.prod

Tactic:
induction h with
| zero => rfl
| cons rh _ rt =>
  rw [prod_cons, prod_cons]
  exact mul_le_mul' rh rt

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
@[continuity]
lemma continuous_sumCoeffsExp : Continuous (fun (p : ℝ) => ∑ i, a i * (b i) ^ p)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : i ∈ univ
⊢ Continuous (HPow.hPow (b i))

Tactic:
exact Continuous.rpow continuous_const continuous_id (fun x => Or.inl (ne_of_gt (R.b_pos i)))

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Continuous fun p => ∑ i : α, a i * b i ^ p

Tactic:
refine continuous_finset_sum Finset.univ fun i _ => Continuous.mul (by continuity) ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : i ∈ univ
⊢ Continuous (HPow.hPow (b i))

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : i ∈ univ
⊢ Continuous fun p => a i

Tactic:
continuity

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem Minpoly.toAdjoin.surjective : Function.Surjective (Minpoly.toAdjoin R x)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ adjoin R (Subtype.val ⁻¹' {x}) ≤ (toAdjoin R x).range

Tactic:
exact adjoin_le fun ⟨y₁, y₂⟩ h ↦ ⟨mk (minpoly R x) X, by simpa [toAdjoin] using h.symm⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
x✝ : ↥(adjoin R {x})
y₁ : S
y₂ : y₁ ∈ adjoin R {x}
h : ⟨y₁, y₂⟩ ∈ Subtype.val ⁻¹' {x}
⊢ (toAdjoin R x).toRingHom ((mk (minpoly R x)) X) = ⟨y₁, y₂⟩

Tactic:
simpa [toAdjoin] using h.symm

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Function.Surjective ⇑(toAdjoin R x)

Tactic:
rw [← AlgHom.range_eq_top, _root_.eq_top_iff, ← adjoin_adjoin_coe_preimage]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ adjoin R (Subtype.val ⁻¹' {x}) ≤ (toAdjoin R x).range
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem tendsto_mul_log_one_plus_div_atTop (t : ℝ) :
    Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)

Proof state:
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)

Tactic:
have h₂ : Tendsto (fun x : ℝ => x⁻¹) atTop (𝓝[≠] 0) :=
  tendsto_inv_atTop_nhdsGT_zero.mono_right (nhdsGT_le_nhdsNE _)

Result:
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t)
h₂ : Tendsto (fun x => x⁻¹) atTop (𝓝[≠] 0)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)

Proof state:
t : ℝ
⊢ Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t)

Tactic:
simpa [hasDerivAt_iff_tendsto_slope, slope_fun_def] using
  (((hasDerivAt_id (0 : ℝ)).const_mul t).const_add 1).log (by simp)

Result:
no goals

Proof state:
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t)
h₂ : Tendsto (fun x => x⁻¹) atTop (𝓝[≠] 0)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)

Tactic:
simpa only [Function.comp_def, inv_inv] using h₁.comp h₂

Result:
no goals

Proof state:
t : ℝ
⊢ 1 + t * id 0 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
t : ℝ
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)

Tactic:
have h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t) := by
  simpa [hasDerivAt_iff_tendsto_slope, slope_fun_def] using
    (((hasDerivAt_id (0 : ℝ)).const_mul t).const_add 1).log (by simp)

Result:
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
-- Mathlib/RingTheory/Localization/Defs.lean
theorem map_eq_zero_iff (r : R) : algebraMap R S r = 0 ↔ ∃ m : M, ↑m * r = 0

Proof state:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
⊢ (∃ m, ↑m * r = 0) → (algebraMap R S) r = 0

Tactic:
rintro ⟨m, hm⟩

Result:
case mpr.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
m : ↥M
hm : ↑m * r = 0
⊢ (algebraMap R S) r = 0

Proof state:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
⊢ (algebraMap R S) r = 0 → ∃ m, ↑m * r = 0

Tactic:
intro h

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
h : (algebraMap R S) r = 0
⊢ ∃ m, ↑m * r = 0

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
⊢ (algebraMap R S) r = 0 ↔ ∃ m, ↑m * r = 0

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
⊢ (algebraMap R S) r = 0 → ∃ m, ↑m * r = 0

case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
⊢ (∃ m, ↑m * r = 0) → (algebraMap R S) r = 0

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
h : (algebraMap R S) r = 0
m : ↥M
hm : ↑m * 0 = ↑m * r
⊢ ↑m * r = 0

Tactic:
simpa using hm.symm

Result:
no goals

Proof state:
case mpr.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
m : ↥M
hm : ↑m * r = 0
⊢ (algebraMap R S) r = 0

Tactic:
rw [← (IsLocalization.map_units S m).mul_right_inj, mul_zero, ← RingHom.map_mul, hm,
  RingHom.map_zero]

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
h : (algebraMap R S) r = 0
⊢ ∃ m, ↑m * r = 0

Tactic:
obtain ⟨m, hm⟩ := (IsLocalization.eq_iff_exists M S).mp ((algebraMap R S).map_zero.trans h.symm)

Result:
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
h : (algebraMap R S) r = 0
m : ↥M
hm : ↑m * 0 = ↑m * r
⊢ ∃ m, ↑m * r = 0

Proof state:
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
h : (algebraMap R S) r = 0
m : ↥M
hm : ↑m * 0 = ↑m * r
⊢ ∃ m, ↑m * r = 0

Tactic:
exact ⟨m, by simpa using hm.symm⟩

Result:
no goals
-- Mathlib/Analysis/Complex/Conformal.lean
theorem DifferentiableAt.conformalAt (h : DifferentiableAt ℂ f z) (hf' : deriv f z ≠ 0) :
    ConformalAt f z

Proof state:
case nonzero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ fderiv ℂ f z ≠ 0

Tactic:
simpa only [Ne, ContinuousLinearMap.ext_ring_iff]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ ConformalAt f z

Tactic:
rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))

Tactic:
apply isConformalMap_complex_linear

Result:
case nonzero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ fderiv ℂ f z ≠ 0
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem isClosed_Ioc_iff {a b : α} : IsClosed (Set.Ioc a b) ↔ b ≤ a

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioc a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
exact this hab.le

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioc a b)
hab : a < b
this : closure (Ioc a b) = Ioc a b
⊢ False

Tactic:
rw [closure_Ioc hab.ne, Icc_eq_Ioc_same_iff] at this

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioc a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioc a b)
hab : a < b
⊢ False

Tactic:
have := h.closure_eq

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioc a b)
hab : a < b
this : closure (Ioc a b) = Ioc a b
⊢ False

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsClosed (Ioc a b)

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed (Ioc a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_lt fun hab => ?_, by simp_all⟩

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioc a b)
hab : a < b
⊢ False