harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem constantCoeff_wittStructureInt (Φ : MvPolynomial idx ℤ) (h : constantCoeff Φ = 0) (n : ℕ) :
    constantCoeff (wittStructureInt p Φ n) = 0

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
⊢ constantCoeff (wittStructureInt p Φ n) = 0

Tactic:
have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff (wittStructureInt p Φ n) = 0

Proof state:
case a.h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff ((map (Int.castRingHom ℚ)) Φ) = 0

Tactic:
rw [constantCoeff_map, h, RingHom.map_zero]

Result:
no goals

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n✝ : ℕ
m n : ℤ
⊢ (Int.castRingHom ℚ) m = (Int.castRingHom ℚ) n → m = n

Tactic:
exact Int.cast_inj.mp

Result:
no goals

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ n)) = (Int.castRingHom ℚ) 0

Tactic:
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat, RingHom.map_zero]

Result:
case a.h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff ((map (Int.castRingHom ℚ)) Φ) = 0

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
⊢ Function.Injective ⇑(Int.castRingHom ℚ)

Tactic:
intro m n

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n✝ : ℕ
m n : ℤ
⊢ (Int.castRingHom ℚ) m = (Int.castRingHom ℚ) n → m = n

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff (wittStructureInt p Φ n) = 0

Tactic:
apply inj

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ n)) = (Int.castRingHom ℚ) 0
-- Mathlib/Algebra/Module/Injective.lean
lemma of_equiv (e : Q ≃ₗ[R] M) (h : Module.Baer R Q) : Module.Baer R M := fun I g ↦
  have ⟨g', h'⟩ := h I (e.symm ∘ₗ g)
  ⟨e ∘ₗ g', by simpa [LinearEquiv.eq_symm_apply] using h'⟩

Proof state:
R : Type u
inst✝⁴ : Ring R
Q : Type v
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : Q ≃ₗ[R] M
h : Baer R Q
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] Q
h' : ∀ (x : R) (mem : x ∈ I), g' x = (↑e.symm ∘ₗ g) ⟨x, mem⟩
⊢ ∀ (x : R) (mem : x ∈ I), (↑e ∘ₗ g') x = g ⟨x, mem⟩

Tactic:
simpa [LinearEquiv.eq_symm_apply] using h'

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem ne_zero_iff {p : MvPolynomial σ R} : p ≠ 0 ↔ ∃ d, coeff d p ≠ 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p ≠ 0 ↔ ∃ d, coeff d p ≠ 0

Tactic:
rw [Ne, eq_zero_iff]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∃ d, coeff d p ≠ 0) ↔ ∃ d, coeff d p ≠ 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0

Tactic:
push_neg

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∃ d, coeff d p ≠ 0) ↔ ∃ d, coeff d p ≠ 0
-- Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
lemma extendToSucc_map_le_succ :
    (extendToSucc hj F τ).map (homOfLE (Order.le_succ j)) =
        (extendToSuccObjIso hj F τ j (by simp)).hom ≫ τ ≫
          (extendToSuccObjSuccIso hj F τ).inv :=
  extendToSucc.map_self_succ _ _ _

