harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
/-- A vector with coprime entries, right-multiplied by a matrix in `SL(2, R)`, has
coprime entries. -/
lemma vecMulSL {v : Fin 2 → R} (hab : IsCoprime (v 0) (v 1)) (A : SL(2, R)) :
    IsCoprime ((v ᵥ* A.1) 0) ((v ᵥ* A.1) 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A : SL(2, R)
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)

Tactic:
obtain ⟨g, hg⟩ := hab.exists_SL2_row 0

Result:
case intro
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
t : Fin 2
⊢ v t = ↑g 0 t

Tactic:
fin_cases t <;> tauto

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
this : v = ↑g 0
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)

Tactic:
simpa only [this] using isCoprime_row (g * A) 0

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)

Tactic:
have : v = g 0 := funext fun t ↦ by { fin_cases t <;> tauto }

Result:
case intro
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
this : v = ↑g 0
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem add_le_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c - b)

Proof state:
a b c : Nat
h : b ≤ c
⊢ (a + b ≤ c) = (a ≤ c - b)

Tactic:
have r := add_le_add_le a 0 h

Result:
a b c : Nat
h : b ≤ c
r : (a + b ≤ 0 + c) = (a ≤ 0 + (c - b))
⊢ (a + b ≤ c) = (a ≤ c - b)

Proof state:
a b c : Nat
h : b ≤ c
r : (a + b ≤ 0 + c) = (a ≤ 0 + (c - b))
⊢ (a + b ≤ c) = (a ≤ c - b)

Tactic:
simp only [Nat.zero_add] at r

Result:
a b c : Nat
h : b ≤ c
r : (a + b ≤ c) = (a ≤ c - b)
⊢ (a + b ≤ c) = (a ≤ c - b)

Proof state:
a b c : Nat
h : b ≤ c
r : (a + b ≤ c) = (a ≤ c - b)
⊢ (a + b ≤ c) = (a ≤ c - b)

Tactic:
exact r

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integrable_cexp_neg_mul_sq_add_real_mul_I (hb : 0 < b.re) (c : ℝ) :
    Integrable fun x : ℝ => cexp (-b * (x + c * I) ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun x => cexp (-b * (↑x + ↑c * I) ^ 2)) volume

Tactic:
rw [← hasFiniteIntegral_norm_iff]

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a => ‖cexp (-b * (↑a + ↑c * I) ^ 2)‖) volume

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x => rexp (-(b.re * x ^ 2))) volume

Tactic:
simp_rw [← neg_mul]

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x => rexp (-b.re * x ^ 2)) volume

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x => rexp (-b.re * x ^ 2)) volume

Tactic:
apply integrable_exp_neg_mul_sq hb

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a => ‖cexp (-b * (↑a + ↑c * I) ^ 2)‖) volume

Tactic:
simp_rw [norm_cexp_neg_mul_sq_add_mul_I' hb.ne', neg_sub _ (c ^ 2 * _),
  sub_eq_add_neg _ (b.re * _), Real.exp_add]

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a => rexp (c ^ 2 * (b.im ^ 2 / b.re + b.re)) * rexp (-(b.re * (a - b.im * c / b.re) ^ 2)))
    volume

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x => cexp (-b * (↑x + ↑c * I) ^ 2)) volume

Tactic:
refine
  ⟨(Complex.continuous_exp.comp
        (continuous_const.mul
          ((continuous_ofReal.add continuous_const).pow 2))).aestronglyMeasurable,
    ?_⟩

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun x => cexp (-b * (↑x + ↑c * I) ^ 2)) volume

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
this : Integrable (fun x => rexp (-(b.re * x ^ 2))) volume
⊢ HasFiniteIntegral (fun a => rexp (c ^ 2 * (b.im ^ 2 / b.re + b.re)) * rexp (-(b.re * (a - b.im * c / b.re) ^ 2)))
    volume

Tactic:
exact (Integrable.comp_sub_right this (b.im * c / b.re)).hasFiniteIntegral.const_mul _

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a => rexp (c ^ 2 * (b.im ^ 2 / b.re + b.re)) * rexp (-(b.re * (a - b.im * c / b.re) ^ 2)))
    volume

Tactic:
suffices Integrable fun x : ℝ => exp (-(b.re * x ^ 2)) by
  exact (Integrable.comp_sub_right this (b.im * c / b.re)).hasFiniteIntegral.const_mul _

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x => rexp (-(b.re * x ^ 2))) volume
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
/-- Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic)
to the multiplicative integers, or is densely ordered, exclusively. -/
@[to_additive existing]
lemma LinearOrderedCommGroup.discrete_iff_not_denselyOrdered :
    Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬ DenselyOrdered G

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ Nonempty (Additive G ≃+o ℤ)

