harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_eq_zero_iff : count s = 0 ↔ s = ∅ where
  mp h := eq_empty_of_forall_not_mem fun x hx ↦ by
    simpa [hx] using ((ENNReal.le_tsum x).trans <| le_sum_apply _ _).trans_eq h
  mpr

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
h : count s = 0
x : α
hx : x ∈ s
⊢ False

Tactic:
simpa [hx] using ((ENNReal.le_tsum x).trans <| le_sum_apply _ _).trans_eq h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
⊢ count ∅ = 0

Tactic:
exact measure_empty

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ s = ∅ → count s = 0

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : MeasurableSpace α
⊢ count ∅ = 0
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle (p₁ p₂ p₃ : P) :
    dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ -
      2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (∠ p₁ p₂ p₃)

Proof state:
case h.e'_2.h.e'_5.h.e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

Tactic:
exact (vsub_sub_vsub_cancel_right p₁ p₃ p₂).symm

Result:
no goals

Proof state:
case h.e'_2.h.e'_6.h.e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

Tactic:
exact (vsub_sub_vsub_cancel_right p₁ p₃ p₂).symm

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
p₁ p₂ p₃ : P
⊢ dist p₁ p₃ * dist p₁ p₃ =
    dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ - 2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (∠ p₁ p₂ p₃)

Tactic:
rw [dist_eq_norm_vsub V p₁ p₃, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₃ p₂]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ - 2 * ‖p₁ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ * Real.cos (∠ 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
p₁ p₂ p₃ : P
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ - 2 * ‖p₁ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ * Real.cos (∠ p₁ p₂ p₃)

Tactic:
unfold angle

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ -
      2 * ‖p₁ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ * Real.cos (InnerProductGeometry.angle (p₁ -ᵥ 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
p₁ p₂ p₃ : P
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ -
      2 * ‖p₁ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ * Real.cos (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))

Tactic:
convert norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle
  (p₁ -ᵥ p₂ : V) (p₃ -ᵥ p₂ : V)

Result:
case h.e'_2.h.e'_5.h.e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

case h.e'_2.h.e'_6.h.e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)
-- Mathlib/Data/Set/Lattice.lean
theorem image2_eq_iUnion (s : Set α) (t : Set β) : image2 f s t = ⋃ (i ∈ s) (j ∈ t), {f i j}

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
-- Mathlib/Data/PNat/Basic.lean
theorem mod_add_div (m k : ℕ+) : (mod m k + k * div m k : ℕ) = m

Proof state:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this✝ : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
this : ↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).1 + ↑k * (k.modDivAux (↑m % ↑k) (↑m / ↑k)).2 = ↑m % ↑k + ↑k * (↑m / ↑k)
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
exact this.trans h₀

Result:
no goals

Proof state:
case intro
m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False

Tactic:
exact (m.ne_zero h₀.symm).elim

Result:
no goals

Proof state:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
have : ¬((m : ℕ) % (k : ℕ) = 0 ∧ (m : ℕ) / (k : ℕ) = 0) := by
  rintro ⟨hr, hq⟩
  rw [hr, hq, mul_zero, zero_add] at h₀
  exact (m.ne_zero h₀.symm).elim

Result:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Proof state:
case intro
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False

Tactic:
rw [hr, hq, mul_zero, zero_add] at h₀

Result:
case intro
m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False

Proof state:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)

Tactic:
rintro ⟨hr, hq⟩

Result:
case intro
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False

Proof state:
m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
let h₀ := Nat.mod_add_div (m : ℕ) (k : ℕ)

Result:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Proof state:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
have := modDivAux_spec k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ)) this