Proof state:
C : Type u_1
inst✝² : Category.{?u.81832, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ j ≤ j

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Ico_iff_integrableOn_Ioo' (ha : μ {a} ≠ ∞) :
    IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : ¬a < b
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [Ioo_eq_empty hab, Ico_eq_empty hab]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : a < b
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [← Ioo_union_left hab, integrableOn_union,
  eq_true (integrableOn_singleton_iff.mpr <| Or.inr ha.lt_top), and_true]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
by_cases hab : a < b

Result:
case pos
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : a < b
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : ¬a < b
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
-- Mathlib/Algebra/Divisibility/Basic.lean
lemma dvd_pow (hab : a ∣ b) : ∀ {n : ℕ} (_ : n ≠ 0), a ∣ b ^ n
  | 0,     hn => (hn rfl).elim
  | n + 1, _  => by rw [pow_succ']; exact hab.mul_right _

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hab : a ∣ b
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ∣ b * b ^ n

Tactic:
exact hab.mul_right _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hab : a ∣ b
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ∣ b ^ (n + 1)

Tactic:
rw [pow_succ']

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
hab : a ∣ b
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ∣ b * b ^ n
-- Mathlib/Analysis/Convex/Side.lean
theorem setOf_wOppSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) :
    { y | s.WOppSide x y } = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) s

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
⊢ {y | s.WOppSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s

Tactic:
ext y

Result:
case h
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.WOppSide x y} ↔ y ∈ Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s

Proof state:
case h.mp.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
rw [vsub_eq_zero_iff_eq] at h

Result:
case h.mp.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Proof state:
case h.mp.intro.intro.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ 0 • (x -ᵥ p) +ᵥ p₂ = y

Tactic:
simp [h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negY_smul (P : Fin 3 → R) (u : R) : W'.negY (u • P) = u * W'.negY P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ -(u * P y) - W'.a₁ * (u * P x) - W'.a₃ * (u * P z) = u * (-P y - W'.a₁ * P x - W'.a₃ * P z)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.negY (u • P) = u * W'.negY P

Tactic:
simp only [negY, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ -(u * P y) - W'.a₁ * (u * P x) - W'.a₃ * (u * P z) = u * (-P y - W'.a₁ * P x - W'.a₃ * P z)
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem edist_le_of_edist_le_geometric_two_of_tendsto₀ : edist (f 0) a ≤ 2 * C

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ edist (f 0) a ≤ 2 * C

Tactic:
simpa only [_root_.pow_zero, div_eq_mul_inv, inv_one, mul_one] using
  edist_le_of_edist_le_geometric_two_of_tendsto C hu ha 0

Result:
no goals
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegrable_zero_radius {f : ℂⁿ → E} {c : ℂⁿ} : TorusIntegrable f c 0

Proof state:
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ IntegrableOn (fun θ => f (const (Fin n → ℝ) c θ)) (Icc 0 fun x => 2 * π) volume

Tactic:
apply torusIntegrable_const (f c) c 0

Result:
no goals

Proof state:
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ TorusIntegrable f c 0

Tactic:
rw [TorusIntegrable, torusMap_zero_radius]

Result:
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ IntegrableOn (fun θ => f (const (Fin n → ℝ) c θ)) (Icc 0 fun x => 2 * π) volume
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma apply_le_nnnorm_cfcₙ_nnreal (f : ℝ≥0 → ℝ≥0) (a : A) ⦃x : ℝ≥0⦄ (hx : x ∈ σₙ ℝ≥0 a)
    (hf : ContinuousOn f (σₙ ℝ≥0 a)

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
⊢ f x ≤ ‖cfcₙ f a‖₊

Tactic:
revert hx

Result:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hf : autoParam (ContinuousOn f (σₙ ℝ≥0 a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (0 ≤ a) _auto✝
⊢ x ∈ σₙ ℝ≥0 a → f x ≤ ‖cfcₙ f a‖₊
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem insertIdx_length_self (l : List α) (x : α) : insertIdx l.length x l = l ++ [x]

Proof state:
case nil
α : Type u
x : α
⊢ insertIdx [].length x [] = [] ++ [x]

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
x✝ x : α
l : List α
ih : insertIdx l.length x✝ l = l ++ [x✝]
⊢ insertIdx (x :: l).length x✝ (x :: l) = x :: l ++ [x✝]

Tactic:
simpa using ih

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
⊢ insertIdx l.length x l = l ++ [x]

Tactic:
induction l with
| nil => simp
| cons x l ih => simpa using ih

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a

Proof state:
α✝ : Type u_1
l : List α✝
p : α✝ → Bool
⊢ countP p l = 0 ↔ ∀ (a : α✝), a ∈ l → ¬p a = true

Tactic:
simp only [countP_eq_length_filter, length_eq_zero, filter_eq_nil_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_add_cancel_right {m n k : Int} (i) : (m + i) % n = (k + i) % n ↔ m % n = k % n :=
  ⟨fun H => by
    have := add_emod_eq_add_emod_right (-i) H
    rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this,
  add_emod_eq_add_emod_right _⟩

Proof state:
m n k i : Int
H : (m + i) % n = (k + i) % n
this : (m + i + -i) % n = (k + i + -i) % n
⊢ m % n = k % n

Tactic:
rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this

Result:
no goals

Proof state:
m n k i : Int
H : (m + i) % n = (k + i) % n
⊢ m % n = k % n

Tactic:
have := add_emod_eq_add_emod_right (-i) H

Result:
m n k i : Int
H : (m + i) % n = (k + i) % n
this : (m + i + -i) % n = (k + i + -i) % n
⊢ m % n = k % n
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma leftRightHomologyComparison'_compatibility (h₁ h₁' : S.LeftHomologyData)
    (h₂ h₂' : S.RightHomologyData) :
    leftRightHomologyComparison' h₁ h₂ = leftHomologyMap' (𝟙 S) h₁ h₁' ≫
      leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ =
    leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂

Tactic:
rw [leftRightHomologyComparison'_naturality_assoc (𝟙 S) h₁ h₂ h₁' h₂',
  ← rightHomologyMap'_comp, comp_id, rightHomologyMap'_id, comp_id]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc]
lemma cochainsMap_comp {G H K : Type u} [Group G] [Group H] [Group K]
    {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H)
    (φ : (Action.res _ f).obj A ⟶ B) (ψ : (Action.res _ g).obj B ⟶ C) :
    cochainsMap (f.comp g) ((Action.res _ g).map φ ≫ ψ) =
      cochainsMap f φ ≫ cochainsMap g ψ

Proof state:
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k K
B : Rep k H
C : Rep k G
f : H →* K
g : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
ψ : (Action.res (ModuleCat k) g).obj B ⟶ C
⊢ cochainsMap (f.comp g) ((Action.res (ModuleCat k) g).map φ ≫ ψ) = cochainsMap f φ ≫ cochainsMap g ψ

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_p_lt_one : ‖(p : ℚ_[p])‖ < 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ < 1

Tactic:
rw [norm_p]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ < 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ < 1

Tactic:
exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
lemma adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers (v : HeightOneSpectrum R)
    (a : v.adicCompletion K) : ∃ b ∈ R⁰, a * b ∈ v.adicCompletionIntegers K

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
⊢ ϖ ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
hϖ : v.intValuationDef 0 = ↑(ofAdd (-1))
⊢ False

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
hϖ : v.intValuationDef 0 = ↑(ofAdd (-1))
⊢ False

Tactic:
simp at hϖ

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
d : ℤ
ha : 0 < d
hd : Valued.v a = ↑(ofAdd d)
ϖ : R
hϖ : v.intValuationDef ϖ = ↑(ofAdd (-1))
hϖ0 : ϖ ≠ 0
⊢ d.natAbs • -1 = ↑d.natAbs • -1

Tactic:
simp only [nsmul_eq_mul,
Int.natCast_natAbs, smul_eq_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_mul_cos_add_sin_mul_I_coe_angle {r : ℝ} (hr : 0 < r) (θ : Real.Angle) :
    (arg (r * (Real.Angle.cos θ + Real.Angle.sin θ * I)) : Real.Angle) = θ

Proof state:
r : ℝ
hr : 0 < r
θ : Real.Angle
⊢ ↑(↑r * (↑θ.cos + ↑θ.sin * I)).arg = θ

Tactic:
induction' θ using Real.Angle.induction_on with θ

Result:
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(↑r * (↑(↑θ).cos + ↑(↑θ).sin * I)).arg = ↑θ

Proof state:
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ∃ k, (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)).arg - θ = 2 * π * ↑k

Tactic:
use ⌊(π - θ) / (2 * π)⌋

Result:
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Proof state:
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(↑r * (↑(↑θ).cos + ↑(↑θ).sin * I)).arg = ↑θ

Tactic:
rw [Real.Angle.cos_coe, Real.Angle.sin_coe, Real.Angle.angle_eq_iff_two_pi_dvd_sub]

Result:
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ∃ k, (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)).arg - θ = 2 * π * ↑k

Proof state:
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
exact mod_cast arg_mul_cos_add_sin_mul_I_sub hr θ

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem of_injective (i : ι) : Function.Injective (of : M i →* _)

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
⊢ Function.Injective ⇑of

Tactic:
classical exact (of_leftInverse i).injective

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
⊢ Function.Injective ⇑of

Tactic:
exact (of_leftInverse i).injective

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Doubling.lean
theorem exists_eventually_forall_measure_closedBall_le_mul (K : ℝ) :
    ∃ C : ℝ≥0, ∀ᶠ ε in 𝓝[>] 0, ∀ x, ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ C * μ (closedBall x ε)

Proof state:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε : ∀ (x : α), μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * μ (closedBall x ε)
hε₀ : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ 1 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : K < 1
ε : ℝ
hε : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ μ (closedBall x (t * ε)) ≤ μ (closedBall x ε)

Tactic:
gcongr

Result:
case inl.h.h
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
hK : K < 1
ε : ℝ
hε : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ t * ε ≤ ε
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
@[simp] lemma isMaximumClique_compl [Fintype α] (s : Finset α) :
    Gᶜ.IsMaximumClique s ↔ G.IsMaximumIndepSet s

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
⊢ Gᶜ.IsMaximumClique s ↔ G.IsMaximumIndepSet s

Tactic:
simp [isMaximumIndepSet_iff, isMaximumClique_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
lemma injOn_iff_surjOn {p : Submodule K V} [FiniteDimensional K p]
    {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) :
    Set.InjOn f p ↔ Set.SurjOn f p p

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
⊢ Injective ⇑(f.domRestrict p) ↔ Surjective ⇑(f.restrict h)

Tactic:
simp [disjoint_iff, ← injective_iff_surjective]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
⊢ Set.InjOn ⇑f ↑p ↔ Set.SurjOn ⇑f ↑p ↑p

Tactic:
rw [Set.injOn_iff_injective, ← Set.MapsTo.restrict_surjective_iff h]

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
⊢ Injective ((↑p).restrict ⇑f) ↔ Surjective (Set.MapsTo.restrict (⇑f) (↑p) (↑p) h)

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
⊢ Injective ((↑p).restrict ⇑f) ↔ Surjective (Set.MapsTo.restrict (⇑f) (↑p) (↑p) h)

Tactic:
change Injective (f.domRestrict p) ↔ Surjective (f.restrict h)

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
⊢ Injective ⇑(f.domRestrict p) ↔ Surjective ⇑(f.restrict h)
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem of'_modOf (g : G) : of' k G g %ᵒᶠ g = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
⊢ of' k G g %ᵒᶠ g = 0

Tactic:
simpa only [one_mul] using mul_of'_modOf (1 : k[G]) g

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem isPathConnected_pathComponentIn (h : x ∈ F) : IsPathConnected (pathComponentIn x F) :=
  ⟨x, mem_pathComponentIn_self h, fun ⟨γ, hγ⟩ ↦ by
    refine ⟨γ, fun t ↦
      ⟨(γ.truncateOfLE t.2.1).cast (γ.extend_zero.symm) (γ.extend_extends' t).symm, fun t' ↦ ?_⟩⟩
    dsimp [Path.truncateOfLE, Path.truncate]
    exact γ.extend_extends' ⟨min (max t'.1 0) t.1, by simp [t.2.1, t.2.2]⟩ ▸ hγ _⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
y✝ : X
x✝ : y✝ ∈ pathComponentIn x F
γ : Path x y✝
hγ : ∀ (t : ↑I), γ t ∈ F
⊢ JoinedIn (pathComponentIn x F) x y✝

Tactic:
refine ⟨γ, fun t ↦
  ⟨(γ.truncateOfLE t.2.1).cast (γ.extend_zero.symm) (γ.extend_extends' t).symm, fun t' ↦ ?_⟩⟩

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
y✝ : X
x✝ : y✝ ∈ pathComponentIn x F
γ : Path x y✝
hγ : ∀ (t : ↑I), γ t ∈ F
t t' : ↑I
⊢ ((γ.truncateOfLE ⋯).cast ⋯ ⋯) t' ∈ F

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
y✝ : X
x✝ : y✝ ∈ pathComponentIn x F
γ : Path x y✝
hγ : ∀ (t : ↑I), γ t ∈ F
t t' : ↑I
⊢ (↑t' ⊔ 0) ⊓ ↑t ∈ Icc 0 1

Tactic:
simp [t.2.1, t.2.2]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
y✝ : X
x✝ : y✝ ∈ pathComponentIn x F
γ : Path x y✝
hγ : ∀ (t : ↑I), γ t ∈ F
t t' : ↑I
⊢ ((γ.truncateOfLE ⋯).cast ⋯ ⋯) t' ∈ F

Tactic:
dsimp [Path.truncateOfLE, Path.truncate]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
y✝ : X
x✝ : y✝ ∈ pathComponentIn x F
γ : Path x y✝
hγ : ∀ (t : ↑I), γ t ∈ F
t t' : ↑I
⊢ γ.extend ((↑t' ⊔ 0) ⊓ ↑t) ∈ F

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
y✝ : X
x✝ : y✝ ∈ pathComponentIn x F
γ : Path x y✝
hγ : ∀ (t : ↑I), γ t ∈ F
t t' : ↑I
⊢ γ.extend ((↑t' ⊔ 0) ⊓ ↑t) ∈ F

Tactic:
exact γ.extend_extends' ⟨min (max t'.1 0) t.1, by simp [t.2.1, t.2.2]⟩ ▸ hγ _

Result:
no goals