harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
theorem op {W : MorphismProperty C} {L : C ⥤ D} (h : W.IsInvertedBy L) : W.op.IsInvertedBy L.op :=
  fun X Y f hf => by
  haveI := h f.unop hf
  dsimp
  infer_instance

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ D
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
⊢ IsIso (L.op.map f)

Tactic:
haveI := h f.unop hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ D
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.op.map f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ D
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.map f.unop).op

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ D
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.op.map f)

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : C ⥤ D
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.map f.unop).op
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem SeqLeft.monotone_seqLeft [LawfulMonad m] (f : γ → m α) (g : γ → m β)
  (hmono₁ : monotone g) (hmono₂ : monotone f) :
    monotone (fun x => g x <* f x)

Proof state:
case hmono₁
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => Function.const α <$> g x

Tactic:
apply Functor.monotone_map

Result:
case hmono₁.hmono
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone g

Proof state:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => Function.const α <$> g x <*> f x

Tactic:
apply Seq.monotone_seq

Result:
case hmono₁
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => Function.const α <$> g x

case hmono₂
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone f

Proof state:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => g x <* f x

Tactic:
simp only [seqLeft_eq]

Result:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => Function.const α <$> g x <*> f x

Proof state:
case hmono₂
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone f

Tactic:
assumption

Result:
no goals

Proof state:
case hmono₁.hmono
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone g

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bitwise_and : bitwise and = land

Proof state:
⊢ bitwise and = land

Tactic:
funext m n

Result:
case h.h
m n : ℤ
⊢ bitwise and m n = m.land n

Proof state:
case h.h.negSucc.ofNat.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && y) = fun a b => a && !b

Tactic:
funext x y

Result:
case h.h.negSucc.ofNat.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && x) = (x && !y)

Proof state:
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y => !x && y) m n) = -[m+1].land (ofNat n)

Tactic:
rw [Nat.bitwise_swap, Function.swap]

Result:
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x => !x && y) n m) = -[m+1].land (ofNat n)

Proof state:
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x => !x && y) n m) = -[m+1].land (ofNat n)

Tactic:
congr

Result:
case h.h.negSucc.ofNat.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && y) = fun a b => a && !b

Proof state:
case h.h
m n : ℤ
⊢ bitwise and m n = m.land n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}
  <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true,
    cond_false, cond_true, lor, Nat.ldiff, Bool.and_true, negSucc.injEq,
    Bool.and_false, Nat.land]

Result:
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y => !x && y) m n) = -[m+1].land (ofNat n)

case h.h.negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise (fun x y => !(!x && !y)) m n+1] = -[m+1].land -[n+1]

Proof state:
case h.h.negSucc.ofNat.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && x) = (x && !y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals

Proof state:
case h.h.negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise (fun x y => !(!x && !y)) m n+1] = -[m+1].land -[n+1]

Tactic:
congr

Result:
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or

Proof state:
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

Tactic:
rfl

Result:
no goals

Proof state:
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or

Tactic:
funext x y

Result:
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)

Proof state:
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_mul_sub_mul {k a b x y : α} (hab : k ∣ a - b) (hxy : k ∣ x - y) :
    k ∣ a * x - b * y

Proof state:
case h.e'_4
α : Type u_1
inst✝ : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * (x - y) + (a - b) * y

Tactic:
rw [mul_sub_left_distrib, mul_sub_right_distrib]

Result:
case h.e'_4
α : Type u_1
inst✝ : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * x - a * y + (a * y - b * y)

Proof state:
case h.e'_4
α : Type u_1
inst✝ : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * x - a * y + (a * y - b * y)

Tactic:
simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ k ∣ a * x - b * y

Tactic:
convert dvd_add (hxy.mul_left a) (hab.mul_right y) using 1

Result:
case h.e'_4
α : Type u_1
inst✝ : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * (x - y) + (a - b) * y
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma disjointOfDiffUnion_subset (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
    ↑(hC.disjointOfDiffUnion hs hI) ⊆ C

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ↑(hC.disjointOfDiffUnion hs hI) ⊆ C

Tactic:
simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton, diff_singleton_subset_iff]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ↑⋯.choose ⊆ insert ∅ C

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ↑(hC.disjointOfDiffUnion hs hI) ⊆ C