Result:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this✝ : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
this : ↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).1 + ↑k * (k.modDivAux (↑m % ↑k) (↑m / ↑k)).2 = ↑m % ↑k + ↑k * (↑m / ↑k)
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m
-- Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
theorem differentiableWithinAtProp_self_source {f : E → H'} {s : Set E} {x : E} :
    DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 (I' ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 (↑I' ∘ f) s x

Tactic:
simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
  modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem Int.isCoprime_iff_gcd_eq_one {m n : ℤ} : IsCoprime m n ↔ Int.gcd m n = 1

Proof state:
case mp
m n : ℤ
⊢ IsCoprime m n → m.gcd n = 1

Tactic:
rintro ⟨a, b, h⟩

Result:
case mp.intro.intro
m n a b : ℤ
h : a * m + b * n = 1
⊢ m.gcd n = 1

Proof state:
m n : ℤ
⊢ IsCoprime m n ↔ m.gcd n = 1

Tactic:
constructor

Result:
case mp
m n : ℤ
⊢ IsCoprime m n → m.gcd n = 1

case mpr
m n : ℤ
⊢ m.gcd n = 1 → IsCoprime m n

Proof state:
case mp.intro.intro
m n a b : ℤ
h : a * m + b * n = 1
⊢ m.gcd n = 1

Tactic:
refine Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, ?_⟩)

Result:
case mp.intro.intro
m n a b : ℤ
h : a * m + b * n = 1
⊢ ↑1 = m * a + n * b

Proof state:
case mpr
m n : ℤ
⊢ m.gcdA n * m + m.gcdB n * n = 1 → ∃ a b, a * m + b * n = 1

Tactic:
intro h

Result:
case mpr
m n : ℤ
h : m.gcdA n * m + m.gcdB n * n = 1
⊢ ∃ a b, a * m + b * n = 1

Proof state:
case mpr
m n : ℤ
⊢ m.gcd n = 1 → IsCoprime m n

Tactic:
rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]

Result:
case mpr
m n : ℤ
⊢ m.gcdA n * m + m.gcdB n * n = 1 → ∃ a b, a * m + b * n = 1

Proof state:
case mp.intro.intro
m n a b : ℤ
h : a * m + b * n = 1
⊢ ↑1 = m * a + n * b

Tactic:
rwa [mul_comm m, mul_comm n, eq_comm]

Result:
no goals

Proof state:
case mpr
m n : ℤ
h : m.gcdA n * m + m.gcdB n * n = 1
⊢ ∃ a b, a * m + b * n = 1

Tactic:
exact ⟨_, _, h⟩

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem mk_d_2_1 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (if 2 = 1 + 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁

Tactic:
rw [if_pos rfl, Category.id_comp]

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁

Tactic:
change ite (2 = 1 + 1) (𝟙 X₂ ≫ d₁) 0 = d₁

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (if 2 = 1 + 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
-- Mathlib/Algebra/FreeMonoid/Count.lean
theorem countP_of (x : α) : countP p (of x) = if p x then 1 else 0

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (countP p) (of x) = if p x then 1 else 0

Tactic:
rw [countP_apply, toList_of, List.countP_singleton]

Result:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then 1 else 0) = if p x then 1 else 0

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then 1 else 0) = if p x then 1 else 0

