harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Extension.lean
lemma Cotangent.smul_eq_zero_of_mem (p : P.Ring) (hp : p ∈ P.ker) (m : P.ker.Cotangent) :
    p • m = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
p : P.Ring
hp : p ∈ P.ker
m : P.ker.Cotangent
⊢ p • m = 0

Tactic:
obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ m

Result:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
p : P.Ring
hp : p ∈ P.ker
x : ↥P.ker
⊢ p • P.ker.toCotangent x = 0

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
p : P.Ring
hp : p ∈ P.ker
x : ↥P.ker
⊢ p * ↑x ∈ P.ker * P.ker

Tactic:
exact Ideal.mul_mem_mul hp x.2

Result:
no goals

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
p : P.Ring
hp : p ∈ P.ker
x : ↥P.ker
⊢ p • P.ker.toCotangent x = 0

Tactic:
rw [← map_smul, Ideal.toCotangent_eq_zero, Submodule.coe_smul, smul_eq_mul, pow_two]

Result:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
p : P.Ring
hp : p ∈ P.ker
x : ↥P.ker
⊢ p * ↑x ∈ P.ker * P.ker
-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
theorem w : forkMap P (S : Presieve X) ≫ firstMap P S = forkMap P S ≫ secondMap P S

Proof state:
case h.h
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
a✝ : P.obj (op X)
Y✝ Z✝ : C
g✝ : Z✝ ⟶ Y✝
f✝ : Y✝ ⟶ X
hf✝ : S.arrows f✝
⊢ Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y✝, ⟨Z✝, ⟨g✝, ⟨f✝, hf✝⟩⟩⟩⟩ ((forkMap P S.arrows ≫ firstMap P S) a✝) =
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y✝, ⟨Z✝, ⟨g✝, ⟨f✝, hf✝⟩⟩⟩⟩ ((forkMap P S.arrows ≫ secondMap P S) a✝)

Tactic:
simp [firstMap, secondMap, forkMap]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ forkMap P S.arrows ≫ firstMap P S = forkMap P S.arrows ≫ secondMap P S

Tactic:
ext

Result:
case h.h
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
a✝ : P.obj (op X)
Y✝ Z✝ : C
g✝ : Z✝ ⟶ Y✝
f✝ : Y✝ ⟶ X
hf✝ : S.arrows f✝
⊢ Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y✝, ⟨Z✝, ⟨g✝, ⟨f✝, hf✝⟩⟩⟩⟩ ((forkMap P S.arrows ≫ firstMap P S) a✝) =
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y✝, ⟨Z✝, ⟨g✝, ⟨f✝, hf✝⟩⟩⟩⟩ ((forkMap P S.arrows ≫ secondMap P S) a✝)
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_lt_iff {n : σ} {f : MvPolynomial σ R} {d : ℕ} (h : 0 < d) :
    degreeOf n f < d ↔ ∀ m : σ →₀ ℕ, m ∈ f.support → m n < d

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
⊢ degreeOf n f < d ↔ ∀ m ∈ f.support, m n < d

Tactic:
rwa [degreeOf_eq_sup, Finset.sup_lt_iff]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem neBot_of_comap (h : (comap m g).NeBot) : g.NeBot

Proof state:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : (comap m g).NeBot
⊢ g.NeBot

Tactic:
rw [neBot_iff] at *

Result:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : comap m g ≠ ⊥
⊢ g ≠ ⊥

Proof state:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m ⊥ = ⊥

Tactic:
exact comap_bot

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : comap m g ≠ ⊥
⊢ g ≠ ⊥

Tactic:
contrapose! h

Result:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m g = ⊥

Proof state:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m g = ⊥

Tactic:
rw [h]

Result:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m ⊥ = ⊥
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem infinite_deficient : {n : ℕ | n.Deficient}.Infinite

Proof state:
a : ℕ
⊢ ∃ b ∈ {n | n.Deficient}, a < b

Tactic:
obtain ⟨b, h1, h2⟩ := exists_infinite_primes a.succ

Result:
case intro.intro
a b : ℕ
h1 : a.succ ≤ b
h2 : Prime b
⊢ ∃ b ∈ {n | n.Deficient}, a < b

Proof state:
⊢ {n | n.Deficient}.Infinite

Tactic:
rw [Set.infinite_iff_exists_gt]

Result:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | n.Deficient}, a < b

Proof state:
case intro.intro
a b : ℕ
h1 : a.succ ≤ b
h2 : Prime b
⊢ ∃ b ∈ {n | n.Deficient}, a < b

Tactic:
exact ⟨b, h2.deficient, h1⟩

Result:
no goals

Proof state:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | n.Deficient}, a < b

Tactic:
intro a

