harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Localization.lean
lemma Qh_inverts_quasiIso : (HomotopyCategory.quasiIso C c).IsInvertedBy Qh

Proof state:
case mk.mk.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ HomotopyCategory.quasiIso C c ((HomotopyCategory.quotient C c).map φ) →
    IsIso (Qh.map ((HomotopyCategory.quotient C c).map φ))

Tactic:
rw [HomotopyCategory.quotient_map_mem_quasiIso_iff φ,
  ← HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso]

Result:
case mk.mk.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ IsIso (Q.map φ) → IsIso (Qh.map ((HomotopyCategory.quotient C c).map φ))

Proof state:
case mk.mk
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
φ : { as := K } ⟶ { as := L }
⊢ HomotopyCategory.quasiIso C c φ → IsIso (Qh.map φ)

Tactic:
obtain ⟨φ, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ

Result:
case mk.mk.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ HomotopyCategory.quasiIso C c ((HomotopyCategory.quotient C c).map φ) →
    IsIso (Qh.map ((HomotopyCategory.quotient C c).map φ))

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
⊢ (HomotopyCategory.quasiIso C c).IsInvertedBy Qh

Tactic:
rintro ⟨K⟩ ⟨L⟩ φ

Result:
case mk.mk
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
φ : { as := K } ⟶ { as := L }
⊢ HomotopyCategory.quasiIso C c φ → IsIso (Qh.map φ)

Proof state:
case mk.mk.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ IsIso (Q.map φ) → IsIso (Qh.map ((HomotopyCategory.quotient C c).map φ))

Tactic:
exact (NatIso.isIso_map_iff (quotientCompQhIso C c) φ).2

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
/--
Explicit formula for `toCircle j`. Note that this is "evil" because it uses `ZMod.val`. Where
possible, it is recommended to lift `j` to `ℤ` and use `toAddCircle_intCast` instead.
-/
lemma toAddCircle_apply (j : ZMod N) :
    toAddCircle j = ↑(j.val / N : ℝ)

Proof state:
N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ toAddCircle j = ↑(↑j.val / ↑N)

Tactic:
rw [← toAddCircle_natCast, natCast_zmod_val]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Lemmas.lean
theorem cast_inv_int (n : ℤ) : ((n⁻¹ : ℚ) : α) = (n : α)⁻¹

Proof state:
case negSucc
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.negSucc n))⁻¹ = (↑(Int.negSucc n))⁻¹

Tactic:
simp only [ofInt_eq_cast, Int.cast_negSucc, ← Nat.cast_succ, cast_neg, inv_neg, cast_inv_nat]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹

Tactic:
rcases n with n | n

Result:
case ofNat
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.ofNat n))⁻¹ = (↑(Int.ofNat n))⁻¹

case negSucc
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.negSucc n))⁻¹ = (↑(Int.negSucc n))⁻¹

Proof state:
case ofNat
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.ofNat n))⁻¹ = (↑(Int.ofNat n))⁻¹

Tactic:
simp [ofInt_eq_cast, cast_inv_nat]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem sInter_polar_finite_subset_eq_polar (s : Set E) :
    ⋂₀ (B.polar '' { F | F.Finite ∧ F ⊆ s }) = B.polar s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ ⋂₀ (B.polar '' {F | F.Finite ∧ F ⊆ s}) = B.polar s

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
⊢ x ∈ ⋂₀ (B.polar '' {F | F.Finite ∧ F ⊆ s}) ↔ x ∈ B.polar s

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
hx : ∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i
a : E
ha : a ∈ s
⊢ ‖(B a) x‖ ≤ 1

Tactic:
simpa [mem_polar_singleton] using hx _ (Set.finite_singleton a) (Set.singleton_subset_iff.mpr ha)

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
⊢ x ∈ ⋂₀ (B.polar '' {F | F.Finite ∧ F ⊆ s}) ↔ x ∈ B.polar s

Tactic:
simp only [Set.sInter_image, Set.mem_setOf_eq, Set.mem_iInter, and_imp]

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
⊢ (∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i) ↔ x ∈ B.polar s

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
⊢ (∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i) ↔ x ∈ B.polar s

