harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Kaehler/Basic.lean
/-- `Ω[S⁄R]` is trivial if `R → S` is surjective.
Also see `Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential`. -/
lemma KaehlerDifferential.subsingleton_of_surjective (h : Function.Surjective (algebraMap R S)) :
    Subsingleton (Ω[S⁄R])

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Set.range ⇑(D R S) ⊆ ↑⊥

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
x : S
⊢ (D R S) x ∈ ↑⊥

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
x : S
⊢ (D R S) x ∈ ↑⊥

Tactic:
obtain ⟨x, rfl⟩ := h x

Result:
case intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
x : R
⊢ (D R S) ((algebraMap R S) x) ∈ ↑⊥

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ ⊤ ≤ ⊥

Tactic:
rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Set.range ⇑(D R S) ⊆ ↑⊥

Proof state:
case intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
x : R
⊢ (D R S) ((algebraMap R S) x) ∈ ↑⊥

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Subsingleton (Ω[S⁄R])

Tactic:
suffices (⊤ : Submodule S (Ω[S⁄R])) ≤ ⊥ from
  (subsingleton_iff_forall_eq 0).mpr fun y ↦ this trivial

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ ⊤ ≤ ⊥
-- Mathlib/NumberTheory/FLT/Basic.lean
lemma not_fermatLastTheoremFor_one : ¬ FermatLastTheoremFor 1 :=
  fun h ↦ h 1 1 2 (by norm_num) (by norm_num) (by norm_num) (by norm_num)

Proof state:
h : FermatLastTheoremFor 1
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
h : FermatLastTheoremFor 1
⊢ 1 ^ 1 + 1 ^ 1 = 2 ^ 1

Tactic:
norm_num

Result:
no goals

Proof state:
h : FermatLastTheoremFor 1
⊢ 1 ≠ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem cos_sq_arctan (x : ℝ) : cos (arctan x) ^ 2 = 1 / (1 + x ^ 2)

Proof state:
x : ℝ
⊢ cos (arctan x) ^ 2 = 1 / (1 + x ^ 2)

Tactic:
rw_mod_cast [one_div, ← inv_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive]
lemma max_prod_le (l : List α) (f g : α → M) [LinearOrder M]
    [MulLeftMono M] [MulRightMono M] :
    max (l.map f).prod (l.map g).prod ≤ (l.map fun i ↦ max (f i) (g i)).prod

Proof state:
case left.h
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ≤ f i✝ ⊔ g i✝

Tactic:
apply le_max_left

Result:
no goals

Proof state:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ⊔ (map g l).prod ≤ (map (fun i => f i ⊔ g i) l).prod

Tactic:
rw [max_le_iff]

Result:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i => f i ⊔ g i) l).prod ∧ (map g l).prod ≤ (map (fun i => f i ⊔ g i) l).prod

Proof state:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i => f i ⊔ g i) l).prod ∧ (map g l).prod ≤ (map (fun i => f i ⊔ g i) l).prod

Tactic:
constructor <;> apply List.prod_le_prod' <;> intros

Result:
case left.h
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ≤ f i✝ ⊔ g i✝

case right.h
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ f i✝ ⊔ g i✝

Proof state:
case right.h
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ f i✝ ⊔ g i✝

Tactic:
apply le_max_right

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicative.lean
theorem prime_pow_coprime_prod_of_coprime_insert [DecidableEq α] {s : Finset α} (i : α → ℕ) (p : α)
    (hps : p ∉ s) (is_prime : ∀ q ∈ insert p s, Prime q)
    (is_coprime : ∀ᵉ (q ∈ insert p s) (q' ∈ insert p s), q ∣ q' → q = q') :
    IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
⊢ p ∈ s

Tactic:
obtain ⟨q, q_mem', hdq⟩ := hd.exists_mem_multiset_dvd hdprod

Result:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem' : q ∈ Multiset.map (fun p' => p' ^ i p') s.val
hdq : d ∣ q
⊢ p ∈ s

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdp : d ∣ p ^ i p
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
⊢ p ∈ s

Tactic:
replace hdp := hd.dvd_of_dvd_pow hdp

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
⊢ p ∈ s
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem gcd_eq_left {a b : R} : gcd a b = a ↔ a ∣ b :=
  ⟨fun h => by
    rw [← h]
    apply gcd_dvd_right, fun h => by rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]⟩

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = a
⊢ a ∣ b

Tactic:
rw [← h]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = a
⊢ gcd a b ∣ b

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a ∣ b
⊢ gcd a b = a

Tactic:
rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = a
⊢ gcd a b ∣ b

Tactic:
apply gcd_dvd_right

Result:
no goals
-- Mathlib/RingTheory/CotangentLocalizationAway.lean
@[simp]
lemma compLocalizationAwayAlgHom_X_inl : compLocalizationAwayAlgHom T g P (X (Sum.inl ())) =
      IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
