harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
theorem IsStableUnderBaseChange.mk' [RespectsIso P]
    (hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [HasPullback f g] (_ : P g),
      P (pullback.fst f g)) :
    IsStableUnderBaseChange P where
  of_isPullback {X Y Y' S f g f' g'} sq hg

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
⊢ P g'

Tactic:
let e := sq.flip.isoPullback

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P g'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
⊢ P g'

Tactic:
haveI : HasPullback f g := sq.flip.hasPullback

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
⊢ P g'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P g'

Tactic:
rw [← P.cancel_left_of_respectsIso e.inv, sq.flip.isoPullback_inv_fst]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P (pullback.fst f g)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P (pullback.fst f g)

Tactic:
exact hP₂ _ _ _ f g hg

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.le_right_of_left_le' (hf : ConvexOn 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s)
    (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hfx : f x ≤ f (a • x + b • y)) :
    f (a • x + b • y) ≤ f y

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
hfx : f x ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f y

Tactic:
rw [add_comm] at hab hfx ⊢

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : b + a = 1
hfx : f x ≤ f (b • y + a • x)
⊢ f (b • y + a • x) ≤ f y

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : b + a = 1
hfx : f x ≤ f (b • y + a • x)
⊢ f (b • y + a • x) ≤ f y

Tactic:
exact hf.le_left_of_right_le' hy hx hb ha hab hfx

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
lemma one_sub_inv_eq_geometric_of_summable_norm {f : ℕ →*₀ F} {p : ℕ} (hp : p.Prime)
    (hsum : Summable fun x ↦ ‖f x‖) :
    (1 - f p)⁻¹ = ∑' (e : ℕ), f (p ^ e)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x => ‖f x‖
⊢ (1 - f p)⁻¹ = ∑' (e : ℕ), f p ^ e

Tactic:
refine (tsum_geometric_of_norm_lt_one <| summable_geometric_iff_norm_lt_one.mp ?_).symm

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x => ‖f x‖
⊢ Summable fun n => f p ^ n

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x => ‖f x‖
⊢ (1 - f p)⁻¹ = ∑' (e : ℕ), f (p ^ e)

Tactic:
simp only [map_pow]

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x => ‖f x‖
⊢ (1 - f p)⁻¹ = ∑' (e : ℕ), f p ^ e

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x => ‖f x‖
⊢ Summable fun a => ‖f p ^ a‖

Tactic:
simpa only [Function.comp_def, map_pow]
  using hsum.comp_injective <| Nat.pow_right_injective hp.one_lt

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x => ‖f x‖
⊢ Summable fun n => f p ^ n

Tactic:
refine Summable.of_norm ?_

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x => ‖f x‖
⊢ Summable fun a => ‖f p ^ a‖
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙHom_eq_cfcₙ_extend {a : A} (g : R → R) (ha : p a) (f : C(σₙ R a, R)₀) :
    cfcₙHom ha f = cfcₙ (Function.extend Subtype.val f g) a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)
hg0 : Function.extend Subtype.val (⇑f) g 0 = 0
⊢ (cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a

Tactic:
rw [cfcₙ_apply ..]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)
hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)
hg0 : Function.extend Subtype.val (⇑f) g 0 = 0
⊢ (cfcₙHom ha) f =
    (cfcₙHom ha)
      { toFun := (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g), continuous_toFun := ⋯, map_zero' := hg0 }

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
g : R → R
ha : p a
f : C(↑(σₙ R a), R)₀
x✝ : ↑(σₙ R a)
⊢ f x✝ = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g) x✝
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
lemma TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply
    (m : M) (n : N) (i : κ) :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ n) i =
    𝒞.repr n i • m

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
i : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) i = (𝒞.repr n) i • m

Tactic:
simp only [equivFinsuppOfBasisRight_apply_tmul, Finsupp.mapRange_apply]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem isConnected_setOf_sOppSide {s : AffineSubspace ℝ P} {x : P} (hx : x ∉ s)
    (h : (s : Set P).Nonempty) : IsConnected { y | s.SOppSide x y }

Proof state:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ ConnectedSpace ↑↑s

Tactic:
convert AddTorsor.connectedSpace s.direction s

Result:
no goals

Proof state:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
⊢ IsConnected {y | s.SOppSide x y}

Tactic:
haveI : Nonempty s := ⟨⟨p, hp⟩⟩

Result:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected {y | s.SOppSide x y}

Proof state:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected {y | s.SOppSide x y}

Tactic:
rw [setOf_sOppSide_eq_image2 hx hp, ← Set.image_prod]