Tactic:
refine ⟨fun hx a ha ↦ ?_, fun hx F _ hF₂ => polar_antitone _ hF₂ hx⟩

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
hx : ∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i
a : E
ha : a ∈ s
⊢ ‖(B a) x‖ ≤ 1
-- Mathlib/Combinatorics/Pigeonhole.lean
theorem exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum (hf : ∀ a ∈ s, f a ∈ t)
    (hb : #t • b < ∑ x ∈ s, w x) : ∃ y ∈ t, b < ∑ x ∈ s with f x = y, w x :=
  exists_lt_of_sum_lt <| by simpa only [sum_fiberwise_of_maps_to hf, sum_const]

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst✝ : LinearOrderedCancelAddCommMonoid M
hf : ∀ a ∈ s, f a ∈ t
hb : #t • b < ∑ x ∈ s, w x
⊢ ∑ i ∈ t, b < ∑ i ∈ t, ∑ x ∈ filter (fun x => f x = i) s, w x

Tactic:
simpa only [sum_fiberwise_of_maps_to hf, sum_const]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuousOn_iInf_dom {u : κ → UniformSpace β'} {F : ι → β' → α}
    {S : Set β'} {k : κ} (hk : UniformEquicontinuousOn (uβ := u k) F S) :
    UniformEquicontinuousOn (uβ := ⨅ k, u k) F S

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (⇑ofFun ∘ swap F) S
⊢ Tendsto (fun x => ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β' ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))

Tactic:
rw [iInf_uniformity]

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (⇑ofFun ∘ swap F) S
⊢ Tendsto (fun x => ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) ((⨅ i, 𝓤 β') ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (⇑ofFun ∘ swap F) S
⊢ UniformContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
unfold UniformContinuousOn

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (⇑ofFun ∘ swap F) S
⊢ Tendsto (fun x => ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β' ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn F S

Tactic:
simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uβ := _)] at hk ⊢

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (⇑ofFun ∘ swap F) S
⊢ UniformContinuousOn (⇑ofFun ∘ swap F) S

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (⇑ofFun ∘ swap F) S
⊢ Tendsto (fun x => ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) ((⨅ i, 𝓤 β') ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))

Tactic:
exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem insert_union {a} {b : β a} {s₁ s₂ : Finmap β} : insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂ :=
  induction_on₂ s₁ s₂ fun a₁ a₂ => by simp [AList.insert_union]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : Finmap β
a₁ a₂ : AList β
⊢ insert a b (⟦a₁⟧ ∪ ⟦a₂⟧) = insert a b ⟦a₁⟧ ∪ ⟦a₂⟧

Tactic:
simp [AList.insert_union]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem le_inf (f' f g : α →ₘ[μ] β) (hf : f' ≤ f) (hg : f' ≤ g) : f' ≤ f ⊓ g

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᶠ[ae μ] ↑f
hg : ↑f' ≤ᶠ[ae μ] ↑g
⊢ ↑f' ≤ᶠ[ae μ] ↑(f ⊓ g)

Tactic:
filter_upwards [hf, hg, coeFn_inf f g] with _ haf hag ha_inf

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᶠ[ae μ] ↑f
hg : ↑f' ≤ᶠ[ae μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑(f ⊓ g) a✝

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᶠ[ae μ] ↑f
hg : ↑f' ≤ᶠ[ae μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑(f ⊓ g) a✝

Tactic:
rw [ha_inf]

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᶠ[ae μ] ↑f
hg : ↑f' ≤ᶠ[ae μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑f a✝ ⊓ ↑g a✝

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᶠ[ae μ] ↑f
hg : ↑f' ≤ᶠ[ae μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑f a✝ ⊓ ↑g a✝

Tactic:
exact le_inf haf hag

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : f' ≤ f
hg : f' ≤ g
⊢ f' ≤ f ⊓ g

Tactic:
rw [← coeFn_le] at hf hg ⊢

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᶠ[ae μ] ↑f
hg : ↑f' ≤ᶠ[ae μ] ↑g
⊢ ↑f' ≤ᶠ[ae μ] ↑(f ⊓ g)
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem kernel_eq_kernel [HasKernels V] {i j j' : ι} (r : c.Rel i j) (r' : c.Rel i j') :
    kernelSubobject (C.d i j) = kernelSubobject (C.d i j')

Proof state:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
⊢ kernelSubobject (C.d i j) = kernelSubobject (C.d i j')

Tactic:
rw [← d_comp_eqToHom C r r']

Result:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
⊢ kernelSubobject (C.d i j' ≫ eqToHom ⋯) = kernelSubobject (C.d i j')

Proof state:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
⊢ kernelSubobject (C.d i j' ≫ eqToHom ⋯) = kernelSubobject (C.d i j')

Tactic:
apply kernelSubobject_comp_mono

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem half_lt_self (hz : a ≠ 0) (ht : a ≠ ∞) : a / 2 < a

Proof state:
case intro
a : ℝ≥0
hz : a ≠ 0
⊢ a / 2 < a

case intro
a : ℝ≥0
hz : a ≠ 0
⊢ 2 ≠ 0

Tactic:
exacts [NNReal.half_lt_self hz, two_ne_zero' _]

Result:
no goals

Proof state:
case intro
a : ℝ≥0
hz : ↑a ≠ 0
⊢ ↑a / 2 < ↑a

Tactic:
rw [coe_ne_zero] at hz

Result:
case intro
a : ℝ≥0
hz : a ≠ 0
⊢ ↑a / 2 < ↑a

Proof state:
a : ℝ≥0∞
hz : a ≠ 0
ht : a ≠ ⊤
⊢ a / 2 < a

Tactic:
lift a to ℝ≥0 using ht

Result:
case intro
a : ℝ≥0
hz : ↑a ≠ 0
⊢ ↑a / 2 < ↑a

Proof state:
case intro
a : ℝ≥0
hz : a ≠ 0
⊢ ↑a / 2 < ↑a

Tactic:
rw [← coe_two, ← coe_div, coe_lt_coe]

Result:
case intro
a : ℝ≥0
hz : a ≠ 0
⊢ a / 2 < a

case intro
a : ℝ≥0
hz : a ≠ 0
⊢ 2 ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Bitwise/Lemmas.lean
theorem shiftRight_add (i : Int) (m n : Nat) :
    i >>> (m + n) = i >>> m >>> n

Proof state:
i : Int
m n : Nat
⊢ (match i, m + n with
    | ofNat n, s => ofNat (n >>> s)
    | -[n+1], s => -[n >>> s+1]) =
    match
      match i, m with
      | ofNat n, s => ofNat (n >>> s)
      | -[n+1], s => -[n >>> s+1],
      n with
    | ofNat n, s => ofNat (n >>> s)
    | -[n+1], s => -[n >>> s+1]

Tactic:
cases i <;> simp [Nat.shiftRight_add]

Result:
no goals

Proof state:
i : Int
m n : Nat
⊢ i >>> (m + n) = i >>> m >>> n

Tactic:
simp only [shiftRight_eq, Int.shiftRight]

Result:
i : Int
m n : Nat
⊢ (match i, m + n with
    | ofNat n, s => ofNat (n >>> s)
    | -[n+1], s => -[n >>> s+1]) =
    match
      match i, m with
      | ofNat n, s => ofNat (n >>> s)
      | -[n+1], s => -[n >>> s+1],
      n with
    | ofNat n, s => ofNat (n >>> s)
    | -[n+1], s => -[n >>> s+1]
-- Mathlib/Topology/Connected/LocPathConnected.lean
theorem LocPathConnectedSpace.of_bases {p : X → ι → Prop} {s : X → ι → Set X}
    (h : ∀ x, (𝓝 x).HasBasis (p x) (s x)) (h' : ∀ x i, p x i → IsPathConnected (s x i)) :
    LocPathConnectedSpace X where
  path_connected_basis x

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
i : ι
hpi : p x i
hi : s x i ⊆ t
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Tactic:
exact ⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Tactic:
rcases (h x).mem_iff.mp ht with ⟨i, hpi, hi⟩

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
i : ι
hpi : p x i
hi : s x i ⊆ t
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
⊢ (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id

Tactic:
rw [hasBasis_self]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Tactic:
intro t ht

Result:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t
-- Mathlib/Analysis/Matrix.lean
@[simp] lemma linfty_opNNNorm_toMatrix (f : (n → α) →L[α] (m → α)) :
    ‖LinearMap.toMatrix' (↑f : (n → α) →ₗ[α] (m → α))‖₊ = ‖f‖₊

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NontriviallyNormedField α
inst✝¹ : NormedAlgebra ℝ α
inst✝ : DecidableEq n
f : (n → α) →L[α] m → α
⊢ ‖{ toLinearMap := (LinearMap.toMatrix' ↑f).mulVecLin, cont := ⋯ }‖₊ = ‖f‖₊

Tactic:
simp only [← toLin'_apply', toLin'_toMatrix']

Result:
no goals

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NontriviallyNormedField α
inst✝¹ : NormedAlgebra ℝ α
inst✝ : DecidableEq n
f : (n → α) →L[α] m → α
⊢ ‖LinearMap.toMatrix' ↑f‖₊ = ‖f‖₊

Tactic:
rw [linfty_opNNNorm_eq_opNNNorm]

Result:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NontriviallyNormedField α
inst✝¹ : NormedAlgebra ℝ α
inst✝ : DecidableEq n
f : (n → α) →L[α] m → α
⊢ ‖{ toLinearMap := (LinearMap.toMatrix' ↑f).mulVecLin, cont := ⋯ }‖₊ = ‖f‖₊
-- Mathlib/Data/Rat/Floor.lean
theorem isInt_intCeil_ofIsRat (r : α) (n : ℤ) (d : ℕ) :
    IsRat r n d → IsInt ⌈r⌉ (-(-n / d))

Proof state:
case mk
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ IsInt ⌈↑n * ⅟↑d⌉ (-(-n / ↑d))

Tactic:
constructor

Result:
case mk.out
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n * ⅟↑d⌉ = ↑(-(-n / ↑d))

Proof state:
case mk.out
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n / ↑d⌉ = -(-n / ↑d)

Tactic:
rw [← ceil_intCast_div_natCast n d, ← ceil_cast (α := α), Rat.cast_div,
  cast_intCast, cast_natCast]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
r : α
n : ℤ
d : ℕ
⊢ IsRat r n d → IsInt ⌈r⌉ (-(-n / ↑d))

Tactic:
rintro ⟨inv, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ IsInt ⌈↑n * ⅟↑d⌉ (-(-n / ↑d))

Proof state:
case mk.out
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n * ⅟↑d⌉ = ↑(-(-n / ↑d))

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]

Result:
case mk.out
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n / ↑d⌉ = -(-n / ↑d)
-- Mathlib/Data/Rel.lean
theorem core_id (s : Set α) : core (@Eq α) s = s

Proof state:
α : Type u_1
s : Set α
⊢ core Eq s = s

Tactic:
simp [core]

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
@[reassoc (attr := simp)]
lemma pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk
    (f : X ⟶ Y) (F : Y.Presheaf C) (V : (Opens Y)ᵒᵖ) (x : X) (hx : f x ∈ V.unop) :
    ((pushforwardPullbackAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F _ x hx =
      F.germ _ (f x) hx

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
V : (Opens ↑Y)ᵒᵖ
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ unop V
⊢ ((pushforwardPullbackAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F ((Opens.map f).obj (unop V)) x hx =
    F.germ (unop V) ((ConcreteCategory.hom f) x) hx

Tactic:
simpa using pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk
  C f F ((Opens.map f).obj V.unop) x hx V.unop (by rfl)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
V : (Opens ↑Y)ᵒᵖ
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ unop V
⊢ (Opens.map f).obj (unop V) ≤ (Opens.map f).obj (unop V)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Noetherian.lean
theorem exists_simple_subobject {X : C} [ArtinianObject X] (h : ¬IsZero X) :
    ∃ Y : Subobject X, Simple (Y : C)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this : Nontrivial (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)

Tactic:
haveI := isAtomic_of_orderBot_wellFounded_lt (ArtinianObject.subobject_lt_wellFounded X)

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)

Tactic:
obtain ⟨Y, s⟩ := (IsAtomic.eq_bot_or_exists_atom_le (⊤ : Subobject X)).resolve_left top_ne_bot

Result:
case intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
Y : Subobject X
s : IsAtom Y ∧ Y ≤ ⊤
⊢ ∃ Y, Simple (underlying.obj Y)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
⊢ ∃ Y, Simple (underlying.obj Y)

Tactic:
haveI : Nontrivial (Subobject X) := nontrivial_of_not_isZero h

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this : Nontrivial (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)

Proof state:
case intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
Y : Subobject X
s : IsAtom Y ∧ Y ≤ ⊤
⊢ ∃ Y, Simple (underlying.obj Y)

Tactic:
exact ⟨Y, (subobject_simple_iff_isAtom _).mpr s.1⟩

Result:
no goals