harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_one_add_le (h : -1 ≤ x) : √(1 + x) ≤ 1 + x / 2

Proof state:
x : ℝ
h : -1 ≤ x
⊢ 1 + x ≤ (1 + x / 2) ^ 2

Tactic:
calc 1 + x
  _ ≤ 1 + x + (x / 2) ^ 2 := le_add_of_nonneg_right <| sq_nonneg _
  _ = _ := by ring

Result:
no goals

Proof state:
x : ℝ
h : -1 ≤ x
⊢ 1 + x + (x / 2) ^ 2 = (1 + x / 2) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
x : ℝ
h : -1 ≤ x
⊢ 0 ≤ 1 + x / 2

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
h : -1 ≤ x
⊢ √(1 + x) ≤ 1 + x / 2

Tactic:
refine sqrt_le_iff.mpr ⟨by linarith, ?_⟩

Result:
x : ℝ
h : -1 ≤ x
⊢ 1 + x ≤ (1 + x / 2) ^ 2
-- Mathlib/RingTheory/RingHomProperties.lean
theorem RespectsIso.cancel_right_isIso (hP : RespectsIso @P) {R S T : CommRingCat} (f : R ⟶ S)
    (g : S ⟶ T) [IsIso g] : P (g.hom.comp f.hom) ↔ P f.hom :=
  ⟨fun H => by
    convert hP.1 (f ≫ g).hom (asIso g).symm.commRingCatIsoToRingEquiv H
    simp [← CommRingCat.hom_comp],
   hP.1 f.hom (asIso g).commRingCatIsoToRingEquiv⟩

Proof state:
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso g
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ CommRingCat.Hom.hom f = (asIso g).symm.commRingCatIsoToRingEquiv.toRingHom.comp (CommRingCat.Hom.hom (f ≫ g))

Tactic:
simp [← CommRingCat.hom_comp]

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso g
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P (CommRingCat.Hom.hom f)

Tactic:
convert hP.1 (f ≫ g).hom (asIso g).symm.commRingCatIsoToRingEquiv H

Result:
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso g
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ CommRingCat.Hom.hom f = (asIso g).symm.commRingCatIsoToRingEquiv.toRingHom.comp (CommRingCat.Hom.hom (f ≫ g))
-- Mathlib/CategoryTheory/Equivalence.lean
theorem counit_app_functor (e : C ≌ D) (X : C) :
    e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 (e.functor.obj ((𝟭 C).obj X))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)