Tactic:
simp only [decide_eq_true_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
  | 0, _, _ => by simp
  | _, _, [] => by simp
  | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..

Proof state:
α : Type u_1
x✝¹ : Nat
x✝ : List α
⊢ take x✝¹ (drop 0 x✝) = drop 0 (take (0 + x✝¹) x✝)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x✝¹ x✝ : Nat
⊢ take x✝ (drop x✝¹ []) = drop x✝¹ (take (x✝¹ + x✝) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n✝ x✝ : Nat
head✝ : α
tail✝ : List α
⊢ take x✝ (drop (n✝ + 1) (head✝ :: tail✝)) = drop (n✝ + 1) (take (n✝ + 1 + x✝) (head✝ :: tail✝))

Tactic:
simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma add_coe_eq_bot_iff : x + b = ⊥ ↔ x = ⊥

Proof state:
α : Type u
inst✝ : Add α
x : WithBot α
b : α
⊢ x + ↑b = ⊥ ↔ x = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
/-- The `eval` map is surjective at `x`. -/
lemma smoothSheaf.eval_surjective (x : M) : Function.Surjective (smoothSheaf.eval IM I N x)

Proof state:
case w
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace HM M
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H N
x : M
⊢ ∀ (t : N), ∃ U f, ∃ (_ : (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯).pred f), f ⟨x, ⋯⟩ = t

Tactic:
intro n

Result:
case w
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace HM M
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H N
x : M
n : N
⊢ ∃ U f, ∃ (_ : (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯).pred f), f ⟨x, ⋯⟩ = n

Proof state:
case w
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace HM M
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H N
x : M
n : N
⊢ ∃ U f, ∃ (_ : (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯).pred f), f ⟨x, ⋯⟩ = n

Tactic:
exact ⟨⊤, fun _ ↦ n, contMDiff_const, rfl⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace HM M
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H N
x : M
⊢ Function.Surjective (eval IM I N x)

Tactic:
apply TopCat.stalkToFiber_surjective

Result:
case w
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace HM M
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H N
x : M
⊢ ∀ (t : N), ∃ U f, ∃ (_ : (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯).pred f), f ⟨x, ⋯⟩ = t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} :
    (replicate n a == replicate n b) = (n == 0 || a == b)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (replicate n a == replicate n b) = (n == 0 || a == b)

Tactic:
cases n with
| zero => simp
| succ n =>
  rw [replicate_succ, replicate_succ, cons_beq_cons, replicate_beq_replicate]
  rw [Bool.eq_iff_iff]
  simp +contextual

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (a == b && (n == 0 || a == b)) = true ↔ (n + 1 == 0 || a == b) = true

Tactic:
simp +contextual

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : BEq α
a b : α
⊢ (replicate 0 a == replicate 0 b) = (0 == 0 || a == b)

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (a == b && (n == 0 || a == b)) = (n + 1 == 0 || a == b)

Tactic:
rw [Bool.eq_iff_iff]

Result:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (a == b && (n == 0 || a == b)) = true ↔ (n + 1 == 0 || a == b) = true

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (replicate (n + 1) a == replicate (n + 1) b) = (n + 1 == 0 || a == b)

Tactic:
rw [replicate_succ, replicate_succ, cons_beq_cons, replicate_beq_replicate]

Result:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (a == b && (n == 0 || a == b)) = (n + 1 == 0 || a == b)
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma map_leftHomologyMap' : F.map (ShortComplex.leftHomologyMap' φ hl₁ hl₂) =
    ShortComplex.leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