Tactic:
refine Nonempty.congr ?_ ?_ <;> intro f

Result:
case refine_1
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
f : G ≃*o Multiplicative ℤ
⊢ Additive G ≃+o ℤ

case refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
f : Additive G ≃+o ℤ
⊢ G ≃*o Multiplicative ℤ

Proof state:
case refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
f : Additive G ≃+o ℤ
⊢ G ≃*o Multiplicative ℤ

Tactic:
exact ⟨MulEquiv.toAdditive'.symm f, by simp⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G

Tactic:
let e : G ≃o Additive G := OrderIso.refl G

Result:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
f : Additive G ≃+o ℤ
⊢ ∀ {a b : G}, (MulEquiv.toAdditive'.symm ↑f).toFun a ≤ (MulEquiv.toAdditive'.symm ↑f).toFun b ↔ a ≤ b

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G

Tactic:
rw [denselyOrdered_iff_of_orderIsoClass e,
  ← LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered (Additive G)]

Result:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ Nonempty (Additive G ≃+o ℤ)

Proof state:
case refine_1
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
f : G ≃*o Multiplicative ℤ
⊢ Additive G ≃+o ℤ

Tactic:
exact ⟨MulEquiv.toAdditive' f, by simp⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
f : G ≃*o Multiplicative ℤ
⊢ ∀ {a b : Additive G}, (MulEquiv.toAdditive' ↑f).toFun a ≤ (MulEquiv.toAdditive' ↑f).toFun b ↔ a ≤ b

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem isInitial_zero : IsInitial 0

Proof state:
⊢ IsInitial 0

Tactic:
exact_mod_cast isInitial_natCast 0

