harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/ModEq.lean
/-- Cancel left multiplication in the modulus.

For cancelling left multiplication on both sides of the `≡`, see `nat.modeq.mul_left_cancel'`. -/
lemma of_mul_left (m : ℕ) (h : a ≡ b [MOD m * n]) : a ≡ b [MOD n]

Proof state:
n a b m : ℕ
h : ↑(m * n) ∣ ↑b - ↑a
⊢ ↑n ∣ ↑b - ↑a

Tactic:
exact (dvd_mul_left (n : ℤ) (m : ℤ)).trans h

Result:
no goals

Proof state:
n a b m : ℕ
h : a ≡ b [MOD m * n]
⊢ a ≡ b [MOD n]

Tactic:
rw [modEq_iff_dvd] at *

Result:
n a b m : ℕ
h : ↑(m * n) ∣ ↑b - ↑a
⊢ ↑n ∣ ↑b - ↑a
-- Mathlib/CategoryTheory/Equivalence.lean
theorem changeFunctor_trans (e : C ≌ D) {G G' : C ⥤ D} (iso₁ : e.functor ≅ G) (iso₂ : G ≅ G') :
    (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
G G' : C ⥤ D
iso₁ : e.functor ≅ G
iso₂ : G ≅ G'
⊢ (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem other_spec' [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : s(a, Mem.other' h) = z

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ s(a, Mem.other' h) = z

Tactic:
induction z

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ s(x✝, y✝)
⊢ s(a, Mem.other' h) = s(x✝, y✝)

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ s(x✝, y✝)
h' : a = x✝ ∨ a = y✝
⊢ s(a, Mem.other' h) = s(x✝, y✝)

Tactic:
aesop (add norm unfold [Sym2.rec, Quot.rec]) (rule_sets := [Sym2])

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ s(x✝, y✝)
⊢ s(a, Mem.other' h) = s(x✝, y✝)

Tactic:
have h' := mem_iff.mp h

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ s(x✝, y✝)
h' : a = x✝ ∨ a = y✝
⊢ s(a, Mem.other' h) = s(x✝, y✝)
-- Mathlib/Condensed/Light/Basic.lean
@[ext]
lemma hom_ext {X Y : LightCondensed.{u} C} (f g : X ⟶ Y) (h : ∀ S, f.val.app S = g.val.app S) :
    f = g

Proof state:
case h
C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.val.app S = g.val.app S
⊢ f.val = g.val

Tactic:
ext

Result:
case h.w.h
C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.val.app S = g.val.app S
x✝ : LightProfiniteᵒᵖ
⊢ f.val.app x✝ = g.val.app x✝

Proof state:
case h.w.h
C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.val.app S = g.val.app S
x✝ : LightProfiniteᵒᵖ
⊢ f.val.app x✝ = g.val.app x✝

Tactic:
exact h _

Result:
no goals

Proof state:
C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.val.app S = g.val.app S
⊢ f = g

Tactic:
apply Sheaf.hom_ext

Result:
case h
C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.val.app S = g.val.app S
⊢ f.val = g.val
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_range_le_card {ι : Type*} [Fintype ι] (b : ι → M) :
    (Set.range b).finrank R ≤ Fintype.card ι

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ (Finset.image b Finset.univ).card ≤ Fintype.card ι

Tactic:
exact Finset.card_image_le

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ (range b).toFinset.card ≤ Fintype.card ι

Tactic:
rw [Set.toFinset_range]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ (Finset.image b Finset.univ).card ≤ Fintype.card ι

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ Set.finrank R (range b) ≤ Fintype.card ι

Tactic:
classical
refine (finrank_span_le_card _).trans ?_
rw [Set.toFinset_range]
exact Finset.card_image_le

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ Set.finrank R (range b) ≤ Fintype.card ι

Tactic:
refine (finrank_span_le_card _).trans ?_

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ (range b).toFinset.card ≤ Fintype.card ι
-- Mathlib/Algebra/GroupWithZero/Semiconj.lean
theorem div_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
    SemiconjBy a (x / x') (y / y')

Proof state:
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x / x') (y / y')

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Result:
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)

Proof state:
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)

Tactic:
exact h.mul_right h'.inv_right₀

Result:
no goals
-- Mathlib/Order/GameAdd.lean
theorem GameAdd.fst_snd {a₁ a₂ b : α} (h : rα a₁ a₂) : GameAdd rα s(a₁, b) s(b, a₂)

Proof state:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(b, a₂)

Tactic:
rw [Sym2.eq_swap]

Result:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(b, a₁) s(b, a₂)

Proof state:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(b, a₁) s(b, a₂)

Tactic:
exact GameAdd.snd h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem imp_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a → b) = True

Proof state:
a b : Prop
h : a = False
⊢ (a → b) = True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
lemma _root_.range_mem_nhds_isInteriorPoint {x : M} (h : I.IsInteriorPoint x) :
    range I ∈ 𝓝 (extChartAt I x x)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
h : I.IsInteriorPoint x
⊢ range ↑I ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
rw [mem_nhds_iff]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
h : I.IsInteriorPoint x
⊢ ∃ t ⊆ range ↑I, IsOpen t ∧ ↑(extChartAt I x) x ∈ t

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
h : I.IsInteriorPoint x
⊢ ∃ t ⊆ range ↑I, IsOpen t ∧ ↑(extChartAt I x) x ∈ t

Tactic:
exact ⟨interior (range I), interior_subset, isOpen_interior, h⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
lemma setLIntegral_withDensity_eq_lintegral_mul₀' {μ : Measure α} {f : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) {g : α → ℝ≥0∞} (hg : AEMeasurable g (μ.withDensity f))
    {s : Set α} (hs : MeasurableSet s) :
    ∫⁻ a in s, g a ∂μ.withDensity f = ∫⁻ a in s, (f * g) a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable g ((μ.restrict s).withDensity f)

Tactic:
rw [← restrict_withDensity hs]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable g ((μ.withDensity f).restrict s)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable g ((μ.withDensity f).restrict s)

Tactic:
exact hg.restrict

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul₀' hf.restrict]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable g ((μ.restrict s).withDensity f)
-- Mathlib/Data/Rel.lean
theorem preimage_eq_core (f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).core s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = (Function.graph f).core s

Tactic:
simp [Set.preimage, Rel.core]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem IsOpenMap.piMap {Y : ι → Type*} [∀ i, TopologicalSpace (Y i)] {f : ∀ i, π i → Y i}
    (hfo : ∀ i, IsOpenMap (f i)) (hsurj : ∀ᶠ i in cofinite, Surjective (f i)) :
    IsOpenMap (Pi.map f)

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
Y : ι → Type u_8
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → π i → Y i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → π i
⊢ (Filter.pi fun i => 𝓝 (Pi.map f x i)) ≤ Filter.pi fun i => map (f i) (𝓝 (x i))

Tactic:
exact Filter.pi_mono fun i ↦ (hfo i).nhds_le _

Result:
no goals

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
Y : ι → Type u_8
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → π i → Y i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → π i
⊢ 𝓝 (Pi.map f x) ≤ map (Pi.map f) (𝓝 x)

Tactic:
rw [nhds_pi, nhds_pi, map_piMap_pi hsurj]

Result:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
Y : ι → Type u_8
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → π i → Y i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → π i
⊢ (Filter.pi fun i => 𝓝 (Pi.map f x i)) ≤ Filter.pi fun i => map (f i) (𝓝 (x i))

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
Y : ι → Type u_8
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → π i → Y i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
⊢ IsOpenMap (Pi.map f)

Tactic:
refine IsOpenMap.of_nhds_le fun x ↦ ?_

Result:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
Y : ι → Type u_8
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → π i → Y i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → π i
⊢ 𝓝 (Pi.map f x) ≤ map (Pi.map f) (𝓝 x)
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ici_succ_eq_Ioi_of_not_isMax (ha : ¬ IsMax a) : Ici (succ a) = Ioi a

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a

Tactic:
rw [mem_Ici, mem_Ioi, succ_le_iff_of_not_isMax ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Ici (succ a) = Ioi a

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem bind₁_xInTermsOfW_wittPolynomial [Invertible (p : R)] (k : ℕ) :
    bind₁ (xInTermsOfW p R) (W_ R k) = X k

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x ∈ range (k + 1), C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k

Tactic:
rw [sum_range_succ_comm, tsub_self, pow_zero, pow_one, bind₁_X_right, mul_comm, ← C_pow,
  xInTermsOfW_aux]

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ X k - ∑ i ∈ range k, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (k - i) +
      ∑ x ∈ range k, C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) =
    X k

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ X k - ∑ i ∈ range k, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (k - i) +
      ∑ x ∈ range k, C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) =
    X k

Tactic:
simp only [Nat.cast_pow, C_pow, bind₁_X_right, sub_add_cancel]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ (bind₁ (xInTermsOfW p R)) (W_ R k) = X k

Tactic:
rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum]

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x ∈ range (k + 1), (bind₁ (xInTermsOfW p R)) (C (↑p ^ x) * X x ^ p ^ (k - x)) = X k

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x ∈ range (k + 1), (bind₁ (xInTermsOfW p R)) (C (↑p ^ x) * X x ^ p ^ (k - x)) = X k