Tactic:
erw [← Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)), functor_unit_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 (e.functor.obj ((𝟭 C).obj X))
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_addY (P Q : Fin 3 → A) : (W'.baseChange B).toProjective.addY (f ∘ P) (f ∘ Q) =
    f ((W'.baseChange A).toProjective.addY P Q)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (baseChange W' B).toProjective.addY (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toProjective.addY P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_addY, map_baseChange]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem cos_ne_zero_iff {θ : ℂ} : cos θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ (2 * k + 1) * π / 2

Proof state:
θ : ℂ
⊢ cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * ↑π / 2

Tactic:
rw [← not_exists, not_iff_not, cos_eq_zero_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_reverse (a : α) (l : Vector α n) : count a l.reverse = count a l

Proof state:
α : Type u_1
inst✝ : BEq α
n : Nat
a : α
l : Vector α n
⊢ count a l.reverse = count a l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
⊢ count a { toArray := l, size_toArray := ⋯ }.reverse = count a { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
⊢ count a { toArray := l, size_toArray := ⋯ }.reverse = count a { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.inter_isBasis_biInter {ι : Type*} (hI : M.Indep I) {X : ι → Set α} {A : Set ι}
    (hA : A.Nonempty) (h : ∀ i ∈ A, M.IsBasis ((X i) ∩ I) (X i)) :
    M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)

Proof state:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋃ i ∈ A, (fun i => X i ∩ I) i ⊆ I

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)

Tactic:
refine (hI.inter_left _).isBasis_of_subset_of_subset_closure inter_subset_left ?_

Result:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)

Proof state:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ∀ i ∈ A, ⋂ i ∈ A, X i ⊆ M.closure (X i ∩ I)

Tactic:
exact fun i hiA ↦ (biInter_subset_of_mem hiA).trans (h i hiA).subset_closure

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)

Tactic:
simp_rw [← biInter_inter hA,
closure_biInter_eq_biInter_closure_of_biUnion_indep hA (I := fun i ↦ (X i) ∩ I)
    (hI.subset (by simp)), subset_iInter_iff]

Result:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ∀ i ∈ A, ⋂ i ∈ A, X i ⊆ M.closure (X i ∩ I)
-- Mathlib/Data/Matroid/Map.lean
lemma Indep.mapEmbedding (hI : M.Indep I) (f : α ↪ β) : (M.mapEmbedding f).Indep (f '' I)

Proof state:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
hI : M.Indep I
f : α ↪ β
⊢ (M.mapEmbedding f).Indep (⇑f '' I)

Tactic:
simpa [preimage_image_eq I f.injective]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem normalizedFactors_pow {x : α} (n : ℕ) :
    normalizedFactors (x ^ n) = n • normalizedFactors x

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
simp [h0, zero_pow n.succ_ne_zero, smul_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ normalizedFactors (x ^ n) = n • normalizedFactors x

Tactic:
induction' n with n ih

Result:
case zero
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
⊢ normalizedFactors (x ^ 0) = 0 • normalizedFactors x

case succ
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Proof state:
case succ
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
by_cases h0 : x = 0

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Proof state:
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
rw [pow_succ', succ_nsmul', normalizedFactors_mul h0 (pow_ne_zero _ h0), ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
⊢ normalizedFactors (x ^ 0) = 0 • normalizedFactors x

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem changeFormAux_changeFormAux (B : BilinForm R M) (v : M) (x : CliffordAlgebra Q) :
    changeFormAux Q B v (changeFormAux Q B v x) = (Q v - B v v) • x

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ (ι Q) v * ((ι Q) v * x - (contractLeft (B v)) x) - (contractLeft (B v)) ((ι Q) v * x - (contractLeft (B v)) x) =
    (Q v - (B v) v) • x

Tactic:
rw [mul_sub, ← mul_assoc, ι_sq_scalar, map_sub, contractLeft_ι_mul, ← sub_add, sub_sub_sub_comm,
  ← Algebra.smul_def, sub_self, sub_zero, contractLeft_contractLeft, add_zero, sub_smul]

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ ((changeFormAux Q B) v) (((changeFormAux Q B) v) x) = (Q v - (B v) v) • x

Tactic:
simp only [changeFormAux_apply_apply]

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ (ι Q) v * ((ι Q) v * x - (contractLeft (B v)) x) - (contractLeft (B v)) ((ι Q) v * x - (contractLeft (B v)) x) =
    (Q v - (B v) v) • x
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Fork.ofCone_π {F : WalkingParallelPair ⥤ C} (t : Cone F) (j) :
    (Fork.ofCone t).π.app j = t.π.app j ≫ eqToHom (by simp) := rfl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
j : WalkingParallelPair
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
@[reassoc (attr := simp)]
lemma map_hom_inv_id (F : C ⥤ D) :
    F.map e.hom ≫ F.map e.inv = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
X Y : C
e : X ≅ Y
F : C ⥤ D
⊢ F.map e.hom ≫ F.map e.inv = 𝟙 (F.obj X)

Tactic:
rw [← F.map_comp, e.hom_inv_id, F.map_id]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₄_of_isCharTwoJNeZeroNF_of_char_two : W.c₄ = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 1 ^ 2 = 1

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.c₄ = 1

Tactic:
rw [c₄_of_isCharTwoJNeZeroNF, b₂_of_isCharTwoJNeZeroNF_of_char_two]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 1 ^ 2 = 1
-- Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean
theorem submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det' {n : ℕ}
    (M : Matrix (Fin n) (Fin (n + 1)) R) (hv : ∀ i, ∑ j, M i j = 0) (j₁ j₂ : Fin (n + 1)) :
    (M.submatrix id (Fin.succAbove j₁)).det =
      Int.negOnePow (j₁ - j₂) • (M.submatrix id (Fin.succAbove j₂)).det

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0
j₁ j₂ : Fin (n + 1)
x✝ : Fin n
⊢ (∑ j : Fin (n + 1), Mᵀ j) x✝ = 0 x✝

Tactic:
simp_rw [Finset.sum_apply, transpose_apply, hv, Pi.zero_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ ∑ j : Fin (n + 1), Mᵀ j = 0

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0
j₁ j₂ : Fin (n + 1)
x✝ : Fin n
⊢ (∑ j : Fin (n + 1), Mᵀ j) x✝ = 0 x✝

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix id j₁.succAbove).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det

Tactic:
rw [← det_transpose, transpose_submatrix,
  submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det M.transpose ?_ j₁ j₂,
  ← det_transpose, transpose_submatrix, transpose_transpose]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ ∑ j : Fin (n + 1), Mᵀ j = 0
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_eq_empty : (s : Set α) = ∅ ↔ s = ⊤

Proof state:
α : Type u_1
inst✝ : LE α
s : UpperSet α
⊢ ↑s = ∅ ↔ s = ⊤

Tactic:
simp [SetLike.ext'_iff]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem hasIntegral_zero : HasIntegral I l (fun _ => (0 : E)) vol 0

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
⊢ HasIntegral I l (fun x => 0) vol 0

Tactic:
simpa only [← (vol I).map_zero] using hasIntegral_const (0 : E)

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem eta_fin_three (A : Matrix (Fin 3) (Fin 3) α) :
    A = !![A 0 0, A 0 1, A 0 2;
           A 1 0, A 1 1, A 1 2;
           A 2 0, A 2 1, A 2 2]

Proof state:
case a
α : Type u
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A i j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] i j

Tactic:
fin_cases i <;> fin_cases j <;> rfl

Result:
no goals

Proof state:
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2]

Tactic:
ext i j

Result:
case a
α : Type u
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A i j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] i j
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem irrational (h : LiouvilleWith p x) (hp : 1 < p) : Irrational x

Proof state:
case intro
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
⊢ False

Tactic:
rcases eq_or_ne r 0 with (rfl | h0)

Result:
case intro.inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ False

case intro.inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ False

Proof state:
p x : ℝ
h : LiouvilleWith p x
hp : 1 < p
⊢ Irrational x

Tactic:
rintro ⟨r, rfl⟩

Result:
case intro
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
⊢ False

Proof state:
case intro.inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ 1 = ↑1

case intro.inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r ≠ 0

Tactic:
exacts [Int.cast_one.symm, Rat.cast_ne_zero.mpr h0]

Result:
no goals

Proof state:
case intro.inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r * ↑r⁻¹ = ↑1

Tactic:
rw [Rat.cast_inv, mul_inv_cancel₀]

Result:
case intro.inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ 1 = ↑1

case intro.inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r ≠ 0

Proof state:
case intro.inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0

Tactic:
rw [Rat.cast_zero, Int.cast_zero]

Result:
no goals

Proof state:
case intro.inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ False

Tactic:
refine h.ne_cast_int hp 0 ?_

Result:
case intro.inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0

Proof state:
case intro.inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ False

Tactic:
refine (h.mul_rat (inv_ne_zero h0)).ne_cast_int hp 1 ?_

Result:
case intro.inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r * ↑r⁻¹ = ↑1
-- Mathlib/Order/BooleanAlgebra.lean
theorem disjoint_sdiff_comm : Disjoint (x \ z) y ↔ Disjoint x (y \ z)

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ Disjoint (x \ z) y ↔ Disjoint x (y \ z)

Tactic:
simp_rw [disjoint_iff, sdiff_inf_right_comm, inf_sdiff_assoc]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem orthogonalProjection_orthogonalProjection (s : AffineSubspace ℝ P) [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : P) :
    orthogonalProjection s (orthogonalProjection s p) = orthogonalProjection s p

Proof state:
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑((orthogonalProjection s) p) ∈ s

Tactic:
exact orthogonalProjection_mem p

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ (orthogonalProjection s) ↑((orthogonalProjection s) p) = (orthogonalProjection s) p

Tactic:
ext

Result:
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑((orthogonalProjection s) ↑((orthogonalProjection s) p)) = ↑((orthogonalProjection s) p)

Proof state:
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑((orthogonalProjection s) ↑((orthogonalProjection s) p)) = ↑((orthogonalProjection s) p)

Tactic:
rw [orthogonalProjection_eq_self_iff]

Result:
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑((orthogonalProjection s) p) ∈ s
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma isPullback_opens_inf {X : Scheme} (U V : X.Opens) :
    IsPullback (X.homOfLE inf_le_left) (X.homOfLE inf_le_right) U.ι V.ι :=
  (isPullback_morphismRestrict V.ι U).of_iso (V.ι.isoImage _ ≪≫ X.isoOfEq
    (V.functor_map_eq_inf U)) (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp [← cancel_mono U.ι])
    (by simp [← cancel_mono V.ι]) (by simp) (by simp)

Proof state:
X : Scheme
U V : X.Opens
⊢ V.ι ≫ (Iso.refl X).hom = (Iso.refl ↑V).hom ≫ V.ι

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
⊢ U.ι ≫ (Iso.refl X).hom = (Iso.refl ↑U).hom ≫ U.ι

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
⊢ (V.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑V).hom = (Scheme.Hom.isoImage V.ι (V.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

Tactic:
simp [← cancel_mono V.ι]

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
⊢ V.ι ∣_ U ≫ (Iso.refl ↑U).hom = (Scheme.Hom.isoImage V.ι (V.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

Tactic:
simp [← cancel_mono U.ι]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/Path.lean
lemma spine_map_vertex {n : ℕ} (x : X _⦋n⦌) {m : ℕ} (φ : ⦋m⦌ ⟶ ⦋n⦌)
    (i : Fin (m + 1)) :
    (spine X m (X.map φ.op x)).vertex i = (spine X n x).vertex (φ.toOrderHom i)

Proof state:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
φ : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ (X.spine m (X.map φ.op x)).vertex i = (X.spine n x).vertex ((Hom.toOrderHom φ) i)

Tactic:
dsimp [spine]

Result:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
φ : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ X.map (⦋0⦌.const ⦋m⦌ i).op (X.map φ.op x) = X.map (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom φ) i)).op x

Proof state:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
φ : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ X.map (⦋0⦌.const ⦋m⦌ i).op (X.map φ.op x) = X.map (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom φ) i)).op x

Tactic:
rw [← FunctorToTypes.map_comp_apply]

Result:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
φ : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ X.map (φ.op ≫ (⦋0⦌.const ⦋m⦌ i).op) x = X.map (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom φ) i)).op x

