harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem isEquiv_valuation_valuationSubring : v.IsEquiv v.valuationSubring.valuation

Proof state:
K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : K
⊢ v x ≤ 1 ↔ v.valuationSubring.valuation x ≤ 1

Tactic:
rw [ValuationSubring.valuation_le_one_iff]

Result:
K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : K
⊢ v x ≤ 1 ↔ x ∈ v.valuationSubring

Proof state:
K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.IsEquiv v.valuationSubring.valuation

Tactic:
rw [isEquiv_iff_val_le_one]

Result:
K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ ∀ {x : K}, v x ≤ 1 ↔ v.valuationSubring.valuation x ≤ 1

Proof state:
K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ ∀ {x : K}, v x ≤ 1 ↔ v.valuationSubring.valuation x ≤ 1

Tactic:
intro x

Result:
K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : K
⊢ v x ≤ 1 ↔ v.valuationSubring.valuation x ≤ 1

Proof state:
K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : K
⊢ v x ≤ 1 ↔ x ∈ v.valuationSubring

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem rescale_mk (f : ℕ → R) (a : R) : rescale a (mk f) = mk fun n : ℕ => a ^ n * f n

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
⊢ (rescale a) (mk f) = mk fun n => a ^ n * f n

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
n✝ : ℕ
⊢ (coeff R n✝) ((rescale a) (mk f)) = (coeff R n✝) (mk fun n => a ^ n * f n)

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
n✝ : ℕ
⊢ (coeff R n✝) ((rescale a) (mk f)) = (coeff R n✝) (mk fun n => a ^ n * f n)

Tactic:
rw [coeff_rescale, coeff_mk, coeff_mk]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
/-- `ofTensorProduct` is functorial in `M`. -/
lemma ofTensorProduct_naturality (f : M →ₗ[R] N) :
    map I f ∘ₗ ofTensorProduct I M =
      ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f

Proof state:
case a.h.h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
x✝ : M
n✝ : ℕ
⊢ ↑(((AlgebraTensorModule.curry (map I f ∘ₗ ofTensorProduct I M)) 1) x✝) n✝ =
    ↑(((AlgebraTensorModule.curry (ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f)) 1) x✝) n✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ map I f ∘ₗ ofTensorProduct I M = ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f

Tactic:
ext

Result:
case a.h.h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
x✝ : M
n✝ : ℕ
⊢ ↑(((AlgebraTensorModule.curry (map I f ∘ₗ ofTensorProduct I M)) 1) x✝) n✝ =
    ↑(((AlgebraTensorModule.curry (ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f)) 1) x✝) n✝
-- Mathlib/Data/Matroid/Closure.lean
lemma ext_closure {M₁ M₂ : Matroid α} (h : ∀ X, M₁.closure X = M₂.closure X) : M₁ = M₂ :=
  ext_indep (by simpa using h univ)
    (fun _ _ ↦ by simp_rw [indep_iff_forall_closure_diff_ne, h])

Proof state:
α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
x✝¹ : Set α
x✝ : x✝¹ ⊆ M₁.E
⊢ M₁.Indep x✝¹ ↔ M₂.Indep x✝¹

Tactic:
simp_rw [indep_iff_forall_closure_diff_ne, h]

Result:
no goals

Proof state:
α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
⊢ M₁.E = M₂.E

Tactic:
simpa using h univ

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem coeFn_negPart (f : Lp ℝ p μ) : ∀ᵐ a ∂μ, negPart f a = -min (f a) 0 :=
  (coeFn_negPart_eq_max f).mono fun a h => by rw [h, ← max_neg_neg, neg_zero]

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h : ↑↑(negPart f) a = -↑↑f a ⊔ 0
⊢ ↑↑(negPart f) a = -(↑↑f a ⊓ 0)

Tactic:
rw [h, ← max_neg_neg, neg_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.Multiset.stronglyMeasurable_prod (s : Multiset (α → M))
    (hs : ∀ f ∈ s, StronglyMeasurable f) :
    StronglyMeasurable fun x => (s.map fun f : α → M => f x).prod

Proof state:
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
s : Multiset (α → M)
hs : ∀ f ∈ s, StronglyMeasurable f
⊢ StronglyMeasurable fun x => (Multiset.map (fun f => f x) s).prod

Tactic:
simpa only [← Pi.multiset_prod_apply] using s.stronglyMeasurable_prod' hs

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem chartAt_subtype_val_symm_eventuallyEq (U : Opens M) {x : U} :
    (chartAt H x.val).symm =ᶠ[𝓝 (chartAt H x.val x.val)] Subtype.val ∘ (chartAt H x).symm

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U : Opens M
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)
⊢ ↑e.symm =ᶠ[𝓝 (↑e ↑x)] Subtype.val ∘ ↑(chartAt H x).symm

