harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Preserves/Finite.lean
/-- We can always derive `PreservesFiniteColimits C`
by showing that we are preserving colimits at an arbitrary universe. -/
lemma preservesFiniteColimits_of_preservesFiniteColimitsOfSize (F : C ⥤ D)
    (h :
      ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), PreservesColimitsOfShape J F) :
    PreservesFiniteColimits F where
      preservesFiniteColimits J (_ : SmallCategory J) _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this✝ : Category.{?u.29471, ?u.29469} (ULiftHom (ULift.{?u.29469, 0} J)) := ULiftHom.category
this : PreservesColimitsOfShape (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesColimitsOfShape J F

Tactic:
exact preservesColimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesColimitsOfShape J F

Tactic:
letI : Category (ULiftHom (ULift J)) := ULiftHom.category

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : Category.{?u.29471, ?u.29469} (ULiftHom (ULift.{?u.29469, 0} J)) := ULiftHom.category
⊢ PreservesColimitsOfShape J F

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : Category.{?u.29471, ?u.29469} (ULiftHom (ULift.{?u.29469, 0} J)) := ULiftHom.category
⊢ PreservesColimitsOfShape J F

Tactic:
haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this✝ : Category.{?u.29471, ?u.29469} (ULiftHom (ULift.{?u.29469, 0} J)) := ULiftHom.category
this : PreservesColimitsOfShape (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesColimitsOfShape J F
-- Mathlib/Data/Matroid/Closure.lean
lemma spanning_iff_closure_eq (hS : S ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
S : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ M.Spanning S ↔ M.closure S = M.E

Tactic:
rw [spanning_iff, and_iff_left hS]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma GrowsPolynomially.div {f g : ℝ → ℝ} (hf : GrowsPolynomially f)
    (hg : GrowsPolynomially g) : GrowsPolynomially fun x => f x / g x

Proof state:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : (fun x => f x / g x) = fun x => f x * (g x)⁻¹
⊢ GrowsPolynomially fun x => f x / g x

Tactic:
rw [this]

Result:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : (fun x => f x / g x) = fun x => f x * (g x)⁻¹
⊢ GrowsPolynomially fun x => f x * (g x)⁻¹

Proof state:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : (fun x => f x / g x) = fun x => f x * (g x)⁻¹
⊢ GrowsPolynomially fun x => f x * (g x)⁻¹

Tactic:
exact GrowsPolynomially.mul hf (GrowsPolynomially.inv hg)

Result:
no goals

Proof state:
case h
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
x✝ : ℝ
⊢ f x✝ / g x✝ = f x✝ * (g x✝)⁻¹

Tactic:
rw [div_eq_mul_inv]

Result:
no goals

Proof state:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
⊢ GrowsPolynomially fun x => f x / g x

Tactic:
have : (fun x => f x / g x) = fun x => f x * (g x)⁻¹ := by ext; rw [div_eq_mul_inv]

Result:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : (fun x => f x / g x) = fun x => f x * (g x)⁻¹
⊢ GrowsPolynomially fun x => f x / g x

Proof state:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
⊢ (fun x => f x / g x) = fun x => f x * (g x)⁻¹

Tactic:
ext

Result:
case h
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
x✝ : ℝ
⊢ f x✝ / g x✝ = f x✝ * (g x✝)⁻¹
-- Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean
lemma dualSubmodule_dualSubmodule_of_basis
    {ι} [Finite ι] (hB : B.Nondegenerate) (hB' : B.IsSymm) (b : Basis ι S M) :
    B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range b))) =
      Submodule.span R (Set.range b)

Proof state:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := FiniteDimensional.of_fintype_basis b
⊢ B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
  dualBasis_dualBasis B hB hB']

Result:
no goals

Proof state:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
⊢ B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
classical
letI := FiniteDimensional.of_fintype_basis b
rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
  dualBasis_dualBasis B hB hB']

Result:
no goals

Proof state:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
⊢ B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
letI := FiniteDimensional.of_fintype_basis b

Result:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := FiniteDimensional.of_fintype_basis b
⊢ B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma deterministic_map {f : α → β} (hf : Measurable f) {g : β → γ} (hg : Measurable g) :
    (deterministic f hf).map g = deterministic (g ∘ f) (hg.comp hf)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
⊢ (deterministic f hf).map g = deterministic (g ∘ f) ⋯

Tactic:
rw [← id_map, ← map_comp_right _ hf hg, id_map]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem dist_eq_one_iff_adj : G.dist u v = 1 ↔ G.Adj u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = 1 ↔ G.Adj u v

Tactic:
rw [dist, ENat.toNat_eq_iff, ENat.coe_one, edist_eq_one_iff_adj]

Result:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ 1 ≠ 0

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ 1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/PathCategory/Basic.lean
/-- To prove a property on morphisms of a path category with given source `a`, it suffices to
prove it for the identity and prove that the property is preserved under composition on the right
with length 1 paths. -/
lemma induction_fixed_source {a : Paths V} (P : ∀ {b : Paths V}, (a ⟶ b) → Prop)
    (id : P (𝟙 a))
    (comp : ∀ {u v : V} (p : a ⟶ of.obj u) (q : u ⟶ v), P p → P (p ≫ of.map q)) :
    ∀ {b : Paths V} (f : a ⟶ b), P f

Proof state:
V : Type u₁
inst✝ : Quiver V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ of.obj u) (q : u ⟶ v), P p → P (p ≫ of.map q)
b✝ : Paths V
f : a ⟶ b✝
⊢ P f