Result:
a : ℕ
⊢ ∃ b ∈ {n | n.Deficient}, a < b
-- Mathlib/Data/Nat/Totient.lean
theorem totient_dvd_of_dvd {a b : ℕ} (h : a ∣ b) : φ a ∣ φ b

Proof state:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ (a.factorization.prod fun p k => p ^ (k - 1) * (p - 1)) ∣ b.factorization.prod fun p k => p ^ (k - 1) * (p - 1)

Tactic:
refine Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul ?_ dvd_rfl

Result:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
p : ℕ
x✝ : p ∈ a.factorization.support
⊢ p ^ (a.factorization p - 1) ∣ p ^ (b.factorization p - 1)

Proof state:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ φ a ∣ φ b

Tactic:
rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]

Result:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ (a.factorization.prod fun p k => p ^ (k - 1) * (p - 1)) ∣ b.factorization.prod fun p k => p ^ (k - 1) * (p - 1)

Proof state:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
p : ℕ
x✝ : p ∈ a.factorization.support
⊢ p ^ (a.factorization p - 1) ∣ p ^ (b.factorization p - 1)

Tactic:
exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)

Result:
no goals

Proof state:
case inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
⊢ φ a ∣ φ b

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Result:
case inr.inl
a : ℕ
ha0 : a ≠ 0
h : a ∣ 0
⊢ φ a ∣ φ 0

case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ φ a ∣ φ b

Proof state:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ φ a ∣ φ b

Tactic:
have hab' := primeFactors_mono h hb0

Result:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ φ a ∣ φ b

Proof state:
case inl
b : ℕ
h : 0 ∣ b
⊢ φ 0 ∣ φ b

Tactic:
simp [zero_dvd_iff.1 h]

Result:
no goals

Proof state:
case inr.inl
a : ℕ
ha0 : a ≠ 0
h : a ∣ 0
⊢ φ a ∣ φ 0

Tactic:
simp

Result:
no goals

Proof state:
a b : ℕ
h : a ∣ b
⊢ φ a ∣ φ b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Result:
case inl
b : ℕ
h : 0 ∣ b
⊢ φ 0 ∣ φ b

case inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
⊢ φ a ∣ φ b
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma Args.numeric_P1 {x y} : (Args.P1 x y).Numeric ↔ x.Numeric ∧ y.Numeric

Proof state:
x y : PGame
⊢ (P1 x y).Numeric ↔ x.Numeric ∧ y.Numeric

Tactic:
simp [Args.Numeric, Args.toMultiset]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Basic.lean
lemma IsCondKernel.isSFiniteKernel (hρ : ρ ≠ 0) : IsSFiniteKernel ρCond

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝ : ρ.IsCondKernel ρCond
hρ : ρ ≠ 0
⊢ IsSFiniteKernel ρCond

Tactic:
contrapose! hρ

Result:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝ : ρ.IsCondKernel ρCond
hρ : ¬IsSFiniteKernel ρCond
⊢ ρ = 0

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝ : ρ.IsCondKernel ρCond
hρ : ¬IsSFiniteKernel ρCond
⊢ ρ = 0

Tactic:
rwa [← ρ.disintegrate ρCond, Measure.compProd_of_not_isSFiniteKernel]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/Basic.lean
@[simp]
lemma mem_zeroLocus_iff {U : Opens X} (s : Set (X.presheaf.obj (op U))) (x : X) :
    x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