Tactic:
simp only [Nat.cast_pow, map_pow, C_pow, map_mul, algHom_C, algebraMap_eq]

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x ∈ range (k + 1), C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k
-- Mathlib/RingTheory/Artinian/Module.lean
theorem eventually_isCompl_ker_pow_range_pow [IsNoetherian R M] (f : M →ₗ[R] M) :
    ∀ᶠ n in atTop, IsCompl (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : Disjoint (ker (f ^ n)) (range (f ^ n)) ∧ Codisjoint (ker (f ^ n)) (range (f ^ n))
⊢ IsCompl (ker (f ^ n)) (range (f ^ n))

Tactic:
simpa only [isCompl_iff]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
⊢ ∀ᶠ (n : ℕ) in atTop, IsCompl (ker (f ^ n)) (range (f ^ n))

Tactic:
filter_upwards [f.eventually_disjoint_ker_pow_range_pow.and
  f.eventually_codisjoint_ker_pow_range_pow] with n hn

Result:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : Disjoint (ker (f ^ n)) (range (f ^ n)) ∧ Codisjoint (ker (f ^ n)) (range (f ^ n))
⊢ IsCompl (ker (f ^ n)) (range (f ^ n))
-- Mathlib/Data/Real/ConjExponents.lean
lemma div_conj_eq_sub_one : p / q = p - 1

Proof state:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ p / q = p - 1

Tactic:
field_simp [h.symm.ne_zero]

Result:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ p = (p - 1) * q

Proof state:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ p = (p - 1) * q

Tactic:
rw [h.sub_one_mul_conj]

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem primaryComponent.exists_orderOf_eq_prime_pow (g : CommMonoid.primaryComponent G p) :
    ∃ n : ℕ, orderOf g = p ^ n

Proof state:
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ ∃ n, orderOf g = p ^ n

Tactic:
obtain ⟨_, hn⟩ := g.property

Result:
case intro
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
w✝ : ℕ
hn : orderOf ↑g = p ^ w✝
⊢ ∃ n, orderOf g = p ^ n

Proof state:
case intro
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
w✝ : ℕ
hn : orderOf ↑g = p ^ w✝
⊢ ∃ n, orderOf g = p ^ n

Tactic:
rw [orderOf_submonoid g] at hn

Result:
case intro
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
w✝ : ℕ
hn : orderOf g = p ^ w✝
⊢ ∃ n, orderOf g = p ^ n

Proof state:
case intro
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
w✝ : ℕ
hn : orderOf g = p ^ w✝
⊢ ∃ n, orderOf g = p ^ n

Tactic:
exact ⟨_, hn⟩

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem exists_mem_map {f : α → β} {o : Option α} {p : β → Prop} :
    (∃ y ∈ o.map f, p y) ↔ ∃ x ∈ o, p (f x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
o : Option α
p : β → Prop
⊢ (∃ y, y ∈ Option.map f o ∧ p y) ↔ ∃ x, x ∈ o ∧ p (f x)

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
/-- The boundary is the complement of the interior. -/
lemma compl_interior : (I.interior M)ᶜ = I.boundary M

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ ModelWithCorners.interior M ⊓ ModelWithCorners.boundary M = ⊥

Tactic:
exact disjoint_iff_inter_eq_empty.mp I.disjoint_interior_boundary

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ (ModelWithCorners.interior M)ᶜ = ModelWithCorners.boundary M

Tactic:
apply compl_unique ?_ I.interior_union_boundary_eq_univ

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ ModelWithCorners.interior M ⊓ ModelWithCorners.boundary M = ⊥
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Iic_of_intervalIntegral_norm_bounded (I b : ℝ)
    (hfi : ∀ i, IntegrableOn f (Ioc (a i) b) μ) (ha : Tendsto a l atBot)
    (h : ∀ᶠ i in l, (∫ x in a i..b, ‖f x‖ ∂μ) ≤ I) : IntegrableOn f (Iic b) μ

Proof state:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a : ι → ℝ
f : ℝ → E
I b : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun i => Ioi (a i)
⊢ ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))