Tactic:
induction f with
| nil => exact id
| cons _ w h => exact comp _ w h

Result:
no goals

Proof state:
V : Type u₁
inst✝ : Quiver V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ of.obj u) (q : u ⟶ v), P p → P (p ≫ of.map q)
⊢ ∀ {b : Paths V} (f : a ⟶ b), P f

Tactic:
intro _ f

Result:
V : Type u₁
inst✝ : Quiver V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ of.obj u) (q : u ⟶ v), P p → P (p ≫ of.map q)
b✝ : Paths V
f : a ⟶ b✝
⊢ P f

Proof state:
case nil
V : Type u₁
inst✝ : Quiver V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ of.obj u) (q : u ⟶ v), P p → P (p ≫ of.map q)
b✝ : Paths V
⊢ P Quiver.Path.nil

Tactic:
exact id

Result:
no goals

Proof state:
case cons
V : Type u₁
inst✝ : Quiver V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ of.obj u) (q : u ⟶ v), P p → P (p ≫ of.map q)
b✝¹ b✝ c✝ : Paths V
a✝ : Quiver.Path a b✝
w : b✝ ⟶ c✝
h : P a✝
⊢ P (a✝.cons w)

Tactic:
exact comp _ w h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Bitwise/Lemmas.lean
theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0

Proof state:
n : Nat
⊢ 0 >>> n = 0

Tactic:
simp [Int.shiftRight_eq_div_pow]

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/LineDeriv.lean
theorem IsLocalExtr.lineDeriv_eq_zero (h : IsLocalExtr f a) : lineDeriv ℝ f a = 0 :=
  funext fun b ↦ IsExtrFilter.lineDeriv_eq_zero h <| Continuous.tendsto' (by fun_prop) _ _ (by simp)

Proof state:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
f : E → ℝ
a : E
h : IsLocalExtr f a
b : E
⊢ Continuous fun t => a + t • b

Tactic:
fun_prop

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
f : E → ℝ
a : E
h : IsLocalExtr f a
b : E
⊢ a + 0 • b = a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem isGLB_sInf (s : Set (WithTop α)) : IsGLB s (sInf s)

Proof state:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ BddBelow s

Tactic:
use ⊥

Result:
case h
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ ⊥ ∈ lowerBounds s

Proof state:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
exact isGLB_sInf' hs

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
a✝¹ : WithTop α
a✝ : a✝¹ ∈ s
⊢ ⊥ ≤ a✝¹

Tactic:
exact bot_le

Result:
no goals

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsGLB s (sInf s)

Tactic:
by_cases hs : BddBelow s

Result:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)

Proof state:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ False

Tactic:
apply hs

Result:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ BddBelow s

Proof state:
case h
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ ⊥ ∈ lowerBounds s

Tactic:
intro _ _

Result:
case h
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
a✝¹ : WithTop α
a✝ : a✝¹ ∈ s
⊢ ⊥ ≤ a✝¹

Proof state:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
exfalso

Result:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ False
-- Mathlib/Data/List/TFAE.lean
theorem forall_tfae {α : Type*} (l : List (α → Prop)) (H : ∀ a : α, (l.map (fun p ↦ p a)).TFAE) :
    (l.map (fun p ↦ ∀ a, p a)).TFAE