simp [zeroLocus]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
/-- Dense sets have small doubling. -/
@[to_additive addConst_le_inv_dens "Dense sets have small doubling."]
lemma mulConst_le_inv_dens : σₘ[A, B] ≤ A.dens⁻¹

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ ↑(#(A * B)) / ↑(#A) ≤ ↑(Fintype.card G) / ↑(#A)

Tactic:
gcongr

Result:
case hab.h
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ #(A * B) ≤ Fintype.card G

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ σₘ[A, B] ≤ A.dens⁻¹

Tactic:
rw [dens, inv_div, mulConst]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ ↑(#(A * B)) / ↑(#A) ≤ ↑(Fintype.card G) / ↑(#A)

Proof state:
case hab.h
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ #(A * B) ≤ Fintype.card G

Tactic:
exact card_le_univ _

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem IsCycle.cycleOf [DecidableRel f.SameCycle] [DecidableEq α]
    (hf : IsCycle f) : cycleOf f x = if f x = x then 1 else f

Proof state:
case pos
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : f x = x
⊢ f.cycleOf x = if f x = x then 1 else f

Tactic:
rwa [if_pos hx, cycleOf_eq_one_iff]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
⊢ f.cycleOf x = if f x = x then 1 else f

Tactic:
by_cases hx : f x = x

Result:
case pos
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : f x = x
⊢ f.cycleOf x = if f x = x then 1 else f

case neg
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : ¬f x = x
⊢ f.cycleOf x = if f x = x then 1 else f

Proof state:
case neg
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : ¬f x = x
⊢ f.cycleOf x = if f x = x then 1 else f

Tactic:
rwa [if_neg hx, hf.cycleOf_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Products/Bifunctor.lean
theorem map_id_comp (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map ((𝟙 W, f ≫ g) : (W, X) ⟶ (W, Z)) =
      F.map ((𝟙 W, f) : (W, X) ⟶ (W, Y)) ≫ F.map ((𝟙 W, g) : (W, Y) ⟶ (W, Z))

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W, f ≫ g) = F.map (𝟙 W, f) ≫ F.map (𝟙 W, g)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.comp_id]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem coevaluation_comp_rightAdjointMate {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) :
    η_ Y (Yᘁ) ≫ _ ◁ (fᘁ) = η_ _ _ ≫ f ▷ _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ Y Yᘁ ≫ Y ◁ fᘁ) =
    (tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ X Xᘁ ≫ f ▷ Xᘁ)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ η_ Y Yᘁ ≫ Y ◁ fᘁ = η_ X Xᘁ ≫ f ▷ Xᘁ

Tactic:
apply_fun (tensorLeftHomEquiv _ Y (Yᘁ) _).symm

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ Y Yᘁ ≫ Y ◁ fᘁ) =
    (tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ X Xᘁ ≫ f ▷ Xᘁ)
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousAt_iSup {f : ι → α → δ} (h : ∀ i, LowerSemicontinuousAt (f i) x) :
    LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x :=
  lowerSemicontinuousAt_ciSup (by simp) h

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
ι : Sort u_3
δ : Type u_4
inst✝ : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem gcd_eq : gcdD a b = gcd a b

Proof state:
case intro.intro.intro.intro.intro.intro
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcdD b = a.gcd b

Tactic:
apply dvd_antisymm

Result:
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcdD b ∣ a.gcd b

case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcd b ∣ a.gcdD b
-- Mathlib/Data/Nat/Cast/Defs.lean
theorem cast_add [AddMonoidWithOne R] (m n : ℕ) : ((m + n : ℕ) : R) = m + n

Proof state:
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑(m + (n + 1)) = ↑m + ↑(n + 1)

Tactic:
rw [add_succ, cast_succ, ih, cast_succ, add_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
⊢ ↑(m + n) = ↑m + ↑n

Tactic:
induction n with
| zero => simp
| succ n ih => rw [add_succ, cast_succ, ih, cast_succ, add_assoc]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ ↑(m + 0) = ↑m + ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_le_sqrt (h : x ≤ y) : √x ≤ √y

Proof state:
x y : ℝ
h : x ≤ y
⊢ x.toNNReal ≤ y.toNNReal

Tactic:
exact toNNReal_le_toNNReal h

Result:
no goals

Proof state:
x y : ℝ
h : x ≤ y
⊢ √x ≤ √y

Tactic:
rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt]

Result:
x y : ℝ
h : x ≤ y
⊢ x.toNNReal ≤ y.toNNReal
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem index_exists {j : ℕ} (h : j < n) : ∃ i : ℕ, j < c.sizeUpTo (i + 1) ∧ i < c.length

Proof state:
n : ℕ
c : Composition n
j : ℕ
h : j < n
⊢ ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length

Tactic:
have n_pos : 0 < n := lt_of_le_of_lt (zero_le j) h

Result:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
⊢ ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length

Proof state:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this✝ : 0 < c.blocks.sum
length_pos : 0 < c.blocks.length
this : c.length - 1 + 1 = c.length
⊢ j < c.sizeUpTo (c.length - 1 + 1)

Tactic:
simp [this, h]

Result:
no goals

Proof state:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
⊢ 0 < c.blocks.sum

Tactic:
rwa [← c.blocks_sum] at n_pos

Result:
no goals

Proof state:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < c.blocks.sum
length_pos : 0 < c.blocks.length
⊢ j < c.sizeUpTo (c.length - 1 + 1)

Tactic:
have : c.length - 1 + 1 = c.length := Nat.succ_pred_eq_of_pos length_pos

Result:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this✝ : 0 < c.blocks.sum
length_pos : 0 < c.blocks.length
this : c.length - 1 + 1 = c.length
⊢ j < c.sizeUpTo (c.length - 1 + 1)

Proof state:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < c.blocks.sum
length_pos : 0 < c.blocks.length
⊢ ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length

Tactic:
refine ⟨c.length - 1, ?_, Nat.pred_lt (ne_of_gt length_pos)⟩

Result:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < c.blocks.sum
length_pos : 0 < c.blocks.length
⊢ j < c.sizeUpTo (c.length - 1 + 1)

Proof state:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
⊢ ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length

Tactic:
have : 0 < c.blocks.sum := by rwa [← c.blocks_sum] at n_pos

