harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Constructible.lean
@[stacks 005B]
lemma IsRetrocompact.image_of_isEmbedding (hs : IsRetrocompact s) (hfemb : IsEmbedding f)
    (hfcomp : IsRetrocompact (range f)) : IsRetrocompact (f '' s)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (range f ∩ U)

Tactic:
exact hfcomp hUcomp hUopen

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
⊢ IsRetrocompact (f '' s)

Tactic:
rintro U hUcomp hUopen

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (f '' s ∩ U)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (s ∩ f ⁻¹' U)

Tactic:
refine hs ?_ <| hUopen.preimage hfemb.continuous

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (f ⁻¹' U)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (f ⁻¹' U)

Tactic:
rw [hfemb.isCompact_iff, image_preimage_eq_inter_range, inter_comm]

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (range f ∩ U)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (f '' s ∩ U)

Tactic:
rw [← image_inter_preimage, ← hfemb.isCompact_iff]

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (s ∩ f ⁻¹' U)
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma leadingCoeff_esymmAlgHomMonomial (t : Fin n →₀ ℕ) (hnm : n ≤ m) :
    leadingCoeff toLex (esymmAlgHomMonomial (Fin m) t r) = r

Proof state:
case ha.hD
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ Function.Injective ⇑toLex

case ha.hadd
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ ∀ (a1 a2 : Fin m →₀ ℕ), toLex (a1 + a2) = toLex a1 + toLex a2

Tactic:
exacts [toLex.injective, toLex_add]

Result:
no goals

Proof state:
case ha
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) (f✝ + fun₀ | i => b✝) r) = r

Tactic:
rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
    ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,
    ih]

Result:
case ha.hD
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ Function.Injective ⇑toLex

case ha.hadd
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ ∀ (a1 a2 : Fin m →₀ ℕ), toLex (a1 + a2) = toLex a1 + toLex a2

Proof state:
case h0
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
⊢ leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) 0 r) = r

Tactic:
rw [esymmAlgHom_zero, leadingCoeff_toLex_C]

Result:
no goals

Proof state:
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
t : Fin n →₀ ℕ
hnm : n ≤ m
⊢ leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) t r) = r

Tactic:
induction t using Finsupp.induction₂ with
| h0 => rw [esymmAlgHom_zero, leadingCoeff_toLex_C]
| ha i _ _ _ _ ih =>
  rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
      ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,
      ih]
  exacts [toLex.injective, toLex_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem LinearEquiv.det_symm_mul_det {A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) :
    LinearMap.det (f.symm : M →ₗ[A] M) * LinearMap.det (f : M →ₗ[A] M) = 1

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
f : M ≃ₗ[A] M
⊢ LinearMap.det ↑f.symm * LinearMap.det ↑f = 1

Tactic:
simp [← LinearMap.det_comp]

Result:
no goals
-- Mathlib/Topology/Order/LawsonTopology.lean
theorem isTopologicalBasis : TopologicalSpace.IsTopologicalBasis (lawsonBasis α)

Proof state:
case h.e'_2
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ lower α ⊓ scott α univ =
    induced (⇑WithLower.toLower) WithLower.instTopologicalSpace ⊓
      induced (⇑WithScott.toScott) WithScott.instTopologicalSpace

Tactic:
apply (congrArg₂ min _) _

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ lower α = induced (⇑WithLower.toLower) WithLower.instTopologicalSpace

α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2 (fun x x_1 => ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen U}
⊢ scott α univ = induced (⇑WithScott.toScott) WithScott.instTopologicalSpace
-- Mathlib/Analysis/Calculus/Conformal/InnerProduct.lean
theorem conformalAt_iff {f : E → F} {x : E} {f' : E →L[ℝ] F} (h : HasFDerivAt f f' x) :
    ConformalAt f x ↔ ∃ c : ℝ, 0 < c ∧ ∀ u v : E, ⟪f' u, f' v⟫ = c * ⟪u, v⟫

Proof state:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E → F
x : E
f' : E →L[ℝ] F
h : HasFDerivAt f f' x
⊢ ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), inner (f' u) (f' v) = c * inner u v