Tactic:
exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn ⟨x⟩)

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U : Opens M
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)

Tactic:
apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds

Result:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U : Opens M
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ ↑e ↑x ∈ (e.subtypeRestr ⋯).target

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U : Opens M
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ ↑e ↑x ∈ (e.subtypeRestr ⋯).target

Tactic:
exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U : Opens M
x : ↥U
⊢ ↑(chartAt H ↑x).symm =ᶠ[𝓝 (↑(chartAt H ↑x) ↑x)] Subtype.val ∘ ↑(chartAt H x).symm

Tactic:
set e := chartAt H x.val

Result:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U : Opens M
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ ↑e.symm =ᶠ[𝓝 (↑e ↑x)] Subtype.val ∘ ↑(chartAt H x).symm

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U : Opens M
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ ↑e.symm =ᶠ[𝓝 (↑e ↑x)] Subtype.val ∘ ↑(chartAt H x).symm

Tactic:
have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
  apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
  exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

Result:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U : Opens M
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)
⊢ ↑e.symm =ᶠ[𝓝 (↑e ↑x)] Subtype.val ∘ ↑(chartAt H x).symm
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem integrable_coeFn (f : α →₁[μ] β) : Integrable f μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ Integrable (↑↑f) μ

Tactic:
rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ MemLp (↑↑f) 1 μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ MemLp (↑↑f) 1 μ

Tactic:
exact Lp.memLp f

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousOn.isOpen_preimage {t : Set β} (h : ContinuousOn f s)
    (hs : IsOpen s) (hp : f ⁻¹' t ⊆ s) (ht : IsOpen t) : IsOpen (f ⁻¹' t)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen s