Tactic:
intro i

Result:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a : ι → ℝ
f : ℝ → E
I b : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun i => Ioi (a i)
i : ι
⊢ IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
-- Mathlib/Combinatorics/Schnirelmann.lean
@[simp] lemma schnirelmannDensity_univ : schnirelmannDensity Set.univ = 1 :=
  (schnirelmannDensity_eq_one_iff_of_zero_mem (by simp)).2 (by simp)

Proof state:
⊢ 0 ∈ Set.univ

Tactic:
simp

Result:
no goals

Proof state:
⊢ Set.univ = Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem dropLast_eq_dropLastTR : @dropLast = @dropLastTR

Proof state:
⊢ @dropLast = @dropLastTR

Tactic:
funext α l

Result:
case h.h
α : Type u_1
l : List α
⊢ l.dropLast = l.dropLastTR

Proof state:
case h.h
α : Type u_1
l : List α
⊢ l.dropLast = l.dropLastTR

Tactic:
simp [dropLastTR]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `mul_inv_le_iff₀'` for a version with multiplication on the other side. -/
lemma mul_inv_le_iff₀ (hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ a * c where
  mp h

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hc : 0 < c
h : b * c⁻¹ ≤ a
⊢ b ≤ a * c

Tactic:
simpa [hc.ne'] using mul_le_mul_of_nonneg_right h hc.le

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hc : 0 < c
h : b ≤ a * c
⊢ b * c⁻¹ ≤ a

Tactic:
simpa [hc.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg.2 hc.le)

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_natCast (n : ℕ) : birthday n = n

Proof state:
n : ℕ
⊢ (toGame ↑n).birthday = ↑n

Tactic:
exact birthday_ordinalToGame _

Result:
no goals

Proof state:
n : ℕ
⊢ (↑n).birthday = ↑n

Tactic:
rw [← toGame_natCast]

Result:
n : ℕ
⊢ (toGame ↑n).birthday = ↑n
-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem fderivWithin_comp₃ {g' : G → G'} {g : F → G} {t : Set F} {u : Set G} {y : F} {y' : G}
    (hg' : DifferentiableWithinAt 𝕜 g' u y') (hg : DifferentiableWithinAt 𝕜 g t y)
    (hf : DifferentiableWithinAt 𝕜 f s x) (h2g : MapsTo g t u) (h2f : MapsTo f s t) (h3g : g y = y')
    (h3f : f x = y) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (g' ∘ g ∘ f) s x =
      (fderivWithin 𝕜 g' u y').comp ((fderivWithin 𝕜 g t y).comp (fderivWithin 𝕜 f s 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
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : E → F
x : E
s : Set E
g' : G → G'
g : F → G
t : Set F
u : Set G
hf : DifferentiableWithinAt 𝕜 f s x
h2g : MapsTo g t u
h2f : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
hg' : DifferentiableWithinAt 𝕜 g' u (g (f x))
⊢ fderivWithin 𝕜 (g' ∘ g ∘ f) s x =
    (fderivWithin 𝕜 g' u (g (f x))).comp ((fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x))

Tactic:
exact (hg'.hasFDerivWithinAt.comp x (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h2f) <|
  h2g.comp h2f).fderivWithin hxs

Result:
no goals

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
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : E → F
x : E
s : Set E
g' : G → G'
g : F → G
t : Set F
u : Set G
y : F
y' : G
hg' : DifferentiableWithinAt 𝕜 g' u y'
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h2g : MapsTo g t u
h2f : MapsTo f s t
h3g : g y = y'
h3f : f x = y
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (g' ∘ g ∘ f) s x = (fderivWithin 𝕜 g' u y').comp ((fderivWithin 𝕜 g t y).comp (fderivWithin 𝕜 f s x))

Tactic:
substs h3g h3f

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
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : E → F
x : E
s : Set E
g' : G → G'
g : F → G
t : Set F
u : Set G
hf : DifferentiableWithinAt 𝕜 f s x
h2g : MapsTo g t u
h2f : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
hg' : DifferentiableWithinAt 𝕜 g' u (g (f x))
⊢ fderivWithin 𝕜 (g' ∘ g ∘ f) s x =
    (fderivWithin 𝕜 g' u (g (f x))).comp ((fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x))