Result:
no goals
-- Mathlib/Algebra/Category/CoalgebraCat/Basic.lean
lemma Hom.toCoalgHom_injective (V W : CoalgebraCat.{v} R) :
    Function.Injective (Hom.toCoalgHom' : Hom V W → _) :=
  fun ⟨f⟩ ⟨g⟩ _ => by congr

Proof state:
R : Type u
inst✝ : CommRing R
V W : CoalgebraCat R
x✝² x✝¹ : V.Hom W
f g : ↑V.toModuleCat →ₗc[R] ↑W.toModuleCat
x✝ : { toCoalgHom' := f }.toCoalgHom' = { toCoalgHom' := g }.toCoalgHom'
⊢ { toCoalgHom' := f } = { toCoalgHom' := g }

Tactic:
congr

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coe_eq_one_iff : (φ : PowerSeries R) = 1 ↔ φ = 1

Proof state:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
⊢ ↑φ = 1 ↔ φ = 1

Tactic:
rw [← coe_one, coe_inj]

Result:
no goals
-- Mathlib/Data/Finset/Interval.lean
theorem Icc_eq_image_powerset (h : s ⊆ t) : Icc s t = (t \ s).powerset.image (s ∪ ·)

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ u ∈ Icc s t ↔ u ∈ image (fun x => s ∪ x) (t \ s).powerset

Tactic:
simp_rw [mem_Icc, mem_image, mem_powerset]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u ≤ t ↔ ∃ a ⊆ t \ s, s ∪ a = u

Proof state:
case h.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊆ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v ≤ t

Tactic:
exact ⟨le_sup_left, union_subset h <| hv.trans sdiff_subset⟩

Result:
no goals

Proof state:
case h.mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u ≤ t → ∃ a ⊆ t \ s, s ∪ a = u

Tactic:
rintro ⟨hs, ht⟩

Result:
case h.mp.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u ≤ t
⊢ ∃ a ⊆ t \ s, s ∪ a = u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Icc s t = image (fun x => s ∪ x) (t \ s).powerset

Tactic:
ext u

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ u ∈ Icc s t ↔ u ∈ image (fun x => s ∪ x) (t \ s).powerset

Proof state:
case h.mp.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u ≤ t
⊢ ∃ a ⊆ t \ s, s ∪ a = u

Tactic:
exact ⟨u \ s, sdiff_le_sdiff_right ht, sup_sdiff_cancel_right hs⟩

Result:
no goals

Proof state:
case h.mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ (∃ a ⊆ t \ s, s ∪ a = u) → s ≤ u ∧ u ≤ t

Tactic:
rintro ⟨v, hv, rfl⟩

Result:
case h.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊆ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v ≤ t

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u ≤ t ↔ ∃ a ⊆ t \ s, s ∪ a = u

Tactic:
constructor

Result:
case h.mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u ≤ t → ∃ a ⊆ t \ s, s ∪ a = u

case h.mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ (∃ a ⊆ t \ s, s ∪ a = u) → s ≤ u ∧ u ≤ t
-- Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean
theorem dfinsuppFamily_zero :
    dfinsuppFamily (0 : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) = 0

Proof state:
case H.h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
x✝ : (i : ι) → Π₀ (j : κ i), M i j
i✝ : (i : ι) → κ i
⊢ ((dfinsuppFamily 0) x✝) i✝ = (0 x✝) i✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
⊢ dfinsuppFamily 0 = 0

Tactic:
ext

Result:
case H.h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
x✝ : (i : ι) → Π₀ (j : κ i), M i j
i✝ : (i : ι) → κ i
⊢ ((dfinsuppFamily 0) x✝) i✝ = (0 x✝) i✝
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
lemma norm_mahlerTerm : ‖(mahlerTerm a n : C(ℤ_[p], E))‖ = ‖a‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ_[p] E
a : E
n : ℕ
⊢ ‖mahlerTerm a n‖ = ‖a‖

Tactic:
simp only [mahlerTerm, ContinuousMap.norm_smul_const, norm_mahler_eq, one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/CoherentTopology.lean
theorem coherentTopology.mem_sieves_of_hasEffectiveEpiFamily (S : Sieve X) :
    (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
      EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a)) ) →
        (S ∈ (coherentTopology C) X)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) → S ∈ (coherentTopology C) X

Tactic:
intro ⟨α, _, Y, π, hπ⟩

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ (coherentTopology C) X

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows

Tactic:
exact fun _ _ h ↦ by cases h; exact hπ.2 _

Result:
no goals

Proof state:
case hR
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (coherentCoverage C).covering X

Tactic:
exact ⟨_, inferInstance, Y, π, rfl, hπ.1⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ (coherentTopology C) X

Tactic:
apply (coherentCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows

case hR
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (coherentCoverage C).covering X

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : x✝ ∈ Presieve.ofArrows Y π
⊢ x✝ ∈ S.arrows

Tactic:
cases h

Result:
case mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ π i✝ ∈ S.arrows

Proof state:
case mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ π i✝ ∈ S.arrows

Tactic:
exact hπ.2 _

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
theorem Module.End.iSup_genEigenspace_restrict_eq_top
    {p : Submodule K V} {f : Module.End K V} [FiniteDimensional K V]
    (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ μ, ⨆ k : ℕ, f.genEigenspace μ k = ⊤) :
    ⨆ μ, ⨆ k : ℕ, Module.End.genEigenspace (LinearMap.restrict f h) μ k = ⊤

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, ⨆ k, (f.genEigenspace μ) ↑k = ⊤
⊢ ⨆ μ, ⨆ k, (genEigenspace (LinearMap.restrict f h) μ) ↑k = ⊤

Tactic:
simp_rw [iSup_genEigenspace_eq] at h' ⊢

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, f.maxGenEigenspace μ = ⊤
⊢ ⨆ μ, maxGenEigenspace (LinearMap.restrict f h) μ = ⊤

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, f.maxGenEigenspace μ = ⊤
⊢ ⨆ μ, maxGenEigenspace (LinearMap.restrict f h) μ = ⊤

Tactic:
apply Module.End.genEigenspace_restrict_eq_top h h'

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_div_eq_mul_div : a / (b / c) = a * c / b

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b c : α
⊢ a / (b / c) = a * c / b

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem mem_chart_target_iff (p : H × E) (q : TM) :
    p ∈ (chartAt (ModelProd H E) q).target ↔ p.1 ∈ (chartAt H q.1).target

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
p : H × E
q : TM
⊢ p.1 ∈ (chartAt H q.proj).target ∧
      (↑((chartAt H q.proj).symm.prod (PartialEquiv.refl E).symm) p).1 ∈ (chartAt H q.proj).source ↔
    p.1 ∈ (chartAt H q.proj).target

Tactic:
simp +contextual only [and_iff_left_iff_imp, mfld_simps]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
p : H × E
q : TM
⊢ p.1 ∈ (chartAt H q.proj).target ∧
      (↑((chartAt H q.proj).prod (PartialEquiv.refl E)).symm p).1 ∈ (chartAt H q.proj).source ↔
    p.1 ∈ (chartAt H q.proj).target

Tactic:
rw [PartialEquiv.prod_symm]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
p : H × E
q : TM
⊢ p.1 ∈ (chartAt H q.proj).target ∧
      (↑((chartAt H q.proj).symm.prod (PartialEquiv.refl E).symm) p).1 ∈ (chartAt H q.proj).source ↔
    p.1 ∈ (chartAt H q.proj).target

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
p : H × E
q : TM
⊢ p ∈ (chartAt (ModelProd H E) q).target ↔ p.1 ∈ (chartAt H q.proj).target

Tactic:
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
p : H × E
q : TM
⊢ p.1 ∈ (chartAt H q.proj).target ∧
      (↑((chartAt H q.proj).prod (PartialEquiv.refl E)).symm p).1 ∈ (chartAt H q.proj).source ↔
    p.1 ∈ (chartAt H q.proj).target
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive two_nsmul_sup_eq_add_add_abs_sub]
lemma sup_sq_eq_mul_mul_mabs_div (a b : α) : (a ⊔ b) ^ 2 = a * b * |b / a|ₘ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = a * b * mabs (b / a)

Tactic:
rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
   mul_assoc, ← pow_two, inv_mul_cancel_left]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem add_one_lt_exp_of_pos {x : ℝ} (hx : 0 < x) : x + 1 < exp x :=
  (by nlinarith : x + 1 < 1 + x + x ^ 2 / 2).trans_le (quadratic_le_exp_of_nonneg hx.le)