hp : f ⁻¹' t ⊆ s
ht : IsOpen t
⊢ IsOpen (f ⁻¹' t)

Tactic:
convert (continuousOn_open_iff hs).mp h t ht

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen s
hp : f ⁻¹' t ⊆ s
ht : IsOpen t
⊢ f ⁻¹' t = s ∩ f ⁻¹' t

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen s
hp : f ⁻¹' t ⊆ s
ht : IsOpen t
⊢ f ⁻¹' t = s ∩ f ⁻¹' t

Tactic:
rw [inter_comm, inter_eq_self_of_subset_left hp]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDF.iInf_rat_gt_eq (hf : IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ b ∂(ν a), ∀ q, ⨅ r : Ioi q, f (a, b) r = f (a, b) q

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
⊢ ∀ᵐ (b : β) ∂ν a, ∀ (q : ℚ), ⨅ r, f (a, b) ↑r = f (a, b) q

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.iInf_rat_gt_eq

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Pairwise.lean
theorem pairwise_append {as bs : Array α} :
    (as ++ bs).Pairwise R ↔ as.Pairwise R ∧ bs.Pairwise R ∧ (∀ x ∈ as, ∀ y ∈ bs, R x y)

Proof state:
α : Type u_1
R : α → α → Prop
as bs : Array α
⊢ List.Pairwise R (as ++ bs).toList ↔
    List.Pairwise R as.toList ∧ List.Pairwise R bs.toList ∧ ∀ (x : α), x ∈ as → ∀ (y : α), y ∈ bs → R x y

Tactic:
simp [← mem_toList, toList_append, ← List.pairwise_append]

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
as bs : Array α
⊢ Pairwise R (as ++ bs) ↔ Pairwise R as ∧ Pairwise R bs ∧ ∀ (x : α), x ∈ as → ∀ (y : α), y ∈ bs → R x y

Tactic:
unfold Pairwise

Result:
α : Type u_1
R : α → α → Prop
as bs : Array α
⊢ List.Pairwise R (as ++ bs).toList ↔
    List.Pairwise R as.toList ∧ List.Pairwise R bs.toList ∧ ∀ (x : α), x ∈ as → ∀ (y : α), y ∈ bs → R x y
-- Mathlib/Data/NNRat/Defs.lean
theorem toNNRat_pos : 0 < toNNRat q ↔ 0 < q

Proof state:
q : ℚ
⊢ 0 < q.toNNRat ↔ 0 < q

Tactic:
simp [toNNRat, ← coe_lt_coe]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Decomposition.lean
theorem decompose_coe {i : ι} (x : ℳ i) : decompose ℳ (x : M) = DirectSum.of _ i x

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ (decompose ℳ) ↑x = (of (fun i => ↥(ℳ i)) i) x

Tactic:
rw [← decompose_symm_of _, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_insertListConst_le [BEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} :
    (insertListConst l toInsert).length ≤ l.length + toInsert.length

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (insertList l (List.map Prod.toSigma toInsert)).length ≤ l.length + (List.map Prod.toSigma toInsert).length

Tactic:
apply length_insertList_le

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (insertList l (List.map Prod.toSigma toInsert)).length ≤ l.length + toInsert.length

Tactic:
rw [← List.length_map toInsert Prod.toSigma]

Result:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (insertList l (List.map Prod.toSigma toInsert)).length ≤ l.length + (List.map Prod.toSigma toInsert).length

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (insertListConst l toInsert).length ≤ l.length + toInsert.length

Tactic:
unfold insertListConst

Result:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (insertList l (List.map Prod.toSigma toInsert)).length ≤ l.length + toInsert.length
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isGE_swap {o : Ordering} : o.swap.isGE = o.isLE

Proof state:
o : Ordering
⊢ o.swap.isGE = o.isLE

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Data/Rat/Cast/CharZero.lean
theorem cast_mk (a b : ℤ) : (a /. b : α) = a / b

Proof state:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a b : ℤ
⊢ ↑(a /. b) = ↑a / ↑b

Tactic:
simp only [divInt_eq_div, cast_div, cast_intCast]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem comp_isOpenMap_iff (h : X ≃ₜ Y) {f : Z → X} : IsOpenMap (h ∘ f) ↔ IsOpenMap f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap (⇑h.symm ∘ ⇑h ∘ f)

Tactic:
exact h.symm.isOpenMap.comp hf

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
⊢ IsOpenMap (⇑h ∘ f) → IsOpenMap f

Tactic:
intro hf

Result:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
⊢ IsOpenMap (⇑h ∘ f) ↔ IsOpenMap f

Tactic:
refine ⟨?_, fun hf => h.isOpenMap.comp hf⟩

Result:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
⊢ IsOpenMap (⇑h ∘ f) → IsOpenMap f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap f

Tactic:
rw [← Function.id_comp f, ← h.symm_comp_self, Function.comp_assoc]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap (⇑h.symm ∘ ⇑h ∘ f)
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
theorem trace_zero (h : j ≠ i) : trace (stdBasisMatrix i j c) = 0

Proof state:
n : Type u_10
α : Type u_12
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : AddCommMonoid α
i j : n
c : α
h : j ≠ i
⊢ (stdBasisMatrix i j c).trace = 0

Tactic:
simp [trace, -diag_apply, h]

Result:
no goals
-- Mathlib/Algebra/Prime/Defs.lean
theorem Prime.irreducible (hp : Prime p) : Irreducible p :=
  ⟨hp.not_unit, fun a b ↦ by
    rintro rfl
    exact (hp.dvd_or_dvd dvd_rfl).symm.imp
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_right <| right_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_right · _)
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_left <| left_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_left · _)⟩

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b : M
⊢ p = a * b → IsUnit a ∨ IsUnit b

Tactic:
rintro rfl

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
a b : M
hp : Prime (a * b)
⊢ IsUnit a ∨ IsUnit b
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropOn_symm_of_mem_maximalAtlas [HasGroupoid M G] (hG : G.LocalInvariantProp G Q)
    (hQ : ∀ y, Q id univ y) (he : e ∈ maximalAtlas M G) : LiftPropOn Q e.symm e.target

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : H
hx : x ∈ e.target
⊢ e.target ∈ 𝓝 x

Tactic:
exact e.open_target.mem_nhds hx

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
⊢ LiftPropOn Q (↑e.symm) e.target

Tactic:
intro x hx

Result:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : H
hx : x ∈ e.target
⊢ LiftPropWithinAt Q (↑e.symm) e.target x

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : H
hx : x ∈ e.target
⊢ LiftPropWithinAt Q (↑e.symm) e.target x

Tactic:
apply hG.liftPropWithinAt_of_liftPropAt_of_mem_nhds
  (hG.liftPropAt_symm_of_mem_maximalAtlas hQ he hx)

Result:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : H
hx : x ∈ e.target
⊢ e.target ∈ 𝓝 x
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc (attr := simp)] lemma w₀₂_τ₁ : S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0