Tactic:
simp only [conformalAt_iff', h.fderiv]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_ofSubsingleton_id [Subsingleton ι] [Nontrivial G] (i : ι) :
    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖ = 1

Proof state:
𝕜 : Type u
ι : Type v
G : Type wG
inst✝⁵ : Fintype ι
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Subsingleton ι
inst✝ : Nontrivial G
i : ι
⊢ ‖(ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_sub (a b : α) : toIcoMod hp a (b - p) = toIcoMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (b - p) = toIcoMod hp a b

Tactic:
simpa only [one_zsmul] using toIcoMod_sub_zsmul hp a b 1

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem div_add_mod' (m k : ℕ+) : (div m k * k + mod m k : ℕ) = m

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

Tactic:
exact div_add_mod _ _

Result:
no goals

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

Tactic:
rw [mul_comm]

Result:
m k : ℕ+
⊢ ↑k * m.div k + ↑(m.mod k) = ↑m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findIdx? f = l.unattach.findIdx? g

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx? f l = findIdx? g l.unattach

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ findIdx? f { toList := toList✝ } = findIdx? g { toList := toList✝ }.unattach

Proof state:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ findIdx? f { toList := toList✝ } = findIdx? g { toList := toList✝ }.unattach

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
lemma smul_pow (r : M) (x : N) : ∀ n, (r • x) ^ n = r ^ n • x ^ n
  | 0 => by simp
  | n + 1 => by rw [pow_succ', smul_pow _ _ n, smul_mul_smul_comm, ← pow_succ', ← pow_succ']

Proof state:
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)

Tactic:
rw [pow_succ', smul_pow _ _ n, smul_mul_smul_comm, ← pow_succ', ← pow_succ']

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
⊢ (r • x) ^ 0 = r ^ 0 • x ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem isCoatom_ker_of_surjective [IsSimpleModule R N] {f : M →ₗ[R] N}
    (hf : Function.Surjective f) : IsCoatom (LinearMap.ker f)

Proof state:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ IsSimpleModule R (M ⧸ ker f)

Tactic:
exact IsSimpleModule.congr (f.quotKerEquivOfSurjective hf)

Result:
no goals

Proof state:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ IsCoatom (ker f)

Tactic:
rw [← isSimpleModule_iff_isCoatom]

Result:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ IsSimpleModule R (M ⧸ ker f)
-- Mathlib/Algebra/Group/Idempotent.lean
lemma mul_of_commute (hab : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) :
    IsIdempotentElem (a * b)

Proof state:
S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ IsIdempotentElem (a * b)

Tactic:
rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem ofAdd_multiset_prod (s : Multiset α) : ofAdd s.sum = (s.map ofAdd).prod

Proof state:
α : Type u_3
inst✝ : AddCommMonoid α
s : Multiset α
⊢ ofAdd s.sum = (Multiset.map (⇑ofAdd) s).prod

Tactic:
simp [ofAdd]

Result:
α : Type u_3
inst✝ : AddCommMonoid α
s : Multiset α
⊢ s.sum = s.prod

Proof state:
α : Type u_3
inst✝ : AddCommMonoid α
s : Multiset α
⊢ s.sum = s.prod

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdropWhile_concat_neg (x : α) (h : ¬p x) : rdropWhile p (l ++ [x]) = l ++ [x]

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rdropWhile p (l ++ [x]) = l ++ [x]

Tactic:
rw [rdropWhile_concat, if_neg h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem coe_deleteEdges_le : (G'.deleteEdges s).coe ≤ (G'.coe : SimpleGraph G'.verts)

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v w : ↑(G'.deleteEdges s).verts
⊢ (G'.deleteEdges s).coe.Adj v w → G'.coe.Adj v w

Tactic:
simp +contextual

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).coe ≤ G'.coe

Tactic:
intro v w

Result:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v w : ↑(G'.deleteEdges s).verts
⊢ (G'.deleteEdges s).coe.Adj v w → G'.coe.Adj v w
-- Mathlib/Data/Finset/Prod.lean
theorem product_eq_empty {s : Finset α} {t : Finset β} : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_product, not_and_or, not_nonempty_iff_eq_empty,
  not_nonempty_iff_eq_empty]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
/-- The standard simplex in the zero-dimensional space is empty. -/
lemma stdSimplex_of_isEmpty_index [IsEmpty ι] [Nontrivial 𝕜] : stdSimplex 𝕜 ι = ∅ :=
  eq_empty_of_forall_not_mem <| by rintro f ⟨-, hf⟩; simp at hf

Proof state:
case intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial 𝕜
f : ι → 𝕜
hf : ∑ x : ι, f x = 1
⊢ False

Tactic:
simp at hf

Result:
no goals

Proof state:
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial 𝕜
⊢ ∀ (x : ι → 𝕜), x ∉ stdSimplex 𝕜 ι

Tactic:
rintro f ⟨-, hf⟩

Result:
case intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial 𝕜
f : ι → 𝕜
hf : ∑ x : ι, f x = 1
⊢ False
-- Mathlib/Data/Set/Prod.lean
theorem prod_insert : s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
⊢ s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t

Tactic:
simp only [insert_eq, prod_union, prod_singleton]

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma isClosed_preimage_val_coborder :
    IsClosed (coborder s ↓∩ s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (coborder s ↓∩ s)

Tactic:
rw [isClosed_preimage_val, inter_eq_right.mpr subset_coborder, coborder_inter_closure]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem dist_div_cos_oangle_center_eq_two_mul_radius {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) :
    dist p₁ p₂ / Real.Angle.cos (∡ p₂ p₁ s.center) = 2 * s.radius

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = 2 * s.radius

Tactic:
rw [← dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₂ h, mul_div_cancel₀ _ (two_ne_zero' ℝ)]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurableSet_of_differentiableAt : MeasurableSet { x | DifferentiableAt 𝕜 f x }

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
f : E → F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
this : IsComplete univ
⊢ MeasurableSet {x | DifferentiableAt 𝕜 f x}

Tactic:
convert measurableSet_of_differentiableAt_of_isComplete 𝕜 f this

Result:
case h.e'_3.h.e'_2.h.a
𝕜 : 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
f : E → F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
this : IsComplete univ
x✝ : E
⊢ DifferentiableAt 𝕜 f x✝ ↔ DifferentiableAt 𝕜 f x✝ ∧ fderiv 𝕜 f x✝ ∈ univ

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
f : E → F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
⊢ MeasurableSet {x | DifferentiableAt 𝕜 f x}

Tactic:
have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ

Result:
𝕜 : 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
f : E → F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
this : IsComplete univ
⊢ MeasurableSet {x | DifferentiableAt 𝕜 f x}

Proof state:
case h.e'_3.h.e'_2.h.a
𝕜 : 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
f : E → F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
this : IsComplete univ
x✝ : E
⊢ DifferentiableAt 𝕜 f x✝ ↔ DifferentiableAt 𝕜 f x✝ ∧ fderiv 𝕜 f x✝ ∈ univ

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem length_pos_of_pos (h : 0 < n) : 0 < c.length

Proof state:
case h
n : ℕ
c : Composition n
h : 0 < n
⊢ 0 < c.blocks.sum

Tactic:
convert h

Result:
case h.e'_4
n : ℕ
c : Composition n
h : 0 < n
⊢ c.blocks.sum = n

Proof state:
case h.e'_4
n : ℕ
c : Composition n
h : 0 < n
⊢ c.blocks.sum = n

Tactic:
exact c.blocks_sum

Result:
no goals

Proof state:
n : ℕ
c : Composition n
h : 0 < n
⊢ 0 < c.length

Tactic:
apply length_pos_of_sum_pos

Result:
case h
n : ℕ
c : Composition n
h : 0 < n
⊢ 0 < c.blocks.sum
-- Mathlib/Data/Rat/Defs.lean
lemma neg_def (q : ℚ) : -q = -q.num /. q.den

Proof state:
q : ℚ
⊢ -q = -q.num /. ↑q.den

Tactic:
rw [← neg_divInt, num_divInt_den]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
lemma cauchy_inf_uniformSpace {u v : UniformSpace β} {F : Filter β} :
    Cauchy (uniformSpace := u ⊓ v) F ↔
    Cauchy (uniformSpace := u) F ∧ Cauchy (uniformSpace := v) F

Proof state:
β : Type v
u v : UniformSpace β
F : Filter β
⊢ Cauchy F ↔ Cauchy F ∧ Cauchy F

Tactic:
unfold Cauchy

Result:
β : Type v
u v : UniformSpace β
F : Filter β
⊢ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β

Proof state:
β : Type v
u v : UniformSpace β
F : Filter β
⊢ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β

Tactic:
rw [inf_uniformity (u := u), le_inf_iff, and_and_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem edges_transfer (hp) : (p.transfer H hp).edges = p.edges

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).edges = p.edges

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_smul_left (hT : DominatedFinMeasAdditive μ T C) (c : ℝ) (f : α → E) :
    setToFun μ (fun s => c • T s) (hT.smul c) f = c • setToFun μ T hT f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
⊢ setToFun μ (fun s => c • T s) ⋯ f = c • setToFun μ T hT f

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hf : Integrable f μ
⊢ setToFun μ (fun s => c • T s) ⋯ f = c • setToFun μ T hT f

case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ (fun s => c • T s) ⋯ f = c • setToFun μ T hT f

Proof state:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ (fun s => c • T s) ⋯ f = c • setToFun μ T hT f

Tactic:
simp_rw [setToFun_undef _ hf, smul_zero]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hf : Integrable f μ
⊢ setToFun μ (fun s => c • T s) ⋯ f = c • setToFun μ T hT f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left hT c]

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.mod_left (a b ab : ℕ) (r : ℤ) (hab : a % b = ab) (hr : jacobiSymNat ab b = r) :
    jacobiSymNat a b = r

Proof state:
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSymNat a b = r

Tactic:
rw [← hr, jacobiSymNat, jacobiSymNat, _root_.jacobiSym.mod_left a b, ← hab]

Result:
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSym (↑a % ↑b) b = jacobiSym (↑(a % b)) b

Proof state:
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSym (↑a % ↑b) b = jacobiSym (↑(a % b)) b

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Defs.lean
theorem one_lt_mul_self_iff : 1 < a * a ↔ 1 < a :=
  ⟨(fun h ↦ by push_neg at h ⊢; exact mul_le_one' h h).mtr, fun h ↦ one_lt_mul'' h h⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommMonoid α
a : α
h : ¬1 < a
⊢ ¬1 < a * a

Tactic:
push_neg at h ⊢

Result:
α : Type u_1
inst✝ : LinearOrderedCommMonoid α
a : α
h : a ≤ 1
⊢ a * a ≤ 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommMonoid α
a : α
h : a ≤ 1
⊢ a * a ≤ 1

Tactic:
exact mul_le_one' h h

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem discr_comp (f : (n → R) →ₗ[R] n → R) :
    (Q.comp f).discr = f.toMatrix'.det * f.toMatrix'.det * Q.discr

Proof state:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Invertible 2
Q : QuadraticMap R (n → R) R
f : (n → R) →ₗ[R] n → R
⊢ (Q.comp f).discr = (LinearMap.toMatrix' f).det * (LinearMap.toMatrix' f).det * Q.discr

Tactic:
simp only [Matrix.det_transpose, mul_left_comm, QuadraticMap.toMatrix'_comp, mul_comm,
  Matrix.det_mul, discr]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualMap_bijective_iff {f : V₁ →ₗ[K] V₂} :
    Function.Bijective f.dualMap ↔ Function.Bijective f

Proof state:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Bijective ⇑f.dualMap ↔ Function.Bijective ⇑f

Tactic:
simp_rw [Function.Bijective, dualMap_surjective_iff, dualMap_injective_iff, and_comm]

Result:
no goals