Result:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected ((fun x_1 => x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' Set.Iio 0 ×ˢ ↑s)

Proof state:
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
h : (↑s).Nonempty
⊢ IsConnected {y | s.SOppSide x y}

Tactic:
obtain ⟨p, hp⟩ := h

Result:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
⊢ IsConnected {y | s.SOppSide x y}

Proof state:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected ((fun x_1 => x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' Set.Iio 0 ×ˢ ↑s)

Tactic:
refine (isConnected_Iio.prod (isConnected_iff_connectedSpace.2 ?_)).image _
  ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Result:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ ConnectedSpace ↑↑s
-- Mathlib/Analysis/Fourier/ZMod.lean
/-- The discrete Fourier transform of `Φ` is even if and only if `Φ` itself is. -/
lemma dft_even_iff {Φ : ZMod N → ℂ} : (𝓕 Φ).Even ↔ Φ.Even

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Function.Even (𝓕 Φ) ↔ Function.Even Φ

Tactic:
have h {f : ZMod N → ℂ} (hf : f.Even) : (𝓕 f).Even := by
  simp only [Function.Even, ← congr_fun (dft_comp_neg f), funext hf, implies_true]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Even f → Function.Even (𝓕 f)
⊢ Function.Even (𝓕 Φ) ↔ Function.Even Φ

Proof state:
N : ℕ
inst✝ : NeZero N
Φ f : ZMod N → ℂ
hf : Function.Even f
⊢ Function.Even (𝓕 f)

Tactic:
simp only [Function.Even, ← congr_fun (dft_comp_neg f), funext hf, implies_true]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Even f → Function.Even (𝓕 f)
hΦ : Function.Even (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = Φ x

Tactic:
simpa only [neg_neg, smul_right_inj (NeZero.ne (N : ℂ)), dft_dft] using h hΦ (-x)

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Even f → Function.Even (𝓕 f)
⊢ Function.Even (𝓕 Φ) ↔ Function.Even Φ

Tactic:
refine ⟨fun hΦ x ↦ ?_, h⟩

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Even f → Function.Even (𝓕 f)
hΦ : Function.Even (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = Φ x
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
lemma summable_exp_nat_mul_iff {a : ℝ} :
    Summable (fun n : ℕ ↦ exp (n * a)) ↔ a < 0

Proof state:
a : ℝ
⊢ (Summable fun n => rexp (↑n * a)) ↔ a < 0

Tactic:
simp only [exp_nat_mul, summable_geometric_iff_norm_lt_one, norm_of_nonneg (exp_nonneg _),
  exp_lt_one_iff]

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem trans_range {a b c : X} (γ₁ : Path a b) (γ₂ : Path b c) :
    range (γ₁.trans γ₂) = range γ₁ ∪ range γ₂

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : γ₂ ⟨t, ⋯⟩ = x
h : t = 0
⊢ { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨1 / 2, ⋯⟩ =
    x

Tactic:
rw [coe_mk_mk, Function.comp_apply, if_pos le_rfl, Subtype.coe_mk,
  mul_one_div_cancel (two_ne_zero' ℝ)]

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : γ₂ ⟨t, ⋯⟩ = x
h : t = 0
⊢ γ₁.extend 1 = x
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
/-- The norm of a maximal ideal is `> 1` -/
lemma one_lt_absNorm : 1 < absNorm v.asIdeal

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
⊢ False

Tactic:
apply IsPrime.ne_top v.isPrime

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
⊢ v.asIdeal = ⊤

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
⊢ 1 < absNorm v.asIdeal

Tactic:
by_contra! h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
⊢ False

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
this : 0 < absNorm v.asIdeal
⊢ absNorm v.asIdeal = 1

Tactic:
omega

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
⊢ 0 < absNorm v.asIdeal

Tactic:
rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
⊢ Finite (𝓞 K ⧸ v.asIdeal)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
⊢ v.asIdeal = ⊤

Tactic:
rw [← absNorm_eq_one_iff]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
⊢ absNorm v.asIdeal = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
⊢ absNorm v.asIdeal = 1

Tactic:
have : 0 < absNorm v.asIdeal := by
  rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff]
  exact (v.asIdeal.fintypeQuotientOfFreeOfNeBot v.ne_bot).finite

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
this : 0 < absNorm v.asIdeal
⊢ absNorm v.asIdeal = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
h : absNorm v.asIdeal ≤ 1
⊢ Finite (𝓞 K ⧸ v.asIdeal)

Tactic:
exact (v.asIdeal.fintypeQuotientOfFreeOfNeBot v.ne_bot).finite

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem mem_range' : ∀{n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step * i
  | 0 => by simp [range', Nat.not_lt_zero]
  | n + 1 => by
    have h (i) : i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n

Proof state:
s step m n : Nat
⊢ m ∈ range' s (n + 1) step ↔ ∃ i, i < n + 1 ∧ m = s + step * i

Tactic:
have h (i) : i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n := by
  cases i <;> simp [Nat.succ_le, Nat.succ_inj']

Result:
s step m n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n
⊢ m ∈ range' s (n + 1) step ↔ ∃ i, i < n + 1 ∧ m = s + step * i

Proof state:
s step m n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ b a, a = b + 1 ∧ b < n ∧ m = s + step * a

Tactic:
simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]

Result:
no goals

Proof state:
s step m n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n
⊢ m ∈ range' s (n + 1) step ↔ ∃ i, i < n + 1 ∧ m = s + step * i

Tactic:
simp [range', mem_range', Nat.lt_succ, h]

Result:
s step m n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a, (∃ j, a = j + 1 ∧ j < n) ∧ m = s + step * a

Proof state:
s step m n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a, (∃ j, a = j + 1 ∧ j < n) ∧ m = s + step * a

Tactic:
simp only [← exists_and_right, and_assoc]

Result:
s step m n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a x, a = x + 1 ∧ x < n ∧ m = s + step * a

Proof state:
s step m n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a x, a = x + 1 ∧ x < n ∧ m = s + step * a

Tactic:
rw [exists_comm]

Result:
s step m n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ b a, a = b + 1 ∧ b < n ∧ m = s + step * a

Proof state:
s step m n i : Nat
⊢ i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n

Tactic:
cases i <;> simp [Nat.succ_le, Nat.succ_inj']

Result:
no goals

Proof state:
s step m : Nat
⊢ m ∈ range' s 0 step ↔ ∃ i, i < 0 ∧ m = s + step * i

Tactic:
simp [range', Nat.not_lt_zero]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem Chain.imp {r₁ r₂ : α → α → Prop} (H : ∀ a b, r₁ a b → r₂ a b) (p : Chain r₁ s) :
    Chain r₂ s

Proof state:
case HI
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)

Tactic:
rw [chain_coe_cons] at p ⊢

Result:
case HI
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : List.Chain r₁ a✝¹ (l✝ ++ [a✝¹])
⊢ List.Chain r₂ a✝¹ (l✝ ++ [a✝¹])

Proof state:
case H0
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil

Tactic:
trivial

Result:
no goals

Proof state:
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ s
⊢ Chain r₂ s

Tactic:
induction s

Result:
case H0
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil

case HI
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)

Proof state:
case HI
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : List.Chain r₁ a✝¹ (l✝ ++ [a✝¹])
⊢ List.Chain r₂ a✝¹ (l✝ ++ [a✝¹])

Tactic:
exact p.imp H

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} {k fallback : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    (ofList l).getKeyD k fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k fallback : α
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ (ofList l).getKeyD k fallback = fallback

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/RingTheory/Ideal/Pointwise.lean
theorem mem_pointwise_smul_iff_inv_smul_mem {a : M} {S : Ideal R} {x : R} :
    x ∈ a • S ↔ a⁻¹ • x ∈ S :=
  ⟨fun h => by simpa using smul_mem_pointwise_smul a⁻¹ _ _ h,
    fun h => by simpa using smul_mem_pointwise_smul a _ _ h⟩

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x : R
h : a⁻¹ • x ∈ S
⊢ x ∈ a • S

Tactic:
simpa using smul_mem_pointwise_smul a _ _ h

Result:
no goals

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x : R
h : x ∈ a • S
⊢ a⁻¹ • x ∈ S

Tactic:
simpa using smul_mem_pointwise_smul a⁻¹ _ _ h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem mem_alterKey_of_key_ne {a : α} {f : Option (β a) → Option (β a)}
    {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.1 ≠ a) :
    p ∈ alterKey a f l ↔ p ∈ l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
p : (a : α) × β a
hne : p.fst ≠ a
⊢ (p ∈
      match f (getValueCast? a l) with
      | none => eraseKey a l
      | some v => insertEntry a v l) ↔
    p ∈ l

Tactic:
split <;> simp only [mem_eraseKey_of_key_ne p hne, mem_insertEntry_of_key_ne p hne]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
p : (a : α) × β a
hne : p.fst ≠ a
⊢ p ∈ alterKey a f l ↔ p ∈ l

Tactic:
rw [alterKey]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
p : (a : α) × β a
hne : p.fst ≠ a
⊢ (p ∈
      match f (getValueCast? a l) with
      | none => eraseKey a l
      | some v => insertEntry a v l) ↔
    p ∈ l