harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_empty_left : ∅ ○ t = ∅

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
t : Finset α
⊢ ∅ ○ t = ∅

Tactic:
simp [disjSups]

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem _root_.Continuous.path_eval {Y} [TopologicalSpace Y] {f : Y → Path x y} {g : Y → I}
    (hf : Continuous f) (hg : Continuous g) : Continuous fun y => f y (g y)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
x y : X
Y : Type u_4
inst✝ : TopologicalSpace Y
f : Y → Path x y
g : Y → ↑I
hf : Continuous f
hg : Continuous g
⊢ Continuous fun y_1 => (f y_1) (g y_1)

Tactic:
continuity

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem norm_toContinuousLinearMap_comp [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G)
    {g : E →SL[σ₁₂] F} : ‖f.toContinuousLinearMap.comp g‖ = ‖g‖ :=
  opNorm_ext (f.toContinuousLinearMap.comp g) g fun x => by
    simp only [norm_map, coe_toContinuousLinearMap, coe_comp', Function.comp_apply]

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomIsometric σ₁₂
f : F →ₛₗᵢ[σ₂₃] G
g : E →SL[σ₁₂] F
x : E
⊢ ‖(f.toContinuousLinearMap.comp g) x‖ = ‖g x‖

Tactic:
simp only [norm_map, coe_toContinuousLinearMap, coe_comp', Function.comp_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/NatAntidiagonal.lean
theorem prod_antidiagonal_subst {n : ℕ} {f : ℕ × ℕ → ℕ → M} :
    ∏ p ∈ antidiagonal n, f p n = ∏ p ∈ antidiagonal n, f p (p.1 + p.2) :=
  prod_congr rfl fun p hp ↦ by rw [mem_antidiagonal.mp hp]

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → ℕ → M
p : ℕ × ℕ
hp : p ∈ antidiagonal n
⊢ f p n = f p (p.1 + p.2)

Tactic:
rw [mem_antidiagonal.mp hp]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_comp : (g.comp f).lTensor M = (g.lTensor M).comp (f.lTensor M)

Proof state:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : M
n : N
⊢ (((TensorProduct.mk R M N).compr₂ (lTensor M (g ∘ₗ f))) m) n =
    (((TensorProduct.mk R M N).compr₂ (lTensor M g ∘ₗ lTensor M f)) m) n

Tactic:
simp only [compr₂_apply, mk_apply, comp_apply, lTensor_tmul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
⊢ lTensor M (g ∘ₗ f) = lTensor M g ∘ₗ lTensor M f

Tactic:
ext m n

Result:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : M
n : N
⊢ (((TensorProduct.mk R M N).compr₂ (lTensor M (g ∘ₗ f))) m) n =
    (((TensorProduct.mk R M N).compr₂ (lTensor M g ∘ₗ lTensor M f)) m) n
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_X_pow (n : ℕ) : (X ^ n : R[X]).roots = n • ({0} : Multiset R)

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ (X ^ n).roots = n • {0}

Tactic:
rw [roots_pow, roots_X]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem three_le_nValue (hN : 64 ≤ N) : 3 ≤ nValue N

Proof state:
N : ℕ
hN : 64 ≤ N
⊢ 2 ^ ↑6 ≤ ↑N

Tactic:
rw [rpow_natCast]

Result:
N : ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑N

Proof state:
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑6

Tactic:
norm_num1

Result:
no goals

Proof state:
N : ℕ
hN : 64 ≤ N
⊢ 2 < √(log ↑N)

Tactic:
apply lt_sqrt_of_sq_lt

Result:
case h
N : ℕ
hN : 64 ≤ N
⊢ 2 ^ 2 < log ↑N

Proof state:
N : ℕ
hN : 64 ≤ N
⊢ 3 ≤ nValue N

Tactic:
rw [nValue, ← lt_iff_add_one_le, lt_ceil, cast_two]

Result:
N : ℕ
hN : 64 ≤ N
⊢ 2 < √(log ↑N)

Proof state:
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log (2 ^ ↑6)

Tactic:
rw [log_rpow zero_lt_two, ← div_lt_iff₀']

Result:
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 < log 2

N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑6

Proof state:
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 ≤ 0.6931471803

Tactic:
norm_num1

Result:
no goals

Proof state:
case h
N : ℕ
hN : 64 ≤ N
⊢ 2 ^ 2 < log ↑N

Tactic:
have : (2 : ℝ) ^ ((6 : ℕ) : ℝ) ≤ N := by
  rw [rpow_natCast]
  exact (cast_le.2 hN).trans' (by norm_num1)

Result:
case h
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log ↑N

Proof state:
N : ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑N

Tactic:
exact (cast_le.2 hN).trans' (by norm_num1)

Result:
no goals

Proof state:
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 < log 2

Tactic:
exact log_two_gt_d9.trans_le' (by norm_num1)

Result:
no goals

Proof state:
N : ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑64

Tactic:
norm_num1

Result:
no goals

Proof state:
case h
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log ↑N

Tactic:
apply lt_of_lt_of_le _ (log_le_log (rpow_pos_of_pos zero_lt_two _) this)

Result:
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log (2 ^ ↑6)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_empty (f : α → β) : map f #v[] = #v[]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ Array.map f { toArray := #[], size_toArray := ⋯ }.toArray = #[]

Tactic:
exact Array.map_empty f

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ map f { toArray := #[], size_toArray := ⋯ } = { toArray := #[], size_toArray := ⋯ }

Tactic:
rw [map, mk.injEq]

Result:
α : Type u_1
β : Type u_2
f : α → β
⊢ Array.map f { toArray := #[], size_toArray := ⋯ }.toArray = #[]
-- Mathlib/Topology/Algebra/Module/LocallyConvex.lean
theorem locallyConvexSpace_inf {t₁ t₂ : TopologicalSpace E} (h₁ : @LocallyConvexSpace 𝕜 E _ _ _ t₁)
    (h₂ : @LocallyConvexSpace 𝕜 E _ _ _ t₂) : @LocallyConvexSpace 𝕜 E _ _ _ (t₁ ⊓ t₂)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine locallyConvexSpace_iInf fun b => ?_

Result:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
b : Bool
⊢ LocallyConvexSpace 𝕜 E

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
b : Bool
⊢ LocallyConvexSpace 𝕜 E

Tactic:
cases b <;> assumption

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
theorem projIcc :
    smoothTransition (projIcc (0 : ℝ) 1 zero_le_one x) = smoothTransition x

Proof state:
case refine_2
x✝ x : ℝ
hx : 1 < x
⊢ x.smoothTransition = smoothTransition 1

Tactic:
rw [smoothTransition.one, one_of_one_le hx.le]

Result:
no goals

Proof state:
case refine_1
x✝ x : ℝ
hx : x < 0
⊢ x.smoothTransition = smoothTransition 0

Tactic:
rw [smoothTransition.zero, zero_of_nonpos hx.le]

Result:
no goals

Proof state:
x : ℝ
⊢ (↑(projIcc 0 1 ⋯ x)).smoothTransition = x.smoothTransition

Tactic:
refine congr_fun
  (IccExtend_eq_self zero_le_one smoothTransition (fun x hx => ?_) fun x hx => ?_) x

Result:
case refine_1
x✝ x : ℝ
hx : x < 0
⊢ x.smoothTransition = smoothTransition 0

case refine_2
x✝ x : ℝ
hx : 1 < x
⊢ x.smoothTransition = smoothTransition 1
-- Mathlib/Algebra/Group/TypeTags/Basic.lean
lemma Pi.single_additiveOfMul_eq {ι : Type*} [DecidableEq ι] {M : ι → Type*}
    [(i : ι) → Monoid (M i)] (i : ι) (a : M i) (j : ι) :
    Pi.single (f := fun i ↦ Additive (M i)) i (Additive.ofMul a) j =
      Additive.ofMul ((Pi.mulSingle i a) j)

Proof state:
case inl
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
a : M j
⊢ single j (ofMul a) j = ofMul (mulSingle j a j)

Tactic:
simp only [mulSingle_eq_same, single_eq_same]

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)

Tactic:
rcases eq_or_ne j i with rfl | h

Result:
case inl
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
a : M j
⊢ single j (ofMul a) j = ofMul (mulSingle j a j)

case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)

Proof state:
case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)

Tactic:
simp only [single, ne_eq, h, not_false_eq_true, Function.update_of_ne, zero_apply, mulSingle,
  one_apply, ofMul_one]

Result:
no goals
-- Mathlib/Data/Finset/Dedup.lean
theorem Nodup.toFinset_inj {l l' : Multiset α} (hl : Nodup l) (hl' : Nodup l')
    (h : l.toFinset = l'.toFinset) : l = l'

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : Multiset α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l = l'

Tactic:
simpa [← toFinset_eq hl, ← toFinset_eq hl'] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem zero_pow_of_pos (n : Nat) (h : 0 < n) : 0 ^ n = 0

Proof state:
case succ
n : Nat
h : 0 < n + 1
⊢ 0 ^ (n + 1) = 0

Tactic:
simp [Nat.pow_succ]

Result:
no goals

Proof state:
case zero
h : 0 < 0
⊢ 0 ^ 0 = 0

Tactic:
cases h

Result:
no goals

Proof state:
n : Nat
h : 0 < n
⊢ 0 ^ n = 0

Tactic:
cases n with
| zero => cases h
| succ n => simp [Nat.pow_succ]

Result:
no goals
-- Mathlib/Data/Finset/Pairwise.lean
theorem Finset.pairwiseDisjoint_range_singleton :
    (Set.range (singleton : α → Finset α)).PairwiseDisjoint id

Proof state:
case intro.intro
α : Type u_1
a b : α
h : {a} ≠ {b}
⊢ Function.onFun Disjoint id {a} {b}

Tactic:
exact disjoint_singleton.2 (ne_of_apply_ne _ h)

Result:
no goals

Proof state:
α : Type u_1
⊢ (Set.range singleton).PairwiseDisjoint id

Tactic:
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h

Result:
case intro.intro
α : Type u_1
a b : α
h : {a} ≠ {b}
⊢ Function.onFun Disjoint id {a} {b}
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Equiv.hasProd_iff (e : γ ≃ β) : HasProd (f ∘ e) a ↔ HasProd f a :=
  e.injective.hasProd_iff <| by simp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
e : γ ≃ β
⊢ ∀ x ∉ Set.range ⇑e, f x = 1

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem card_eq_nat {o} {n : ℕ} : card o = n ↔ o = n

Proof state:
o : Ordinal.{u_1}
n : ℕ
⊢ o.card = ↑n ↔ o = ↑n

Tactic:
simp only [le_antisymm_iff, card_le_nat, nat_le_card]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem submodule_comap_pow_reverse (p : Submodule R (CliffordAlgebra Q)) (n : ℕ) :
    (p ^ n).comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) =
      p.comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) ^ n

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.comap reverse (p ^ n) = Submodule.comap reverse p ^ n

Tactic:
simp_rw [← submodule_map_reverse_eq_comap, submodule_map_pow_reverse]

Result:
no goals
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem extend_div [Div γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
    Function.extend f (g₁ / g₂) (e₁ / e₂) = Function.extend f g₁ e₁ / Function.extend f g₂ e₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂

Tactic:
funext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x

Tactic:
simp [Function.extend_def, apply_dite₂]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂

Tactic:
classical
funext x
simp [Function.extend_def, apply_dite₂]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isClopen_iff {s : Set (PrimeSpectrum R)} :
    IsClopen s ↔ ∃ e : R, IsIdempotentElem e ∧ s = basicOpen e

Proof state:
case intro.intro
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClopen ↑(basicOpen e)

Tactic:
refine ⟨?_, (basicOpen e).2⟩

Result:
case intro.intro
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClosed ↑(basicOpen e)

Proof state:
R : Type u
inst✝ : CommRing R
s : Set (PrimeSpectrum R)
⊢ (∃ e, IsIdempotentElem e ∧ s = ↑(basicOpen e)) → IsClopen s

Tactic:
rintro ⟨e, he, rfl⟩

Result:
case intro.intro
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClopen ↑(basicOpen e)

Proof state:
R : Type u
inst✝ : CommRing R
s : Set (PrimeSpectrum R)
⊢ IsClopen s ↔ ∃ e, IsIdempotentElem e ∧ s = ↑(basicOpen e)

Tactic:
refine ⟨exists_idempotent_basicOpen_eq_of_isClopen, ?_⟩

Result:
R : Type u
inst✝ : CommRing R
s : Set (PrimeSpectrum R)
⊢ (∃ e, IsIdempotentElem e ∧ s = ↑(basicOpen e)) → IsClopen s

Proof state:
case intro.intro
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClosed ↑(basicOpen e)

Tactic:
rw [PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem e he]

Result:
case intro.intro
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClosed (zeroLocus {1 - e})

Proof state:
case intro.intro
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClosed (zeroLocus {1 - e})

Tactic:
exact isClosed_zeroLocus _

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_eq_Ioo' (hxy : x ≠ y) : openSegment 𝕜 x y = Ioo (min x y) (max x y)

Proof state:
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
hxy : x ≠ y
h : x < y
⊢ openSegment 𝕜 x y = Ioo (x ⊓ y) (x ⊔ y)

Tactic:
rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
⊢ openSegment 𝕜 x y = Ioo (x ⊓ y) (x ⊔ y)

Tactic:
rw [openSegment_symm, openSegment_eq_Ioo h, max_eq_left h.le, min_eq_right h.le]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
hxy : x ≠ y
⊢ openSegment 𝕜 x y = Ioo (x ⊓ y) (x ⊔ y)

Tactic:
rcases hxy.lt_or_lt with h | h

Result:
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
hxy : x ≠ y
h : x < y
⊢ openSegment 𝕜 x y = Ioo (x ⊓ y) (x ⊔ y)

case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
⊢ openSegment 𝕜 x y = Ioo (x ⊓ y) (x ⊔ y)
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_asympBound_pos : ∀ᶠ (n : ℕ) in atTop, 0 < asympBound g a b n

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 < asympBound g a b n

Tactic:
exact R.asympBound_pos n hn

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < asympBound g a b n

Tactic:
filter_upwards [eventually_gt_atTop 0] with n hn

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 < asympBound g a b n
-- Mathlib/GroupTheory/OrderOfElement.lean
lemma smul_eq_of_smul_le
    {G : Type*} [Group G] [Finite G] {α : Type*} [PartialOrder α] {g : G} {a : α}
    [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] (h : g • a ≤ a) : g • a = a

Proof state:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ g • a = a

Tactic:
have key := smul_mono_right g (pow_smul_le h (Nat.card G - 1))

Result:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : g • g ^ (Nat.card G - 1) • a ≤ g • a
⊢ g • a = a

Proof state:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : g • g ^ (Nat.card G - 1) • a ≤ g • a
⊢ g • a = a

Tactic:
rw [smul_smul, ← _root_.pow_succ',
  Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key

Result:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : a ≤ g • a
⊢ g • a = a

Proof state:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : a ≤ g • a
⊢ g • a = a

Tactic:
exact le_antisymm h key

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean
theorem GradedAlgebra.ι_apply (m : M) :
    GradedAlgebra.ι R M m =
      DirectSum.of (fun i : ℕ => ⋀[R]^i M) 1
        ⟨ι R m, by simpa only [pow_one] using LinearMap.mem_range_self _ m⟩ :=
  rfl

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (ι R) m ∈ ⋀[R]^1 M

Tactic:
simpa only [pow_one] using LinearMap.mem_range_self _ m

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
lemma rank_le_of_isSMulRegular {S : Type*} [CommSemiring S] [Algebra S R] [Module S M]
    [IsScalarTower S R M] (L L' : Submodule R M) {s : S} (hr : IsSMulRegular M s)
    (h : ∀ x ∈ L, s • x ∈ L') :
    Module.rank R L ≤ Module.rank R L' :=
  ((Algebra.lsmul S R M s).restrict h).rank_le_of_injective <|
    fun _ _ h ↦ by simpa using hr (Subtype.ext_iff.mp h)

Proof state:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
L L' : Submodule R M
s : S
hr : IsSMulRegular M s
h✝ : ∀ x ∈ L, s • x ∈ L'
x✝¹ x✝ : ↥L
h : (LinearMap.restrict ((Algebra.lsmul S R M) s) h✝) x✝¹ = (LinearMap.restrict ((Algebra.lsmul S R M) s) h✝) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using hr (Subtype.ext_iff.mp h)

Result:
no goals
-- Mathlib/Topology/UrysohnsLemma.lean
theorem approx_le_succ (c : CU P) (n : ℕ) (x : X) : c.approx n x ≤ c.approx (n + 1) x

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ approx (n + 1) c x
c : CU P
⊢ approx (n + 1) c x ≤ approx (n + 1 + 1) c x

Tactic:
rw [approx, approx]

Result:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ approx (n + 1) c x
c : CU P
⊢ midpoint ℝ (approx n c.left x) (approx n c.right x) ≤ midpoint ℝ (approx (n + 1) c.left x) (approx (n + 1) c.right x)

Proof state:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
⊢ approx 0 c x ≤ approx (0 + 1) c x

Tactic:
simp only [approx, right_U, right_le_midpoint]

Result:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
⊢ c.Uᶜ.indicator 1 x ≤ c.left.Uᶜ.indicator 1 x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
n : ℕ
x : X
⊢ approx n c x ≤ approx (n + 1) c x

Tactic:
induction n generalizing c with
| zero =>
  simp only [approx, right_U, right_le_midpoint]
  exact (approx_mem_Icc_right_left c 0 x).2
| succ n ihn =>
  rw [approx, approx]
  exact midpoint_le_midpoint (ihn _) (ihn _)

Result:
no goals

Proof state:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
⊢ c.Uᶜ.indicator 1 x ≤ c.left.Uᶜ.indicator 1 x

Tactic:
exact (approx_mem_Icc_right_left c 0 x).2

Result:
no goals

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ approx (n + 1) c x
c : CU P
⊢ midpoint ℝ (approx n c.left x) (approx n c.right x) ≤ midpoint ℝ (approx (n + 1) c.left x) (approx (n + 1) c.right x)

Tactic:
exact midpoint_le_midpoint (ihn _) (ihn _)

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem intersection_covering (rj : R ∈ J X) (sj : S ∈ J X) : R ⊓ S ∈ J X

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
⊢ R ⊓ S ∈ J X

Tactic:
apply J.transitive rj _ fun Y f Hf => _

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
⊢ ∀ (Y : C) (f : Y ⟶ X), R.arrows f → Sieve.pullback f (R ⊓ S) ∈ J Y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
⊢ ∀ (Y : C) (f : Y ⟶ X), R.arrows f → Sieve.pullback f (R ⊓ S) ∈ J Y

Tactic:
intros Y f hf

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f (R ⊓ S) ∈ J Y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ ⊤ ⊓ Sieve.pullback f S ∈ J Y

Tactic:
simp [sj]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f (R ⊓ S) ∈ J Y

Tactic:
rw [Sieve.pullback_inter, R.pullback_eq_top_of_mem hf]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ ⊤ ⊓ Sieve.pullback f S ∈ J Y