Tactic:
classical
simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
exact (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.1.trans (Set.subset_insert _ _)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ↑⋯.choose ⊆ insert ∅ C

Tactic:
exact (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.1.trans (Set.subset_insert _ _)

Result:
no goals
-- Mathlib/Order/CompleteSublattice.lean
theorem coe_sSup' (S : Set L) : (↑(sSup S) : α) = ⨆ N ∈ S, (N : α)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ ↑(sSup S) = ⨆ N ∈ S, ↑N

Tactic:
rw [coe_sSup, ← Set.image, sSup_image]

Result:
no goals
-- Mathlib/Topology/Homotopy/Basic.lean
theorem extend_apply_of_one_le (F : Homotopy f₀ f₁) {t : ℝ} (ht : 1 ≤ t) (x : X) :
    F.extend t x = f₁ x

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ (F.extend t) x = f₁ x

Tactic:
rw [← F.apply_one]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ (F.extend t) x = F (1, x)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ (F.extend t) x = F (1, x)

Tactic:
exact ContinuousMap.congr_fun (Set.IccExtend_of_right_le (zero_le_one' ℝ) F.curry ht) x

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem self_add_star' : a + star a = ↑(2 * a.re)

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a + star a = ↑(2 * a.re)

Tactic:
simp [a.self_add_star', Quaternion.coe]

Result:
no goals
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot (h_le : ∀ n, s n ≤ m0)
    (h_indep : iIndep s κ μα) {t : Set Ω} (ht_tail : MeasurableSet[limsup s atBot] t) :
    ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
a : α
ha : IsProbabilityMeasure (κ a)
⊢ IsFiniteMeasure (κ a)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)

Tactic:
filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
apply measure_eq_zero_or_one_of_indepSet_self' ?_
  ((indep_limsup_atBot_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_inj (h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) : A = B

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * B⁻¹ = 1

Tactic:
refine mul_nonsing_inv _ ?_

Result:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ IsUnit B.det

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * A⁻¹ = 1

Tactic:
rw [h]

Result:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * B⁻¹ = 1

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ IsUnit B.det

Tactic:
rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]

Result:
no goals

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ A = B

Tactic:
refine left_inv_eq_left_inv (mul_nonsing_inv _ h') ?_

Result:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * A⁻¹ = 1
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
lemma sin_sq_lt_sq (hx : x ≠ 0) : sin x ^ 2 < x ^ 2

Proof state:
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ sin x ^ 2 < x ^ 2

Tactic:
exact (sin_sq_le_one _).trans_lt (by rwa [one_lt_sq_iff₀ hx₀.le])

Result:
no goals

Proof state:
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ x ≤ π

Tactic:
linarith [two_le_pi]

Result:
no goals

Proof state:
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ sin x ^ 2 < x ^ 2

Tactic:
exact pow_lt_pow_left₀ (sin_lt hx₀)
  (sin_nonneg_of_nonneg_of_le_pi hx₀.le (by linarith [two_le_pi])) (by simp)

Result:
no goals

Proof state:
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ 2 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
x : ℝ
hx : x ≠ 0
this : ∀ {x : ℝ}, x ≠ 0 → 0 < x → sin x ^ 2 < x ^ 2
hx₀ : ¬0 < x
⊢ sin x ^ 2 < x ^ 2

x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
⊢ sin x ^ 2 < x ^ 2

Tactic:
case inr =>
  simpa using this (neg_ne_zero.2 hx) <| neg_pos_of_neg <| hx.lt_of_le <| le_of_not_lt hx₀

Result:
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
⊢ sin x ^ 2 < x ^ 2

Proof state:
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
⊢ sin x ^ 2 < x ^ 2

Tactic:
rcases le_or_lt x 1 with hxπ | hxπ

Result:
case inl
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ sin x ^ 2 < x ^ 2

case inr
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ sin x ^ 2 < x ^ 2

Proof state:
case inr
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ sin x ^ 2 < x ^ 2

Tactic:
case inr =>
  exact (sin_sq_le_one _).trans_lt (by rwa [one_lt_sq_iff₀ hx₀.le])

Result:
no goals

Proof state:
case inl
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ sin x ^ 2 < x ^ 2

case inr
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ sin x ^ 2 < x ^ 2

Tactic:
case inl =>
  exact pow_lt_pow_left₀ (sin_lt hx₀)
    (sin_nonneg_of_nonneg_of_le_pi hx₀.le (by linarith [two_le_pi])) (by simp)

Result:
case inr
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ sin x ^ 2 < x ^ 2

Proof state:
x : ℝ
hx : x ≠ 0
this : ∀ {x : ℝ}, x ≠ 0 → 0 < x → sin x ^ 2 < x ^ 2
hx₀ : ¬0 < x
⊢ sin x ^ 2 < x ^ 2

Tactic:
simpa using this (neg_ne_zero.2 hx) <| neg_pos_of_neg <| hx.lt_of_le <| le_of_not_lt hx₀

Result:
no goals

Proof state:
x : ℝ
hx : x ≠ 0
⊢ sin x ^ 2 < x ^ 2

Tactic:
wlog hx₀ : 0 < x

Result:
case inr
x : ℝ
hx : x ≠ 0
this : ∀ {x : ℝ}, x ≠ 0 → 0 < x → sin x ^ 2 < x ^ 2
hx₀ : ¬0 < x
⊢ sin x ^ 2 < x ^ 2

x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
⊢ sin x ^ 2 < x ^ 2

Proof state:
x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ 1 < x ^ 2

Tactic:
rwa [one_lt_sq_iff₀ hx₀.le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem denote_mkOrCached {aig : AIG α} {input : BinaryInput aig} :
    ⟦aig.mkOrCached input, assign⟧
      =
    (⟦aig, input.lhs, assign⟧
      ||
     ⟦aig, input.rhs, assign⟧)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkOrCached input⟧ =
    !(!⟦assign, { aig := aig, ref := input.lhs }⟧ && !⟦assign, { aig := aig, ref := input.rhs }⟧)

Tactic:
simp [mkOrCached, LawfulOperator.denote_input_entry (f := mkConstCached)]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkOrCached input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ || ⟦assign, { aig := aig, ref := input.rhs }⟧)

Tactic:
rw [← or_as_aig]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkOrCached input⟧ =
    !(!⟦assign, { aig := aig, ref := input.lhs }⟧ && !⟦assign, { aig := aig, ref := input.rhs }⟧)
-- Mathlib/Topology/UrysohnsLemma.lean
/-- A variation of Urysohn's lemma. In a `T2Space X`, for a closed set `t` and a relatively
compact open set `s` such that `t ⊆ s`, there is a continuous function `f` supported in `s`,
`f x = 1` on `t` and `0 ≤ f x ≤ 1`. -/
lemma exists_tsupport_one_of_isOpen_isClosed [T2Space X] {s t : Set X}
    (hs : IsOpen s) (hscp : IsCompact (closure s)) (ht : IsClosed t) (hst : t ⊆ s) :
    ∃ f : C(X, ℝ), tsupport f ⊆ s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1

Proof state:
case h.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c : Urysohns.CU P := { C := closure u, U := tᶜ, P_C := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
⊢ EqOn c.lim 1 t

Tactic:
intro x hx

Result:
case h.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
c : Urysohns.CU P := { C := closure u, U := tᶜ, P_C := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
x : X
hx : x ∈ t
⊢ c.lim x = 1 x

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
let P : Set X → Prop := fun C => sᶜ ⊆ C

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsOpen s
hscp : IsCompact (closure sᶜᶜ)
ht : IsClosed t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen u
hvIsOpen : IsOpen v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDjsjointuv : u ⊆ vᶜ
huvc : closure u ⊆ vᶜ
P : Set X → Prop := fun C => sᶜ ⊆ C
⊢ ∃ f, tsupport ⇑f ⊆ s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
-- Mathlib/Topology/Algebra/UniformRing.lean
theorem map_smul_eq_mul_coe (r : R) :
    Completion.map (r • ·) = ((algebraMap R A r : Completion A) * ·)

Proof state:
case h
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ Completion.map (fun x => r • x) x = ↑((algebraMap R A) r) * x

Tactic:
refine Completion.induction_on x ?_ fun a => ?_

Result:
case h.refine_1
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ IsClosed {a | Completion.map (fun x => r • x) a = ↑((algebraMap R A) r) * a}

case h.refine_2
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ Completion.map (fun x => r • x) ↑a = ↑((algebraMap R A) r) * ↑a

Proof state:
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
⊢ (Completion.map fun x => r • x) = fun x => ↑((algebraMap R A) r) * x

Tactic:
ext x

Result:
case h
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ Completion.map (fun x => r • x) x = ↑((algebraMap R A) r) * x

Proof state:
case h.refine_2
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ Completion.map (fun x => r • x) ↑a = ↑((algebraMap R A) r) * ↑a

Tactic:
simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]

Result:
no goals

Proof state:
case h.refine_1
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ IsClosed {a | Completion.map (fun x => r • x) a = ↑((algebraMap R A) r) * a}

Tactic:
exact isClosed_eq Completion.continuous_map (continuous_mul_left _)

Result:
no goals