Proof state:
x : ℝ
hx : 0 < x
⊢ x + 1 < 1 + x + x ^ 2 / 2

Tactic:
nlinarith

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
⊢ x + 1 < 1 + x + x ^ 2 / 2

Tactic:
nlinarith

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
@[simp] lemma essSup_count_eq_ciSup (hf : BddAbove (Set.range f)) :
    essSup f .count = ⨆ a, f a := essSup_eq_ciSup (by simp) hf

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝² : ConditionallyCompleteLattice β
f : α → β
inst✝¹ : Nonempty α
inst✝ : MeasurableSingletonClass α
hf : BddAbove (range f)
⊢ ∀ (a : α), Measure.count {a} ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleTransform.lean
theorem continuousOn_prod_circle_transform_function {R r : ℝ} (hr : r < R) {z : ℂ} :
    ContinuousOn (fun w : ℂ × ℝ => (circleMap z R w.snd - w.fst)⁻¹ ^ 2)
      (closedBall z r ×ˢ univ)

Proof state:
case hf.h₀.mk.intro
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
⊢ circleMap z R (a, b).2 - (a, b).1 ≠ 0

Tactic:
have ha2 : a ∈ ball z R := closedBall_subset_ball hr ha

Result:
case hf.h₀.mk.intro
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
ha2 : a ∈ ball z R
⊢ circleMap z R (a, b).2 - (a, b).1 ≠ 0

Proof state:
case hf.h₀.mk.intro
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
ha2 : a ∈ ball z R
⊢ circleMap z R (a, b).2 - (a, b).1 ≠ 0

Tactic:
exact sub_ne_zero.2 (circleMap_ne_mem_ball ha2 b)

Result:
no goals

Proof state:
case hf.hg
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap z R x.2 - x.1) (closedBall z r ×ˢ univ)

Tactic:
exact ((continuous_circleMap z R).comp_continuousOn continuousOn_snd).sub continuousOn_fst

Result:
no goals

Proof state:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w => (1 / (circleMap z R w.2 - w.1)) ^ 2) (closedBall z r ×ˢ univ)

Tactic:
apply_rules [ContinuousOn.pow, ContinuousOn.div, continuousOn_const]

Result:
case hf.hg
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap z R x.2 - x.1) (closedBall z r ×ˢ univ)

case hf.h₀
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ x ∈ closedBall z r ×ˢ univ, circleMap z R x.2 - x.1 ≠ 0

Proof state:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w => (circleMap z R w.2 - w.1)⁻¹ ^ 2) (closedBall z r ×ˢ univ)

Tactic:
simp_rw [← one_div]

Result:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w => (1 / (circleMap z R w.2 - w.1)) ^ 2) (closedBall z r ×ˢ univ)

Proof state:
case hf.h₀
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ x ∈ closedBall z r ×ˢ univ, circleMap z R x.2 - x.1 ≠ 0

Tactic:
rintro ⟨a, b⟩ ⟨ha, -⟩

Result:
case hf.h₀.mk.intro
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
⊢ circleMap z R (a, b).2 - (a, b).1 ≠ 0
-- Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
theorem IsTranscendenceBasis.nonempty_iff_transcendental [Nontrivial R]
    (hx : IsTranscendenceBasis R x) :
    Nonempty ι ↔ Algebra.Transcendental R A

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ Nonempty ι ↔ Algebra.Transcendental R A

Tactic:
rw [← not_isEmpty_iff, Algebra.transcendental_iff_not_isAlgebraic, hx.isEmpty_iff_isAlgebraic]

Result:
no goals