Proof state:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
φ : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ X.map (φ.op ≫ (⦋0⦌.const ⦋m⦌ i).op) x = X.map (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom φ) i)).op x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem tendsto_nhdsWithin_nhds [PseudoMetricSpace β] {f : α → β} {a b} :
    Tendsto f (𝓝[s] a) (𝓝 b) ↔
      ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ univ ∧ dist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε

Tactic:
simp only [mem_univ, true_and]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε

Tactic:
rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ univ ∧ dist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem concat_inj_left {l l' : List α} (a : α) : concat l a = concat l' a ↔ l = l' :=
  ⟨init_eq_of_concat_eq, by simp⟩

Proof state:
α : Type u_1
l l' : List α
a : α
⊢ l = l' → l.concat a = l'.concat a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem _root_.Set.LeftInvOn.filter_map_Iic {f : α → β} {g : β → α} (hfg : LeftInvOn g f s) :
    LeftInvOn (map g) (map f) (Iic <| 𝓟 s) := fun F (hF : F ≤ 𝓟 s) ↦ by
  have : (g ∘ f) =ᶠ[𝓟 s] id

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
⊢ map g (map f F) = F

Tactic:
have : (g ∘ f) =ᶠ[𝓟 s] id := by simpa only [eventuallyEq_principal] using hfg

Result:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
⊢ map g (map f F) = F

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
⊢ map g (map f F) = F

Tactic:
rw [map_map, map_congr (this.filter_mono hF), map_id]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
⊢ g ∘ f =ᶠ[𝓟 s] id

Tactic:
simpa only [eventuallyEq_principal] using hfg

Result:
no goals