harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_erase_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
    (m.erase k).1.size ≤ m.1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
⊢ (m.erase k).val.size ≤ m.val.size

Tactic:
simp_to_model [erase] using List.length_eraseKey_le

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem fundamentalFrontier_smul [Group H] [MulAction H α] [SMulCommClass H G α] (g : H) :
    fundamentalFrontier G (g • s) = g • fundamentalFrontier G s

Proof state:
G : Type u_1
H : Type u_2
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
s : Set α
inst✝² : Group H
inst✝¹ : MulAction H α
inst✝ : SMulCommClass H G α
g : H
⊢ fundamentalFrontier G (g • s) = g • fundamentalFrontier G s

Tactic:
simp_rw [fundamentalFrontier, smul_set_inter, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]

Result:
no goals
-- Mathlib/Topology/Connected/LocallyConnected.lean
lemma Topology.IsOpenEmbedding.locallyConnectedSpace [LocallyConnectedSpace α] [TopologicalSpace β]
    {f : β → α} (h : IsOpenEmbedding f) : LocallyConnectedSpace β

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
⊢ (Filter.comap f (𝓝 (f x))).HasBasis ((fun x s => (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) x)
    ((fun x s => f ⁻¹' s) x)

Tactic:
exact LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
  (h.isOpen_range.mem_nhds <| mem_range_self _) |>.comap _

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
⊢ LocallyConnectedSpace β

Tactic:
refine locallyConnectedSpace_of_connected_bases (fun _ s ↦ f ⁻¹' s)
  (fun x s ↦ (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) (fun x ↦ ?_)
  (fun x s hxs ↦ hxs.1.2.2.isPreconnected.preimage_of_isOpenMap h.injective h.isOpenMap hxs.2)

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
⊢ (𝓝 x).HasBasis ((fun x s => (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) x) ((fun x s => f ⁻¹' s) x)

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
⊢ (𝓝 x).HasBasis ((fun x s => (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) x) ((fun x s => f ⁻¹' s) x)

Tactic:
rw [h.nhds_eq_comap]

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
⊢ (Filter.comap f (𝓝 (f x))).HasBasis ((fun x s => (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) x)
    ((fun x s => f ⁻¹' s) x)
-- Mathlib/Data/Rel.lean
theorem image_eq_dom_of_codomain_subset {s : Set β} (h : r.codom ⊆ s) : r.preimage s = r.dom

Proof state:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
⊢ r.preimage s ⊆ r.preimage Set.univ

Tactic:
exact image_subset _ (Set.subset_univ _)

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
⊢ r.preimage Set.univ ⊆ r.preimage s

Tactic:
intro x hx

Result:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
x : α
hx : x ∈ r.preimage Set.univ
⊢ x ∈ r.preimage s

Proof state:
case a.intro
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
x : α
y : β
ryx : r x y
⊢ x ∈ r.preimage s

Tactic:
have hy : y ∈ s := h ⟨x, ryx⟩

Result:
case a.intro
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
x : α
y : β
ryx : r x y
hy : y ∈ s
⊢ x ∈ r.preimage s

Proof state:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
x : α
hx : ∃ y, r x y
⊢ x ∈ r.preimage s

Tactic:
rcases hx with ⟨y, ryx⟩

Result:
case a.intro
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
x : α
y : β
ryx : r x y
⊢ x ∈ r.preimage s

Proof state:
case a.intro
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
x : α
y : β
ryx : r x y
hy : y ∈ s
⊢ x ∈ r.preimage s

Tactic:
exact ⟨y, ⟨hy, ryx⟩⟩

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
x : α
hx : x ∈ r.preimage Set.univ
⊢ x ∈ r.preimage s

Tactic:
simp only [mem_preimage, Set.mem_univ, true_and] at hx

Result:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
x : α
hx : ∃ y, r x y
⊢ x ∈ r.preimage s

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
⊢ r.preimage s = r.dom

Tactic:
rw [← preimage_univ]

Result:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
⊢ r.preimage s = r.preimage Set.univ

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
⊢ r.preimage s = r.preimage Set.univ

Tactic:
apply Set.eq_of_subset_of_subset

Result:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
⊢ r.preimage s ⊆ r.preimage Set.univ

case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
h : r.codom ⊆ s
⊢ r.preimage Set.univ ⊆ r.preimage s
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_mono : Monotone (floor : α → ℕ) := fun a b h => by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact Nat.zero_le _
  · exact le_floor ((floor_le ha).trans h)

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a ≤ b
ha : a ≤ 0
⊢ 0 ≤ ⌊b⌋₊

Tactic:
exact Nat.zero_le _

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
exact le_floor ((floor_le ha).trans h)

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
rw [floor_of_nonpos ha]

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a ≤ b
ha : a ≤ 0
⊢ 0 ≤ ⌊b⌋₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a ≤ b
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
obtain ha | ha := le_total a 0

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
-- Mathlib/Data/Int/Order/Lemmas.lean
theorem natAbs_eq_iff_mul_self_eq {a b : ℤ} : a.natAbs = b.natAbs ↔ a * a = b * b

Proof state:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ ↑a.natAbs = ↑b.natAbs

Tactic:
exact Int.natCast_inj.symm

Result:
no goals

Proof state:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b

Tactic:
rw [← abs_eq_iff_mul_self_eq, abs_eq_natAbs, abs_eq_natAbs]

Result:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ ↑a.natAbs = ↑b.natAbs
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.tan (o.oangle x (x + y)) * ‖x‖ = ‖y‖

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)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).tan * ‖x‖ = ‖y‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero
    (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.left_ne_zero_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 x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

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 x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).tan * ‖x‖ = ‖y‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

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 x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).tan * ‖x‖ = ‖y‖
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem btw_coe_iff {x₁ x₂ x₃ : α} :
    Btw.btw (x₁ : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ↔
      toIcoMod hp'.out x₁ x₂ ≤ toIocMod hp'.out x₁ x₃

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃

Tactic:
rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_right]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem ι_range_disjoint_one :
    Disjoint (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M))
      (1 : Submodule R (ExteriorAlgebra R M))

Proof state:
case intro.intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
hx : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
h : (algebraMap R (ExteriorAlgebra R M)) r ∈ 1
⊢ (algebraMap R (ExteriorAlgebra R M)) r = 0

Tactic:
rw [ι_eq_algebraMap_iff x] at hx

Result:
case intro.intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
h : (algebraMap R (ExteriorAlgebra R M)) r ∈ 1
⊢ (algebraMap R (ExteriorAlgebra R M)) r = 0

Proof state:
case intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : ExteriorAlgebra R M
x : M
hx : (ι R) x = x✝
h : x✝ ∈ 1
⊢ x✝ = 0

Tactic:
obtain ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩ := Submodule.mem_one.mp h

Result:
case intro.intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
hx : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
h : (algebraMap R (ExteriorAlgebra R M)) r ∈ 1
⊢ (algebraMap R (ExteriorAlgebra R M)) r = 0

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Disjoint (LinearMap.range (ι R)) 1

Tactic:
rw [Submodule.disjoint_def]

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ x ∈ LinearMap.range (ι R), x ∈ 1 → x = 0

Proof state:
case intro.intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
h : (algebraMap R (ExteriorAlgebra R M)) r ∈ 1
⊢ (algebraMap R (ExteriorAlgebra R M)) r = 0

Tactic:
rw [hx.2, RingHom.map_zero]

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ x ∈ LinearMap.range (ι R), x ∈ 1 → x = 0

Tactic:
rintro _ ⟨x, hx⟩ h

Result:
case intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : ExteriorAlgebra R M
x : M
hx : (ι R) x = x✝
h : x✝ ∈ 1
⊢ x✝ = 0
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_image [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : (s.image f).Nonempty)
    (g : β → α) :
    (s.image f).sup' hs g = s.sup' hs.of_image (g ∘ f)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ s.sup ((WithBot.some ∘ g) ∘ f) = s.sup (WithBot.some ∘ g ∘ f)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ ↑((image f s).sup' hs g) = ↑(s.sup' ⋯ (g ∘ f))

Tactic:
simp only [coe_sup', sup_image, WithBot.coe_sup]

Result:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ s.sup ((WithBot.some ∘ g) ∘ f) = s.sup (WithBot.some ∘ g ∘ f)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ (image f s).sup' hs g = s.sup' ⋯ (g ∘ f)

Tactic:
rw [← WithBot.coe_eq_coe]

Result:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ ↑((image f s).sup' hs g) = ↑(s.sup' ⋯ (g ∘ f))
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem rowLens_length_ofRowLens {w : List ℕ} {hw : w.Sorted (· ≥ ·)} (hpos : ∀ x ∈ w, 0 < x) :
    (ofRowLens w hw).rowLens.length = w.length

Proof state:
w : List ℕ
hw : List.Sorted (fun x1 x2 => x1 ≥ x2) w
hpos : ∀ x ∈ w, 0 < x
⊢ ¬False ∧ ∀ n < w.length, ∃ (h : n < w.length), 0 < w[n]

Tactic:
exact ⟨not_false, fun n hn => ⟨hn, hpos _ (List.getElem_mem hn)⟩⟩

Result:
no goals

Proof state:
w : List ℕ
hw : List.Sorted (fun x1 x2 => x1 ≥ x2) w
hpos : ∀ x ∈ w, 0 < x
⊢ (ofRowLens w hw).rowLens.length = w.length

Tactic:
simp only [length_rowLens, colLen, Nat.find_eq_iff, mem_cells, mem_ofRowLens,
  lt_self_iff_false, IsEmpty.exists_iff, Classical.not_not]

Result:
w : List ℕ
hw : List.Sorted (fun x1 x2 => x1 ≥ x2) w
hpos : ∀ x ∈ w, 0 < x
⊢ ¬False ∧ ∀ n < w.length, ∃ (h : n < w.length), 0 < w[n]
-- Mathlib/RingTheory/Filtration.lean
theorem Ideal.iInf_pow_eq_bot_of_isLocalRing [IsNoetherianRing R] [IsLocalRing R] (h : I ≠ ⊤) :
    ⨅ i : ℕ, I ^ i = ⊥

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
⊢ ⨅ i, I ^ i = ⊥

Tactic:
convert I.iInf_pow_smul_eq_bot_of_isLocalRing (M := R) h

Result:
case h.e'_2.h.e'_4.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ x✝ • ⊤

Proof state:
case h.e'_2.h.e'_4.h.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
x✝ : ℕ
i : R
⊢ i ∈ I ^ x✝ ↔ i ∈ I ^ x✝ • ⊤

Tactic:
rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one]

Result:
no goals

Proof state:
case h.e'_2.h.e'_4.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ x✝ • ⊤

Tactic:
ext i

Result:
case h.e'_2.h.e'_4.h.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
x✝ : ℕ
i : R
⊢ i ∈ I ^ x✝ ↔ i ∈ I ^ x✝ • ⊤
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem T_add (m n : ℤ) : (T (m + n) : R[T;T⁻¹]) = T m * T n

Proof state:
R : Type u_1
inst✝ : Semiring R
m n : ℤ
⊢ T (m + n) = T m * T n

Tactic:
simp [T, single_mul_single]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem two_mul_sin_mul_cos (x y : ℝ) : 2 * sin x * cos y = sin (x - y) + sin (x + y)

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

Tactic:
simp [sin_add, sin_sub]

Result:
x y : ℝ
⊢ 2 * sin x * cos y = sin x * cos y + sin x * cos y

Proof state:
x y : ℝ
⊢ 2 * sin x * cos y = sin x * cos y + sin x * cos y

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
/-- If `p : X ⟶ Y` is a monomorphism that is not an isomorphism, there exists
a subobject `X'` of `Y` containing `X` (but different from `X`) such that
the inclusion `X ⟶ X'` is a pushout of a monomorphism in the family
`generatingMonomorphisms G`. -/
lemma exists_pushouts
    {X Y : C} (p : X ⟶ Y) [Mono p] (hp : ¬ IsIso p) :
    ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : (generatingMonomorphisms G).pushouts i)
      (_ : ¬ IsIso i) (_ : Mono p'), i ≫ p' = p

Proof state:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
hp : ∃ x, ∀ (x_1 : G ⟶ X), ¬x_1 ≫ p = x
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p

Tactic:
obtain ⟨f, hf⟩ := hp

Result:
case intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p

Proof state:
case intro.refine_1.intro
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : G ⟶ Y
hf : ∀ (x : G ⟶ X), ¬x ≫ p = f
h : ∀ (T : C), Function.Bijective fun x => x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
a : G ⟶ X
ha :
  (fun x => x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)) a = pushout.inr (pullback.fst p f) (pullback.snd p f)
⊢ False

Tactic:
exact hf a (by simpa using ha =≫ pushout.desc p f pullback.condition)

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
/-- Localization commutes with ranges. -/
lemma localized'_range_eq_range_localizedMap (g : M →ₗ[R] P) :
    (range g).localized' S p f' = range ((map p f f' g).extendScalarsOfIsLocalization p S) :=
  SetLike.ext (by apply SetLike.ext_iff.mp (f.range_localizedMap_eq_localized₀_range p f' g).symm)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R M
inst✝¹² : Module R N
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module S N
inst✝⁹ : IsScalarTower R S N
p : Submonoid R
inst✝⁸ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁷ : IsLocalizedModule p f
P : Type u_5
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
Q : Type u_6
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module S Q
inst✝¹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ∀ (x : Q),
    x ∈ localized' S p f' (range g) ↔ x ∈ range (extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g))

Tactic:
apply SetLike.ext_iff.mp (f.range_localizedMap_eq_localized₀_range p f' g).symm

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem finrank_add_finrank_dualCoannihilator_eq (W : Subspace K (Module.Dual K V)) :
    finrank K W + finrank K W.dualCoannihilator = finrank K V

Proof state:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K (Dual K V)
⊢ finrank K ↥W + finrank K ↥(dualCoannihilator W) = finrank K V

Tactic:
rw [finrank_dualCoannihilator_eq, finrank_add_finrank_dualAnnihilator_eq, dual_finrank_eq]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_one_sub_of_lt (h : v x < 1) : v (1 - x) = 1

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 - x) = 1

Tactic:
rw [sub_eq_add_neg 1 x]

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 + -x) = 1

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 + -x) = 1

Tactic:
simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v x < 1
⊢ v (1 - x) = 1

Tactic:
rw [← v.map_one, ← v.map_neg] at h

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 - x) = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1))

Proof state:
n i : Nat
⊢ (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1))

Tactic:
simp [range_eq_range', erase_range']

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measure_singleton (a : ℝ) : f.measure {a} = ofReal (f a - leftLim f a)

Proof state:
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ n, Ioc (u n) a
L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
⊢ Tendsto u atTop (𝓝[<] a)

Tactic:
exact
  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim
    (Eventually.of_forall fun n => u_lt_a n)

Result:
no goals

Proof state:
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
this : a ≤ x
⊢ x ∈ {a}

Tactic:
simp [le_antisymm this (hx 0).2]

Result:
no goals

Proof state:
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ n, Ioc (u n) a
L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
⊢ Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))

Tactic:
simp only [measure_Ioc]

Result:
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ n, Ioc (u n) a
L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
⊢ Tendsto (fun n => ofReal (↑f a - ↑f (u n))) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))

Proof state:
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ n, Ioc (u n) a
L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)

Tactic:
have L2 :
    Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (ofReal (f a - leftLim f a))) := by
  simp only [measure_Ioc]
  have : Tendsto (fun n => f (u n)) atTop (𝓝 (leftLim f a)) := by
    apply (f.mono.tendsto_leftLim a).comp
    exact
      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim
        (Eventually.of_forall fun n => u_lt_a n)
  exact ENNReal.continuous_ofReal.continuousAt.tendsto.comp (tendsto_const_nhds.sub this)

Result:
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ n, Ioc (u n) a
L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
L2 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem coe_affineSpan_singleton (p : P) : (affineSpan k ({p} : Set P) : Set P) = {p}

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p x : P
⊢ x -ᵥ p ∈ vectorSpan k {p} ↔ x ∈ {p}

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
⊢ ↑(affineSpan k {p}) = {p}

Tactic:
ext x

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p x : P
⊢ x ∈ ↑(affineSpan k {p}) ↔ x ∈ {p}

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p x : P
⊢ x ∈ ↑(affineSpan k {p}) ↔ x ∈ {p}

Tactic:
rw [mem_coe, ← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_singleton p)) _,
  direction_affineSpan]

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p x : P
⊢ x -ᵥ p ∈ vectorSpan k {p} ↔ x ∈ {p}