harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
theorem tendsto_pow_zero_of_constantCoeff_zero [CommSemiring R]
    {f} (hf : constantCoeff σ R f = 0) :
    Tendsto (fun n : ℕ => f ^ n) atTop (nhds 0)

Proof state:
case hf
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : (constantCoeff σ R) f = 0
⊢ IsNilpotent 0

Tactic:
exact IsNilpotent.zero

Result:
no goals

Proof state:
case hf
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : (constantCoeff σ R) f = 0
⊢ IsNilpotent ((constantCoeff σ R) f)

Tactic:
rw [hf]

Result:
case hf
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : (constantCoeff σ R) f = 0
⊢ IsNilpotent 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : (constantCoeff σ R) f = 0
⊢ Tendsto (fun n => f ^ n) atTop (nhds 0)

Tactic:
apply tendsto_pow_zero_of_constantCoeff_nilpotent

Result:
case hf
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : (constantCoeff σ R) f = 0
⊢ IsNilpotent ((constantCoeff σ R) f)
-- Mathlib/Analysis/Complex/Positivity.lean
theorem nonneg_of_iteratedDeriv_nonneg {f : ℂ → ℂ} (hf : Differentiable ℂ f) {c : ℂ}
    (h : ∀ n, 0 ≤ iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : c ≤ z) :
    0 ≤ f z

Proof state:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ ‖↑(z - c).re‖ < (↑(z - c).re).re + 1

Tactic:
simpa only [Complex.norm_of_nonneg (nonneg_iff.mp hz).1] using lt_add_one _

Result:
no goals

Proof state:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ z ∈ Metric.ball c ((z - c).re + 1)

Tactic:
rw [← sub_nonneg] at hz

Result:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ z ∈ Metric.ball c ((z - c).re + 1)

Proof state:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ z ∈ Metric.ball c ((z - c).re + 1)

Tactic:
rw [Metric.mem_ball, dist_eq, eq_re_of_ofReal_le hz]

Result:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ ‖↑(z - c).re‖ < (↑(z - c).re).re + 1

Proof state:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ 0 ≤ f z

Tactic:
refine hf.differentiableOn.nonneg_of_iteratedDeriv_nonneg (r := (z - c).re + 1) h hz ?_

Result:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ z ∈ Metric.ball c ((z - c).re + 1)
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
lemma isOpen_extend_target [I.Boundaryless] : IsOpen (f.extend I).target

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
⊢ IsOpen (f.extend I).target