⊢ (compLocalizationAwayAlgHom T g P) (X (Sum.inl ())) =
    IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))

Tactic:
simp [compLocalizationAwayAlgHom]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
lemma injective_lift_iff {I : Ideal R} [I.IsTwoSided]
    {f : R →+* S} (H : ∀ (a : R), a ∈ I → f a = 0) :
    Injective (Quotient.lift I f H) ↔ ker f = I

Proof state:
case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f ≤ I → ker f = I

Tactic:
exact fun h ↦ le_antisymm h H

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ Injective ⇑(Quotient.lift I f H) ↔ ker f = I

Tactic:
rw [injective_iff_ker_eq_bot, ker_quotient_lift, map_eq_bot_iff_le_ker, mk_ker]

Result:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f ≤ I ↔ ker f = I

Proof state:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f ≤ I ↔ ker f = I

Tactic:
constructor

Result:
case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f ≤ I → ker f = I

case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f = I → ker f ≤ I

Proof state:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f = I → ker f ≤ I

Tactic:
rintro rfl

Result:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : (ker f).IsTwoSided
H : ∀ a ∈ ker f, f a = 0
⊢ ker f ≤ ker f

Proof state:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : (ker f).IsTwoSided
H : ∀ a ∈ ker f, f a = 0
⊢ ker f ≤ ker f

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_rotateRight_of_lt {x : BitVec w} {r i : Nat} (hr: r < w) :
    (x.rotateRight r).getLsbD i =
      cond (i < w - r)
      (x.getLsbD (r + i))
      (decide (i < w) && x.getLsbD (i - (w - r)))

Proof state:
case neg
w : Nat
x : BitVec w
r i : Nat
hr : r < w
h : ¬i < w - r
⊢ (x.rotateRightAux r).getLsbD i =
    bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))

Tactic:
simp [h, getLsbD_rotateRightAux_of_geq <| Nat.le_of_not_lt h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hr : r < w
⊢ (x.rotateRightAux r).getLsbD i =
    bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))

Tactic:
by_cases h : i < w - r

Result:
case pos
w : Nat
x : BitVec w
r i : Nat
hr : r < w
h : i < w - r
⊢ (x.rotateRightAux r).getLsbD i =
    bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))

case neg
w : Nat
x : BitVec w
r i : Nat
hr : r < w
h : ¬i < w - r
⊢ (x.rotateRightAux r).getLsbD i =
    bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))

Proof state:
case pos
w : Nat
x : BitVec w
r i : Nat
hr : r < w
h : i < w - r
⊢ (x.rotateRightAux r).getLsbD i =
    bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))

Tactic:
simp [h, getLsbD_rotateRightAux_of_le h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hr : r < w
⊢ (x.rotateRight r).getLsbD i =
    bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))

Tactic:
rw [rotateRight_eq_rotateRightAux_of_lt hr]

Result:
w : Nat
x : BitVec w
r i : Nat
hr : r < w
⊢ (x.rotateRightAux r).getLsbD i =
    bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_map_map {L : Type v} [Field L] [Algebra F L] (f : E →ₐ[F] L) :
    relrank (A.map f) (B.map f) = relrank A B

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : E →ₐ[F] L
⊢ (map f A).relrank (map f B) = A.relrank B

Tactic:
simpa only [lift_id] using lift_relrank_map_map A B f

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma memL1_limitProcess_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν]
    (a : α) {s : Set β} (hs : MeasurableSet s) :
    MemLp ((countableFiltration γ).limitProcess
      (fun n x ↦ densityProcess κ ν n a x s) (ν a)) 1 (ν a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (ν a) univ = ↑((ν a) univ).toNNReal

Tactic:
rw [ENNReal.coe_toNNReal]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (ν a) univ ≠ ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) ≤ ↑((ν a) univ).toNNReal

Tactic:
refine (eLpNorm_densityProcess_le hκν n a s).trans_eq ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (ν a) univ = ↑((ν a) univ).toNNReal

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (ν a) univ ≠ ⊤

Tactic:
exact measure_ne_top _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)) 1 (ν a)