Tactic:
rw [← comp_τ₁, S.w₀₂, zero_τ₁]

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem index (H : Subgroup G) [H.FiniteIndex] : ∃ n : ℕ, H.index = p ^ n

Proof state:
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : H.FiniteIndex
n : ℕ
hn : Nat.card (G ⧸ H.normalCore) = p ^ n
⊢ ∃ n, H.index = p ^ n

Tactic:
obtain ⟨k, _, hk2⟩ :=
  (Nat.dvd_prime_pow hp.out).mp
    ((congr_arg _ (H.normalCore.index_eq_card.trans hn)).mp
      (Subgroup.index_dvd_of_le H.normalCore_le))

Result:
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : H.FiniteIndex
n : ℕ
hn : Nat.card (G ⧸ H.normalCore) = p ^ n
k : ℕ
left✝ : k ≤ n
hk2 : H.index = p ^ k
⊢ ∃ n, H.index = p ^ n

Proof state:
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : H.FiniteIndex
n : ℕ
hn : Nat.card (G ⧸ H.normalCore) = p ^ n
k : ℕ
left✝ : k ≤ n
hk2 : H.index = p ^ k
⊢ ∃ n, H.index = p ^ n

Tactic:
exact ⟨k, hk2⟩

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : H.FiniteIndex
⊢ ∃ n, H.index = p ^ n

Tactic:
obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normalCore)

Result:
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : H.FiniteIndex
n : ℕ
hn : Nat.card (G ⧸ H.normalCore) = p ^ n
⊢ ∃ n, H.index = p ^ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem le_of_lt_or_eq : ∀ {x y : Bool}, x < y ∨ x = y → x ≤ y

Proof state:
⊢ ∀ {x y : Bool}, x < y ∨ x = y → x ≤ y

Tactic:
decide

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem stereographic_apply_neg (v : sphere (0 : E) 1) :
    stereographic (norm_eq_of_mem_sphere v) (-v) = 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ ↑(stereographic ⋯) (-v) = 0

Tactic:
simp [stereographic_apply, orthogonalProjection_orthogonalComplement_singleton_eq_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Spec.lean
theorem Spec_Γ_naturality {R S : CommRingCat.{u}} (f : R ⟶ S) :
    f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op

Proof state:
R S : CommRingCat
f : R ⟶ S
⊢ f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op

Tactic:
ext : 2

Result:
case hf.a
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
⊢ (CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝ =
    (CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝

Proof state:
case hf.a
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
⊢ (CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝ =
    (CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝

Tactic:
refine Subtype.ext <| funext fun x' => ?_

Result:
case hf.a
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x' =
    ↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝) x'

Proof state:
case hf.a
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ ↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝) x' =
    ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x'

Tactic:
apply Localization.localRingHom_to_map

Result:
no goals

Proof state:
case hf.a
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x' =
    ↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝) x'

Tactic:
symm

Result:
case hf.a
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ ↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝) x' =
    ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x'
-- Mathlib/Data/Countable/Defs.lean
theorem uncountable_iff_forall_not_surjective [Nonempty α] :
    Uncountable α ↔ ∀ f : ℕ → α, ¬Surjective f

Proof state:
α : Sort u
inst✝ : Nonempty α
⊢ Uncountable α ↔ ∀ (f : ℕ → α), ¬Surjective f

Tactic:
rw [← not_countable_iff, countable_iff_exists_surjective, not_exists]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
lemma mem_of_mem_measurableAtom {x y : β} (h : y ∈ measurableAtom x) {s : Set β}
    (hs : MeasurableSet s) (hxs : x ∈ s) : y ∈ s

Proof state:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
h : ∀ (i : Set β), x ∈ i → MeasurableSet i → y ∈ i
⊢ y ∈ s

Tactic:
exact h s hxs hs

Result:
no goals

Proof state:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
h : y ∈ measurableAtom x
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
⊢ y ∈ s

Tactic:
simp only [measurableAtom, mem_iInter] at h

Result:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
h : ∀ (i : Set β), x ∈ i → MeasurableSet i → y ∈ i
⊢ y ∈ s
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem FinitePlace.norm_le_one (x : 𝓞 (WithVal (v.valuation K))) : ‖embedding v x‖ ≤ 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ ‖(embedding v) ↑x‖ ≤ 1

Tactic:
rw [norm_def', NNReal.coe_le_one, toNNReal_le_one_iff (one_lt_absNorm_nnreal v)]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ (valuation K v) ↑x ≤ 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ (valuation K v) ↑x ≤ 1

Tactic:
exact valuation_le_one v x

Result:
no goals