Tactic:
rw [extend_target, I.range_eq_univ, inter_univ]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
⊢ IsOpen (↑I.symm ⁻¹' f.target)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
⊢ IsOpen (↑I.symm ⁻¹' f.target)

Tactic:
exact I.continuous_symm.isOpen_preimage _ f.open_target

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem isRight_iff : x.isRight ↔ ∃ y, x = Sum.inr y

Proof state:
α✝ : Type u_1
β✝ : Type u_2
x : α✝ ⊕ β✝
⊢ x.isRight = true ↔ ∃ y, x = inr y

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem map_one_eq_bot : K.map (1 : G →* N) = ⊥ :=
  eq_bot_iff.mpr <| by
    rintro x ⟨y, _, rfl⟩
    simp

Proof state:
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
⊢ map 1 K ≤ ⊥

Tactic:
rintro x ⟨y, _, rfl⟩

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
y : G
left✝ : y ∈ ↑K
⊢ 1 y ∈ ⊥

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
y : G
left✝ : y ∈ ↑K
⊢ 1 y ∈ ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.tan (o.oangle (x + y) y) * ‖y‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).tan * ‖y‖ = ‖x‖

Tactic:
exact (-o).tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).tan * ‖y‖ = ‖x‖

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).tan * ‖y‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).tan * ‖y‖ = ‖x‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).tan * ‖y‖ = ‖x‖
-- Mathlib/Computability/Primrec.lean
theorem nat_rec {f : α → β} {g : α → ℕ × β → β} (hf : Primrec f) (hg : Primrec₂ g) :
    Primrec₂ fun a (n : ℕ) => n.rec (motive := fun _ => β) (f a) fun n IH => g a (n, IH) :=
  Primrec₂.nat_iff.2 <|
    ((Nat.Primrec.casesOn' .zero <|
              (Nat.Primrec.prec hf <|
                    .comp hg <|
                      Nat.Primrec.left.pair <|
                        (Nat.Primrec.left.comp .right).pair <|
                          Nat.Primrec.pred.comp <| Nat.Primrec.right.comp .right).comp <|
                Nat.Primrec.right.pair <| Nat.Primrec.right.comp Nat.Primrec.left).comp <|
          Nat.Primrec.id.pair <| (@Primcodable.prim α).comp Nat.Primrec.left).of_eq
      fun n => by
      simp only [Nat.unpaired, id_eq, Nat.unpair_pair, decode_prod_val, decode_nat,
        Option.some_bind, Option.map_map, Option.map_some']
      rcases @decode α _ n.unpair.1 with - | a; · rfl
      simp only [Nat.pred_eq_sub_one, encode_some, Nat.succ_eq_add_one, encodek, Option.map_some',
        Option.some_bind, Option.map_map]
      induction' n.unpair.2 with m <;> simp [encodek]
      simp [*, encodek]

Proof state:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.rec 0
      (fun n_1 n_ih =>
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH =>
            encode
              (Option.map (fun p => g p.1 p.2)
                ((decode n_1).bind fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode none) =
    encode (none.bind fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2))

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Complex/LocallyUniformLimit.lean
theorem exists_cthickening_tendstoUniformlyOn (hf : TendstoLocallyUniformlyOn F f φ U)
    (hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
    ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K

Tactic:
obtain ⟨δ, hδ, hKδ⟩ := hK.exists_cthickening_subset_open hU hKU

Result:
case intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
δ : ℝ
hδ : 0 < δ
hKδ : cthickening δ K ⊆ U
⊢ ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K

Proof state:
case intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
δ : ℝ
hδ : 0 < δ
hKδ : cthickening δ K ⊆ U
⊢ ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K

Tactic:
exact ⟨δ, hδ, hKδ, tendstoUniformlyOn_deriv_of_cthickening_subset hf hF hδ hK hU hKδ⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem measure_union_lt_top_iff : μ (s ∪ t) < ∞ ↔ μ s < ∞ ∧ μ t < ∞

Proof state:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ⊤
⊢ μ t < ⊤

Tactic:
exact (measure_mono Set.subset_union_right).trans_lt h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ μ (s ∪ t) < ⊤ ↔ μ s < ⊤ ∧ μ t < ⊤

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => measure_union_lt_top h.1 h.2⟩

Result:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ⊤
⊢ μ s < ⊤

case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ⊤
⊢ μ t < ⊤

Proof state:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ⊤
⊢ μ s < ⊤

Tactic:
exact (measure_mono Set.subset_union_left).trans_lt h

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma rnDeriv_add_of_mutuallySingular (ν₁ ν₂ μ : Measure α)
    [SigmaFinite ν₁] [SigmaFinite ν₂] [SigmaFinite μ] (h : ν₂ ⟂ₘ μ) :
    (ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
h : ν₂ ⟂ₘ μ
x : α
hx_add : (ν₁ + ν₂).rnDeriv μ x = (ν₁.rnDeriv μ + ν₂.rnDeriv μ) x
hx_zero : ν₂.rnDeriv μ x = 0 x
⊢ (ν₁ + ν₂).rnDeriv μ x = ν₁.rnDeriv μ x

Tactic:
simp [hx_add, hx_zero]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
h : ν₂ ⟂ₘ μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ

Tactic:
filter_upwards [rnDeriv_add' ν₁ ν₂ μ, (rnDeriv_eq_zero ν₂ μ).mpr h] with x hx_add hx_zero

Result:
case h
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
h : ν₂ ⟂ₘ μ
x : α
hx_add : (ν₁ + ν₂).rnDeriv μ x = (ν₁.rnDeriv μ + ν₂.rnDeriv μ) x
hx_zero : ν₂.rnDeriv μ x = 0 x
⊢ (ν₁ + ν₂).rnDeriv μ x = ν₁.rnDeriv μ x
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem SL_neg_smul (g : SL(2, ℤ)) (z : ℍ) : -g • z = g • z

Proof state:
g : SL(2, ℤ)
z : ℍ
⊢ -g • z = g • z

Tactic:
simp only [coe_GLPos_neg, sl_moeb, coe_int_neg, neg_smul, coe]

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
theorem rpow_one_add_lt_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp1 : 0 < p)
    (hp2 : p < 1) : (1 + s) ^ p < 1 + p * s

Proof state:
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
⊢ 0 < 1 + p * s

Tactic:
rw [← neg_lt_iff_pos_add']

Result:
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
⊢ -1 < p * s

Proof state:
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
⊢ -1 < p * s

Tactic:
rcases lt_or_gt_of_ne hs' with h | h

Result:
case inl
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
h : s < 0
⊢ -1 < p * s

case inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
h : s > 0
⊢ -1 < p * s

Proof state:
case inr.a.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s > 0
⊢ 1 + p * s < 1 + s

Tactic:
apply add_lt_add_left (mul_lt_of_lt_one_left hs' hp2)

Result:
no goals

Proof state:
case h.e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s > 0
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

Tactic:
rw [add_sub_cancel_left, log_one, sub_zero]

Result:
no goals

Proof state:
case inr.a.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / p / s < log (1 + s) / s

Tactic:
convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1

Result:
case h.e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)

case h.e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)

case inr.a.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ 1 + s < 1 + p * s
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma homMk'_id (f : CostructuredArrow S T) : homMk' f (𝟙 f.left) = eqToHom (by aesop_cat)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : CostructuredArrow S T
⊢ mk (S.map (𝟙 f.left) ≫ f.hom) = f

Tactic:
aesop_cat

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ (f.homMk' (𝟙 f.left)).left = (eqToHom ⋯).left

Tactic:
simp [eqToHom_left]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ f.homMk' (𝟙 f.left) = eqToHom ⋯

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ (f.homMk' (𝟙 f.left)).left = (eqToHom ⋯).left
-- Mathlib/Tactic/Positivity/Core.lean
lemma nz_of_isNegNat {n : ℕ} [StrictOrderedRing A]
    (h : NormNum.IsInt e (.negOfNat n)) (w : Nat.ble 1 n = true) : (e : A) ≠ 0

Proof state:
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ e ≠ 0

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]

Result:
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ -↑n ≠ 0

Proof state:
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ ¬↑n = 0

Tactic:
apply ne_of_gt

Result:
case h
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ 0 < ↑n

Proof state:
case h
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ 0 < ↑n

Tactic:
simpa using w

Result:
no goals

Proof state:
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ -↑n ≠ 0

Tactic:
simp only [ne_eq, neg_eq_zero]

Result:
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ ¬↑n = 0
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Set.Finite.ciSup_lt_iff {s : Set ι} {f : ι → α} (hs : s.Finite)
    (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
    ⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a

Proof state:
case mpr.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
w✝ : ι
hmem : w✝ ∈ s
hx : f w✝ = ⨆ i ∈ s, f i
⊢ ⨆ i ∈ s, f i < a

Tactic:
rw [← hx]

Result:
case mpr.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
w✝ : ι
hmem : w✝ ∈ s
hx : f w✝ = ⨆ i ∈ s, f i
⊢ f w✝ < a

Proof state:
case mpr.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
w✝ : ι
hmem : w✝ ∈ s
hx : f w✝ = ⨆ i ∈ s, f i
⊢ f w✝ < a

Tactic:
exact H _ hmem

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a

Tactic:
constructor

Result:
case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i < a → ∀ x ∈ s, f x < a

case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a

Proof state:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
this : ⨆ i ∈ s, f i ∈ f '' s
⊢ ⨆ i ∈ s, f i < a

Tactic:
simp only [mem_image] at this

Result:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
H : ∀ x ∈ s, f x < a
this : ∃ x ∈ s, f x = ⨆ i ∈ s, f i
⊢ ⨆ i ∈ s, f i < a

Proof state:
case pos
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝¹ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
h✝ : x ∈ s
hx : f x = a✝
⊢ a✝ = sSup ∅ ∨ ∃ x ∈ s, f x = a✝

Tactic:
exact Or.inr ⟨_, by assumption, hx⟩

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
theorem subset_support_tsub [DecidableEq ι] {f1 f2 : ι →₀ α} :
    f1.support \ f2.support ⊆ (f1 - f2).support

Proof state:
ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : DecidableEq ι
f1 f2 : ι →₀ α
⊢ f1.support \ f2.support ⊆ (f1 - f2).support

Tactic:
simp +contextual [subset_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mker_prod_map {M' : Type*} {N' : Type*} [MulOneClass M'] [MulOneClass N'] (f : M →* N)
    (g : M' →* N') : mker (prodMap f g) = f.mker.prod (mker g)

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ mker (f.prodMap g) = (mker f).prod (mker g)

Tactic:
rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_bot]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem left_hom_inv_right [IsIso sq] : sq.left ≫ g.hom ≫ inv sq.right = f.hom

Proof state:
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.left ≫ g.hom ≫ inv sq.right = f.hom

Tactic:
simp only [← Category.assoc, IsIso.comp_inv_eq, w]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_eq_one : a * b = 1 ↔ a = 1 ∧ b = 1 :=
  ⟨fun h => ⟨RightCancelMonoid.eq_one_of_mul_right h, RightCancelMonoid.eq_one_of_mul_left h⟩, by
    rintro ⟨rfl, rfl⟩
    exact mul_one _⟩

Proof state:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1

Proof state:
case intro
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1

Tactic:
exact mul_one _

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem embDomain_eq_mapDomain (f : α ↪ β) (v : α →₀ M) : embDomain f v = mapDomain f v

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

Tactic:
by_cases h : a ∈ Set.range f

Result:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∈ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

Proof state:
case pos.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : α
⊢ (embDomain f v) (f a) = (mapDomain (⇑f) v) (f a)

Tactic:
rw [mapDomain_apply f.injective, embDomain_apply]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∈ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

Tactic:
rcases h with ⟨a, rfl⟩

Result:
case pos.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : α
⊢ (embDomain f v) (f a) = (mapDomain (⇑f) v) (f a)

Proof state:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

Tactic:
rw [mapDomain_notin_range, embDomain_notin_range] <;> assumption

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ embDomain f v = mapDomain (⇑f) v

Tactic:
ext a

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem prev_nil : ∀ {it}, ValidFor [] r it → ValidFor [] r it.prev
  | it, h => by
    simp only [Iterator.prev, h.toString, List.reverseAux_nil, h.pos, utf8Len_nil,
      Pos.mk_zero, prev_zero]
    constructor

Proof state:
r : List Char
it : Iterator
h : ValidFor [] r it
⊢ ValidFor [] r { s := { data := r }, i := 0 }

Tactic:
constructor

Result:
no goals

Proof state:
r : List Char
it : Iterator
h : ValidFor [] r it
⊢ ValidFor [] r it.prev

Tactic:
simp only [Iterator.prev, h.toString, List.reverseAux_nil, h.pos, utf8Len_nil,
  Pos.mk_zero, prev_zero]

Result:
r : List Char
it : Iterator
h : ValidFor [] r it
⊢ ValidFor [] r { s := { data := r }, i := 0 }