rw [γ.leftHomologyMap'_eq, (γ.map F).leftHomologyMap'_eq,
  ShortComplex.LeftHomologyMapData.map_φH]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma pentagon (Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε) :
    Pentagon Y₁ Y₂ Y₃ Y₄

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.e_a.e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫ L'.map (α_ X₁ X₂ (X₃ ⊗ X₄)).hom) ≫ (μ L W ε X₁ (X₂ ⊗ X₃ ⊗ X₄)).inv) ≫
      L'.obj X₁ ◁ ((μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ L'.obj X₂ ◁ (μ L W ε X₃ X₄).inv) =
    ((((((((L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫ (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).inv) ≫
                    L'.obj (X₁ ⊗ X₂) ◁ (μ L W ε X₃ X₄).inv) ≫
                  (μ L W ε X₁ X₂).inv ▷ (L'.obj X₃ ⊗ L'.obj X₄)) ≫
                (L'.obj X₁ ⊗ L'.obj X₂) ◁ (μ L W ε X₃ X₄).hom) ≫
              (μ L W ε X₁ X₂).hom ▷ L'.obj (X₃ ⊗ X₄)) ≫
            (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).hom) ≫
          L'.map (α_ X₁ X₂ (X₃ ⊗ X₄)).hom) ≫
        (μ L W ε X₁ (X₂ ⊗ X₃ ⊗ X₄)).inv) ≫
      L'.obj X₁ ◁ ((μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ L'.obj X₂ ◁ (μ L W ε X₃ X₄).inv)

Tactic:
congr

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.e_a.e_a.e_a.e_a.e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom =
    (((((L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫ (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).inv) ≫
              L'.obj (X₁ ⊗ X₂) ◁ (μ L W ε X₃ X₄).inv) ≫
            (μ L W ε X₁ X₂).inv ▷ (L'.obj X₃ ⊗ L'.obj X₄)) ≫
          (L'.obj X₁ ⊗ L'.obj X₂) ◁ (μ L W ε X₃ X₄).hom) ≫
        (μ L W ε X₁ X₂).hom ▷ L'.obj (X₃ ⊗ X₄)) ≫
      (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).hom
-- Mathlib/Data/NNReal/Defs.lean
theorem coe_sInf (s : Set ℝ≥0) : (↑(sInf s) : ℝ) = sInf (((↑) : ℝ≥0 → ℝ) '' s)

Proof state:
case inl

⊢ sInf ∅ = 0

Tactic:
exact @subset_sInf_emptyset ℝ (Set.Ici (0 : ℝ)) _ _ (_)

Result:
no goals

Proof state:
s : Set ℝ≥0
⊢ ↑(sInf s) = sInf (toReal '' s)

Tactic:
rcases Set.eq_empty_or_nonempty s with rfl|hs

Result:
case inl

⊢ ↑(sInf ∅) = sInf (toReal '' ∅)

case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sInf s) = sInf (toReal '' s)

Proof state:
case hs
s : Set ℝ≥0
hs : s.Nonempty
⊢ ∀ x ∈ Subtype.val '' s, 0 ≤ x

Tactic:
rintro - ⟨y, -, rfl⟩

Result:
case hs.intro.intro
s : Set ℝ≥0
hs : s.Nonempty
y : { r // 0 ≤ r }
⊢ 0 ≤ ↑y

Proof state:
case inr
s : Set ℝ≥0
hs : s.Nonempty
A : sInf (Subtype.val '' s) ∈ Set.Ici 0
⊢ ↑(sInf s) = sInf (toReal '' s)

Tactic:
exact (@subset_sInf_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs (OrderBot.bddBelow s) A).symm

Result:
no goals

Proof state:
case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sInf s) = sInf (toReal '' s)

Tactic:
have A : sInf (Subtype.val '' s) ∈ Set.Ici 0 := by
  apply Real.sInf_nonneg
  rintro - ⟨y, -, rfl⟩
  exact y.2

Result:
case inr
s : Set ℝ≥0
hs : s.Nonempty
A : sInf (Subtype.val '' s) ∈ Set.Ici 0
⊢ ↑(sInf s) = sInf (toReal '' s)

Proof state:
case inl

⊢ ↑(sInf ∅) = sInf (toReal '' ∅)

Tactic:
simp only [Set.image_empty, Real.sInf_empty, coe_eq_zero]

Result:
case inl

⊢ sInf ∅ = 0

Proof state:
s : Set ℝ≥0
hs : s.Nonempty
⊢ sInf (Subtype.val '' s) ∈ Set.Ici 0

Tactic:
apply Real.sInf_nonneg

Result:
case hs
s : Set ℝ≥0
hs : s.Nonempty
⊢ ∀ x ∈ Subtype.val '' s, 0 ≤ x

Proof state:
case hs.intro.intro
s : Set ℝ≥0
hs : s.Nonempty
y : { r // 0 ≤ r }
⊢ 0 ≤ ↑y

Tactic:
exact y.2

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem cast_le_natCast {m : ℚ} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ)

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
m : ℚ
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
rw [← cast_le (K := K), cast_natCast]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem dom_bool (f : Bool → α) : Primrec f :=
  (cond .id (const (f true)) (const (f false))).of_eq fun b => by cases b <;> rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : Bool → α
b : Bool
⊢ (bif id b then f true else f false) = f b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean
theorem map_nhds_eq_of_surj [CompleteSpace E] [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
    (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) (h : LinearMap.range f' = ⊤) :
    map f (𝓝 a) = 𝓝 (f a)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
h : LinearMap.range f' = ⊤
f'symm : f'.NonlinearRightInverse := f'.nonlinearRightInverseOfSurjective h
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
f'symm_pos : 0 < f'symm.nnnorm
cpos : 0 < c
s : Set E
s_nhds : s ∈ 𝓝 a
hs : ApproximatesLinearOn f f' s c
⊢ f'symm.nnnorm⁻¹ ≠ 0

Tactic:
simp [ne_of_gt f'symm_pos]

Result:
no goals