Result:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < c.blocks.sum
⊢ ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length

Proof state:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < c.blocks.sum
⊢ ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length

Tactic:
have length_pos : 0 < c.blocks.length := length_pos_of_sum_pos (blocks c) this

Result:
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < c.blocks.sum
length_pos : 0 < c.blocks.length
⊢ ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length
-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- Countable unions of compact sets are σ-compact. -/
lemma isSigmaCompact_sUnion_of_isCompact {S : Set (Set X)} (hc : Set.Countable S)
    (hcomp : ∀ (s : Set X), s ∈ S → IsCompact s) : IsSigmaCompact (⋃₀ S)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
this : Countable ↑S
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
this : Countable ↑S
⊢ IsSigmaCompact (⋃ i, ↑i)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
this : Countable ↑S
⊢ IsSigmaCompact (⋃ i, ↑i)

Tactic:
apply isSigmaCompact_iUnion_of_isCompact _ (fun ⟨s, hs⟩ ↦ hcomp s hs)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
have : Countable S := countable_coe_iff.mpr hc

Result:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
this : Countable ↑S
⊢ IsSigmaCompact (⋃₀ S)
-- Mathlib/Data/PNat/Interval.lean
theorem card_fintype_Ico : Fintype.card (Set.Ico a b) = b - a

Proof state:
a b : ℕ+
⊢ Fintype.card ↑(Set.Ico a b) = ↑b - ↑a

Tactic:
rw [← card_Ico, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma leftHomologyMap_eq [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    leftHomologyMap φ = h₁.leftHomologyIso.hom ≫ γ.φH ≫ h₂.leftHomologyIso.inv

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ = leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ =
    leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φH ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData

Tactic:
rw [← γ.leftHomologyMap'_eq, ← leftHomologyMap'_comp,
  ← leftHomologyMap'_comp, id_comp, comp_id]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ = leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ = h₁.leftHomologyIso.hom ≫ γ.φH ≫ h₂.leftHomologyIso.inv

Tactic:
dsimp [LeftHomologyData.leftHomologyIso, leftHomologyMapIso']

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ =
    leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φH ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData
-- Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean
lemma _root_.IsIntegralClosure.of_isIntegrallyClosedIn
    [Algebra R B] [Algebra A B] [IsScalarTower R A B]
    [IsIntegrallyClosedIn A B] [Algebra.IsIntegral R A] :
    IsIntegralClosure A R B

Proof state:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsIntegrallyClosedIn A B
inst✝ : Algebra.IsIntegral R A
⊢ IsIntegralClosure A R B

Tactic:
refine ⟨IsIntegralClosure.algebraMap_injective _ A _, fun {x} ↦
  ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := A) hx), ?_⟩⟩

Result:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsIntegrallyClosedIn A B
inst✝ : Algebra.IsIntegral R A
x : B
⊢ (∃ y, (algebraMap A B) y = x) → IsIntegral R x

Proof state:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsIntegrallyClosedIn A B
inst✝ : Algebra.IsIntegral R A
x : B
⊢ (∃ y, (algebraMap A B) y = x) → IsIntegral R x

Tactic:
rintro ⟨y, rfl⟩

Result:
case intro
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsIntegrallyClosedIn A B
inst✝ : Algebra.IsIntegral R A
y : A
⊢ IsIntegral R ((algebraMap A B) y)

Proof state:
case intro
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsIntegrallyClosedIn A B
inst✝ : Algebra.IsIntegral R A
y : A
⊢ IsIntegral R ((algebraMap A B) y)

Tactic:
exact IsIntegral.map (IsScalarTower.toAlgHom A A B) (Algebra.IsIntegral.isIntegral y)

Result:
no goals
-- Mathlib/Tactic/NormNum/DivMod.lean
lemma isInt_emod {a b q m a' : ℤ} {b' r : ℕ}
    (ha : IsInt a a') (hb : IsNat b b')
    (hm : q * b' = m) (h : r + m = a') (h₂ : Nat.blt r b' = true) :
    IsNat (a % b) r := ⟨by
  obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb
  simp only [← h, ← hm, Int.add_mul_emod_self]
  rw [Int.emod_eq_of_lt] <;> [simp; simpa using h₂]⟩

Proof state:
a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * ↑b' = m
h : ↑r + m = a'
h₂ : r.blt b' = true
⊢ a % b = ↑r

Tactic:
obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb

Result:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ a % ↑b' = ↑r

Proof state:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ ↑r % ↑b' = ↑r

Tactic:
rw [Int.emod_eq_of_lt] <;> [simp; simpa using h₂]

Result:
no goals

Proof state:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ a % ↑b' = ↑r

Tactic:
simp only [← h, ← hm, Int.add_mul_emod_self]

Result:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ ↑r % ↑b' = ↑r