Proof state:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
⊢ (map (fun p => ∀ (a : α), p a) l).TFAE

Tactic:
simp only [TFAE, List.forall_mem_map]

Result:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∀ (a : α), j a) ↔ ∀ (a : α), j_1 a)

Proof state:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∀ (a : α), p₁ a) ↔ ∀ (a : α), p₂ a

Tactic:
exact forall_congr' fun a ↦ H a (p₁ a) (mem_map_of_mem (fun p ↦ p a) hp₁)
  (p₂ a) (mem_map_of_mem (fun p ↦ p a) hp₂)

Result:
no goals

Proof state:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∀ (a : α), j a) ↔ ∀ (a : α), j_1 a)

Tactic:
intros p₁ hp₁ p₂ hp₂

Result:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∀ (a : α), p₁ a) ↔ ∀ (a : α), p₂ a
-- Mathlib/Data/List/Perm/Subperm.lean
lemma subperm_iff : l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l

Proof state:
α : Type u_1
l₁ l₂ : List α
⊢ l₁ <+~ l₂ → ∃ l, l ~ l₂ ∧ l₁ <+ l

Tactic:
rintro ⟨l, h₁, h₂⟩

Result:
case intro.intro
α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂ : l <+ l₂
⊢ ∃ l, l ~ l₂ ∧ l₁ <+ l

Proof state:
case intro.intro.intro
α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂✝ : l <+ l₂
l' : List α
h₂ : l₂ ~ l ++ l'
⊢ ∃ l, l ~ l₂ ∧ l₁ <+ l

Tactic:
exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
⊢ l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l

Tactic:
refine ⟨?_, fun ⟨l, h₁, h₂⟩ ↦ h₂.subperm.trans h₁.subperm⟩

Result:
α : Type u_1
l₁ l₂ : List α
⊢ l₁ <+~ l₂ → ∃ l, l ~ l₂ ∧ l₁ <+ l

Proof state:
case intro.intro
α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂ : l <+ l₂
⊢ ∃ l, l ~ l₂ ∧ l₁ <+ l

Tactic:
obtain ⟨l', h₂⟩ := h₂.exists_perm_append

Result:
case intro.intro.intro
α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂✝ : l <+ l₂
l' : List α
h₂ : l₂ ~ l ++ l'
⊢ ∃ l, l ~ l₂ ∧ l₁ <+ l
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_one_one_charP (p : ℕ) [Fact p.Prime] [CharP R p] : dickson 1 (1 : R) p = X ^ p

Proof state:
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ dickson 1 1 p = X ^ p

Tactic:
have h : (1 : R) = ZMod.castHom (dvd_refl p) R 1 := by
  simp only [ZMod.castHom_apply, ZMod.cast_one']

Result:
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = (ZMod.castHom ⋯ R) 1
⊢ dickson 1 1 p = X ^ p

Proof state:
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = (ZMod.castHom ⋯ R) 1
⊢ dickson 1 1 p = X ^ p

Tactic:
rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow,
  map_X]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ 1 = (ZMod.castHom ⋯ R) 1

Tactic:
simp only [ZMod.castHom_apply, ZMod.cast_one']

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_monomial_le (s : σ →₀ ℕ) (c : R) :
    (monomial s c).totalDegree ≤ s.sum fun _ ↦ id

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c = 0
⊢ ((monomial s) c).totalDegree ≤ s.sum fun x => id

Tactic:
simp only [hc, map_zero, totalDegree_zero, zero_le]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : ¬c = 0
⊢ ((monomial s) c).totalDegree ≤ s.sum fun x => id

Tactic:
rw [totalDegree_monomial _ hc, Function.id_def]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
⊢ ((monomial s) c).totalDegree ≤ s.sum fun x => id

Tactic:
if hc : c = 0 then
  simp only [hc, map_zero, totalDegree_zero, zero_le]
else
  rw [totalDegree_monomial _ hc, Function.id_def]

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_mul_le_right [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) :
    (A * B).rank ≤ B.rank

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ finrank R ↥(LinearMap.range (A.mulVecLin ∘ₗ B.mulVecLin)) ≤ finrank R ↥(LinearMap.range B.mulVecLin)

Tactic:
exact finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _)
  (rank_lt_aleph0 _ _)

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ (A * B).rank ≤ B.rank

Tactic:
rw [rank, rank, mulVecLin_mul]