Tactic:
refine Submartingale.memLp_limitProcess (martingale_densityProcess hκν a hs).submartingale
  (R := (ν a univ).toNNReal) (fun n ↦ ?_)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) ≤ ↑((ν a) univ).toNNReal
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact
    [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β]
    [TopologicalSpace β] [PseudoMetrizableSpace β] [BorelSpace β] [One β] {f : α → β}
    (hf : Continuous f) {k : Set α} (hk : IsCompact k)
    (h'f : mulSupport f ⊆ k) : StronglyMeasurable f

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : BorelSpace β
inst✝ : One β
f : α → β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ StronglyMeasurable f

Tactic:
rw [stronglyMeasurable_iff_measurable_separable]

Result:
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : BorelSpace β
inst✝ : One β
f : α → β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ Measurable f ∧ IsSeparable (range f)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : BorelSpace β
inst✝ : One β
f : α → β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
⊢ StronglyMeasurable f

Tactic:
letI : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β

Result:
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : BorelSpace β
inst✝ : One β
f : α → β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ StronglyMeasurable f

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OpensMeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : BorelSpace β
inst✝ : One β
f : α → β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ Measurable f ∧ IsSeparable (range f)

Tactic:
exact ⟨hf.measurable, (isCompact_range_of_mulSupport_subset_isCompact hf hk h'f).isSeparable⟩

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem induction_on₂ {β : LocalizedModule S M → LocalizedModule S M → Prop}
    (h : ∀ (m m' : M) (s s' : S), β (mk m s) (mk m' s')) : ∀ x y, β x y

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → LocalizedModule S M → Prop
h : ∀ (m m' : M) (s s' : ↥S), β (mk m s) (mk m' s')
⊢ ∀ (x y : LocalizedModule S M), β x y

Tactic:
rintro ⟨⟨m, s⟩⟩ ⟨⟨m', s'⟩⟩

Result:
case mk.mk.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → LocalizedModule S M → Prop
h : ∀ (m m' : M) (s s' : ↥S), β (mk m s) (mk m' s')
x✝ : LocalizedModule S M
m : M
s : ↥S
y✝ : LocalizedModule S M
m' : M
s' : ↥S
⊢ β (Quot.mk ⇑(r.setoid S M) (m, s)) (Quot.mk ⇑(r.setoid S M) (m', s'))

Proof state:
case mk.mk.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → LocalizedModule S M → Prop
h : ∀ (m m' : M) (s s' : ↥S), β (mk m s) (mk m' s')
x✝ : LocalizedModule S M
m : M
s : ↥S
y✝ : LocalizedModule S M
m' : M
s' : ↥S
⊢ β (Quot.mk ⇑(r.setoid S M) (m, s)) (Quot.mk ⇑(r.setoid S M) (m', s'))

Tactic:
exact h m m' s s'

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem coe_inv_two : ((2⁻¹ : ℝ≥0) : ℝ≥0∞) = 2⁻¹

Proof state:
⊢ ↑2⁻¹ = 2⁻¹

Tactic:
rw [coe_inv _root_.two_ne_zero, coe_two]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_fromBlocks_one₁₁ (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) :
    (Matrix.fromBlocks 1 B C D).det = det (D - C * B)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
this : Invertible 1
⊢ (fromBlocks 1 B C D).det = (D - C * B).det

Tactic:
rw [det_fromBlocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ (fromBlocks 1 B C D).det = (D - C * B).det

Tactic:
haveI : Invertible (1 : Matrix m m α) := invertibleOne

Result:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
this : Invertible 1
⊢ (fromBlocks 1 B C D).det = (D - C * B).det
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_sSup (s : Set ℝ≥0∞) (hs : ∀ r ∈ s, r ≠ ∞) :
    (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)

Proof state:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ⊤
hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ⊤
⊢ (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)

Tactic:
simpa only [← sSup_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iSup hf)

Result:
no goals

Proof state:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ⊤
⊢ (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)

Tactic:
have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs

Result:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ⊤
hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ⊤
⊢ (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem coe_of_s_get?_rat_eq (v_eq_q : v = (↑q : K)) (n : ℕ) :
    (((of q).s.get? n).map (Pair.map (↑)) : Option <| Pair K) = (of v).s.get? n

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) ((of q).s.get? n) = (of v).s.get? n

Tactic:
simp only [of, IntFractPair.seq1, Stream'.Seq.map_get?, Stream'.Seq.get?_tail]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast)
      (Option.map (fun p => { a := 1, b := ↑p.b }) (Stream'.Seq.get? ⟨IntFractPair.stream q, ⋯⟩ (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b }) (Stream'.Seq.get? ⟨IntFractPair.stream v, ⋯⟩ (n + 1))

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))

Tactic:
rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩) <;>
  simp [Stream'.map, Stream'.get, succ_nth_stream_eq]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream v (n + 1))

Tactic:
rw [← IntFractPair.coe_stream'_rat_eq v_eq_q]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast)
      (Option.map (fun p => { a := 1, b := ↑p.b }) (Stream'.Seq.get? ⟨IntFractPair.stream q, ⋯⟩ (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b }) (Stream'.Seq.get? ⟨IntFractPair.stream v, ⋯⟩ (n + 1))

Tactic:
simp only [Stream'.Seq.get?]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream v (n + 1))