Result:
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ finrank R ↥(LinearMap.range (A.mulVecLin ∘ₗ B.mulVecLin)) ≤ finrank R ↥(LinearMap.range B.mulVecLin)
-- Mathlib/Order/Category/DistLat.lean
lemma id_apply (X : DistLat) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : DistLat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
/-- A map is a homeomorphism iff it is continuous and has a continuous inverse. -/
lemma isHomeomorph_iff_exists_inverse : IsHomeomorph f ↔ Continuous f ∧ ∃ g : Y → X,
    LeftInverse g f ∧ RightInverse g f ∧ Continuous g

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
h : X ≃ₜ Y := IsHomeomorph.homeomorph f hf
⊢ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous g

Tactic:
exact ⟨h.symm, h.left_inv, h.right_inv, h.continuous_invFun⟩

Result:
no goals

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous g

Tactic:
let h := hf.homeomorph f

Result:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
h : X ≃ₜ Y := IsHomeomorph.homeomorph f hf
⊢ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous g

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔ Continuous f ∧ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous g

Tactic:
refine ⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩

Result:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsHomeomorph f
⊢ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous g

case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous f ∧ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous g
hf : Continuous f
g : Y → X
hg : LeftInverse g f ∧ RightInverse g f ∧ Continuous g
⊢ IsHomeomorph f

Proof state:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous f ∧ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous g
hf : Continuous f
g : Y → X
hg : LeftInverse g f ∧ RightInverse g f ∧ Continuous g
⊢ IsHomeomorph f

Tactic:
exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem process_difference_le (s : ℕ → Set Ω) (ω : Ω) (n : ℕ) :
    |process s (n + 1) ω - process s n ω| ≤ (1 : ℝ≥0)

Proof state:
Ω : Type u_1
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ (s (n + 1)).indicator (fun a => ‖1 a‖) ω ≤ 1

Tactic:
refine Set.indicator_le' (fun _ _ => ?_) (fun _ _ => zero_le_one) _

Result:
Ω : Type u_1
s : ℕ → Set Ω
ω : Ω
n : ℕ
x✝¹ : Ω
x✝ : x✝¹ ∈ s (n + 1)
⊢ ‖1 x✝¹‖ ≤ 1

Proof state:
Ω : Type u_1
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ |process s (n + 1) ω - process s n ω| ≤ ↑1

Tactic:
norm_cast

Result:
Ω : Type u_1
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ |process s (n + 1) ω - process s n ω| ≤ 1

Proof state:
Ω : Type u_1
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ |process s (n + 1) ω - process s n ω| ≤ 1

Tactic:
rw [process, process, Finset.sum_apply, Finset.sum_apply,
  Finset.sum_range_succ_sub_sum, ← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]

Result:
Ω : Type u_1
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ (s (n + 1)).indicator (fun a => ‖1 a‖) ω ≤ 1

Proof state:
Ω : Type u_1
s : ℕ → Set Ω
ω : Ω
n : ℕ
x✝¹ : Ω
x✝ : x✝¹ ∈ s (n + 1)
⊢ ‖1 x✝¹‖ ≤ 1

Tactic:
rw [Pi.one_apply, norm_one]

Result:
no goals
-- Mathlib/Data/Rat/Floor.lean
theorem isInt_intFloor_ofIsRat (r : α) (n : ℤ) (d : ℕ) :
    IsRat r n d → IsInt ⌊r⌋ (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

Proof state:
case mk.out
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ ⌊↑n / ↑d⌋ = n / ↑d

Tactic:
rw [← floor_intCast_div_natCast n d, ← floor_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
α : 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)
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem degree_le_maxDegree [DecidableRel G.Adj] (v : V) : G.degree v ≤ G.maxDegree

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
this : G.degree v ≤ t
⊢ G.degree v ≤ G.maxDegree

Tactic:
rwa [maxDegree, ht]

Result:
no goals

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
⊢ G.degree v ≤ G.maxDegree

Tactic:
have := Finset.le_max_of_eq (mem_image_of_mem _ (mem_univ v)) ht

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
this : G.degree v ≤ t
⊢ G.degree v ≤ G.maxDegree

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ G.degree v ≤ G.maxDegree

Tactic:
obtain ⟨t, ht : _ = _⟩ := Finset.max_of_mem (mem_image_of_mem (fun v => G.degree v) (mem_univ v))

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
⊢ G.degree v ≤ G.maxDegree