harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- The evaluation map is injective for connected objects. -/
lemma evaluation_injective_of_isConnected (A X : C) [IsConnected A] (a : F.obj A) :
    Function.Injective (fun (f : A ⟶ X) ↦ F.map f a)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective fun f => F.map f a

Tactic:
intro f g (h : F.map f a = F.map g a)

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).carrier
f g : A ⟶ X
h : F.map f a = F.map g a
⊢ f = g

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).carrier
f g : A ⟶ X
h : F.map f a = F.map g a
this : IsIso (equalizer.ι f g)
⊢ f = g

Tactic:
exact eq_of_epi_equalizer

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).carrier
f g : A ⟶ X
h : F.map f a = F.map g a
⊢ IsInitial (equalizer f g) → False

Tactic:
exact not_initial_of_inhabited F ((fiberEqualizerEquiv F f g).symm ⟨a, h⟩)

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).carrier
f g : A ⟶ X
h : F.map f a = F.map g a
⊢ f = g

Tactic:
haveI : IsIso (equalizer.ι f g) := by
  apply IsConnected.noTrivialComponent _ (equalizer.ι f g)
  exact not_initial_of_inhabited F ((fiberEqualizerEquiv F f g).symm ⟨a, h⟩)

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).carrier
f g : A ⟶ X
h : F.map f a = F.map g a
this : IsIso (equalizer.ι f g)
⊢ f = g

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).carrier
f g : A ⟶ X
h : F.map f a = F.map g a
⊢ IsIso (equalizer.ι f g)

Tactic:
apply IsConnected.noTrivialComponent _ (equalizer.ι f g)

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).carrier
f g : A ⟶ X
h : F.map f a = F.map g a
⊢ IsInitial (equalizer f g) → False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_append {l₁ r₁ : Array α} {l₂ r₂ : Array β} (_h : l₁.size = l₂.size) :
    zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
r₂ : Array β
toList✝² : List α
toList✝¹ : List β
_h : { toList := toList✝² }.size = { toList := toList✝¹ }.size
toList✝ : List α
⊢ ({ toList := toList✝² } ++ { toList := toList✝ }).zip ({ toList := toList✝¹ } ++ r₂) =
    { toList := toList✝² }.zip { toList := toList✝¹ } ++ { toList := toList✝ }.zip r₂

Tactic:
cases r₂

Result:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
toList✝³ : List α
toList✝² : List β
_h : { toList := toList✝³ }.size = { toList := toList✝² }.size
toList✝¹ : List α
toList✝ : List β
⊢ ({ toList := toList✝³ } ++ { toList := toList✝¹ }).zip ({ toList := toList✝² } ++ { toList := toList✝ }) =
    { toList := toList✝³ }.zip { toList := toList✝² } ++ { toList := toList✝¹ }.zip { toList := toList✝ }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
r₁ : Array α
r₂ : Array β
toList✝¹ : List α
toList✝ : List β
_h : { toList := toList✝¹ }.size = { toList := toList✝ }.size
⊢ ({ toList := toList✝¹ } ++ r₁).zip ({ toList := toList✝ } ++ r₂) =
    { toList := toList✝¹ }.zip { toList := toList✝ } ++ r₁.zip r₂

Tactic:
cases r₁

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
r₂ : Array β
toList✝² : List α
toList✝¹ : List β
_h : { toList := toList✝² }.size = { toList := toList✝¹ }.size
toList✝ : List α
⊢ ({ toList := toList✝² } ++ { toList := toList✝ }).zip ({ toList := toList✝¹ } ++ r₂) =
    { toList := toList✝² }.zip { toList := toList✝¹ } ++ { toList := toList✝ }.zip r₂

Proof state:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
toList✝³ : List α
toList✝² : List β
_h : { toList := toList✝³ }.size = { toList := toList✝² }.size
toList✝¹ : List α
toList✝ : List β
⊢ ({ toList := toList✝³ } ++ { toList := toList✝¹ }).zip ({ toList := toList✝² } ++ { toList := toList✝ }) =
    { toList := toList✝³ }.zip { toList := toList✝² } ++ { toList := toList✝¹ }.zip { toList := toList✝ }

Tactic:
simp_all [List.zip_append]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
r₁ : Array α
l₂ r₂ : Array β
toList✝ : List α
_h : { toList := toList✝ }.size = l₂.size
⊢ ({ toList := toList✝ } ++ r₁).zip (l₂ ++ r₂) = { toList := toList✝ }.zip l₂ ++ r₁.zip r₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
r₁ : Array α
r₂ : Array β
toList✝¹ : List α
toList✝ : List β
_h : { toList := toList✝¹ }.size = { toList := toList✝ }.size
⊢ ({ toList := toList✝¹ } ++ r₁).zip ({ toList := toList✝ } ++ r₂) =
    { toList := toList✝¹ }.zip { toList := toList✝ } ++ r₁.zip r₂

Proof state:
α : Type u_1
β : Type u_2
l₁ r₁ : Array α
l₂ r₂ : Array β
_h : l₁.size = l₂.size
⊢ (l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
r₁ : Array α
l₂ r₂ : Array β
toList✝ : List α
_h : { toList := toList✝ }.size = l₂.size
⊢ ({ toList := toList✝ } ++ r₁).zip (l₂ ++ r₂) = { toList := toList✝ }.zip l₂ ++ r₁.zip r₂
-- Mathlib/Order/Hom/Basic.lean
theorem OrderIso.complementedLattice_iff (f : α ≃o β) :
    ComplementedLattice α ↔ ComplementedLattice β :=
  ⟨by intro; exact f.complementedLattice,
   by intro; exact f.symm.complementedLattice⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ ComplementedLattice β → ComplementedLattice α

Tactic:
intro

Result:
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice β
⊢ ComplementedLattice α

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ ComplementedLattice α → ComplementedLattice β

Tactic:
intro

Result:
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice α
⊢ ComplementedLattice β

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice β
⊢ ComplementedLattice α

Tactic:
exact f.symm.complementedLattice

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice α
⊢ ComplementedLattice β

Tactic:
exact f.complementedLattice

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_mkPiAlgebraFin_le :
    ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ max 1 ‖(1 : A)‖

Proof state:
case zero
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ 1 ⊔ ‖1‖

Tactic:
exact norm_mkPiAlgebraFin_zero.le.trans (le_max_right _ _)

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1 ⊔ ‖1‖

Tactic:
cases n

Result:
case zero
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ 1 ⊔ ‖1‖

case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
n✝ : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) A‖ ≤ 1 ⊔ ‖1‖

Proof state:
case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
n✝ : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) A‖ ≤ 1 ⊔ ‖1‖

Tactic:
exact (norm_mkPiAlgebraFin_le_of_pos (Nat.zero_lt_succ _)).trans (le_max_left _ _)

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- If the `LSeries` of `f` and of `g` converge somewhere and agree on large real arguments,
then `f n = g n` whenever `n ≠ 0`. -/
lemma LSeries.eq_of_LSeries_eventually_eq {f g : ℕ → ℂ} (hf : abscissaOfAbsConv f < ⊤)
    (hg : abscissaOfAbsConv g < ⊤) (h : (fun x : ℝ ↦ LSeries f x) =ᶠ[atTop] fun x ↦ LSeries g x)
    {n : ℕ} (hn : n ≠ 0) :
    f n = g n

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
⊢ f n = g n

Tactic:
have ha : abscissaOfAbsConv (f - g) ≠ ⊤ :=
  lt_top_iff_ne_top.mp <| (abscissaOfAbsConv_sub_le f g).trans_lt <| max_lt hf hg

Result:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
ha : abscissaOfAbsConv (f - g) ≠ ⊤
⊢ f n = g n

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
⊢ f n = g n

Tactic:
have hsub : (fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ) :=
  LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq hf hg h

Result:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
⊢ f n = g n

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
ha : abscissaOfAbsConv (f - g) ≠ ⊤
⊢ f n = g n

Tactic:
simpa only [Pi.sub_apply, sub_eq_zero]
  using (LSeries_eventually_eq_zero_iff'.mp hsub).resolve_right ha n hn

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
lemma toNNReal_le_toNNReal_iff' {r p : ℝ} : r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0

Proof state:
r p : ℝ
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0

Tactic:
simp_rw [← not_lt, toNNReal_lt_toNNReal_iff', not_and_or]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
theorem coverEntropy_image_le_of_uniformContinuous [UniformSpace X] [UniformSpace Y] {S : X → X}
    {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) :
    coverEntropy T (φ '' F) ≤ coverEntropy S F

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F

Tactic:
rw [coverEntropy_image_of_comap _ h F]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropy S F ≤ coverEntropy S F

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropy S F ≤ coverEntropy S F

Tactic:
exact coverEntropy_antitone S F (uniformContinuous_iff.1 h')

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
theorem quadratic_reciprocity' (hp : p ≠ 2) (hq : q ≠ 2) :
    legendreSym q p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p q

Proof state:
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  (fun x => x * legendreSym p ↑q) (legendreSym q ↑p * legendreSym p ↑q) =
    (fun x => x * legendreSym p ↑q) ((-1) ^ (p / 2 * (q / 2)))
this : ↑↑q ≠ 0
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

Tactic:
simpa only [mul_assoc, ← pow_two, sq_one p this, mul_one] using qr

Result:
no goals

Proof state:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

Tactic:
rcases eq_or_ne p q with h | h

Result:
case inl
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p = q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

Proof state:
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  (fun x => x * legendreSym p ↑q) (legendreSym q ↑p * legendreSym p ↑q) =
    (fun x => x * legendreSym p ↑q) ((-1) ^ (p / 2 * (q / 2)))
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

Tactic:
have : ((q : ℤ) : ZMod p) ≠ 0 := mod_cast prime_ne_zero p q h

Result:
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  (fun x => x * legendreSym p ↑q) (legendreSym q ↑p * legendreSym p ↑q) =
    (fun x => x * legendreSym p ↑q) ((-1) ^ (p / 2 * (q / 2)))
this : ↑↑q ≠ 0
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

Proof state:
case inl
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p = q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

Tactic:
subst p

Result:
case inl
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp : q ≠ 2
⊢ legendreSym q ↑q = (-1) ^ (q / 2 * (q / 2)) * legendreSym q ↑q

Proof state:
case inl
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp : q ≠ 2
⊢ legendreSym q ↑q = (-1) ^ (q / 2 * (q / 2)) * legendreSym q ↑q

Tactic:
rw [(eq_zero_iff q q).mpr (mod_cast natCast_self q), mul_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem one_rpow (x : ℝ) : (1 : ℝ≥0∞) ^ x = 1

Proof state:
x : ℝ
⊢ 1 ^ x = 1

Tactic:
rw [← coe_one, ← coe_rpow_of_ne_zero one_ne_zero]

Result:
x : ℝ
⊢ ↑(1 ^ x) = ↑1

Proof state:
x : ℝ
⊢ ↑(1 ^ x) = ↑1

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_le_opow_right {a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : a ^ b ≤ a ^ c

Proof state:
case inr
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 = a
⊢ a ^ b ≤ a ^ c

Tactic:
subst a

Result:
case inr
b c : Ordinal.{u_1}
h₂ : b ≤ c
h₁ : 0 < 1
⊢ 1 ^ b ≤ 1 ^ c

Proof state:
case inr
b c : Ordinal.{u_1}
h₂ : b ≤ c
h₁ : 0 < 1
⊢ 1 ^ b ≤ 1 ^ c

Tactic:
simp only [one_opow, le_refl]

Result:
no goals

Proof state:
case inl
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c

Tactic:
exact (opow_le_opow_iff_right h₁).2 h₂

Result:
no goals

Proof state:
a b c : Ordinal.{u_1}
h₁ : 0 < a
h₂ : b ≤ c
⊢ a ^ b ≤ a ^ c

Tactic:
rcases lt_or_eq_of_le (one_le_iff_pos.2 h₁) with h₁ | h₁

Result:
case inl
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c

case inr
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 = a
⊢ a ^ b ≤ a ^ c
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem Ideal.IsHomogeneous.toIdeal_homogeneousHull_eq_self (h : I.IsHomogeneous 𝒜) :
    (Ideal.homogeneousHull 𝒜 I).toIdeal = I

Proof state:
case intro.intro
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
i : ι
x : ↥I
⊢ ↑(((decompose 𝒜) ↑x) i) ∈ ↑I

Tactic:
exact h _ x.prop

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} ⊆ ↑I

Tactic:
rintro _ ⟨i, x, rfl⟩

Result:
case intro.intro
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
i : ι
x : ↥I
⊢ ↑(((decompose 𝒜) ↑x) i) ∈ ↑I

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ (homogeneousHull 𝒜 I).toIdeal ≤ I

Tactic:
apply Ideal.span_le.2

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} ⊆ ↑I

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ (homogeneousHull 𝒜 I).toIdeal = I

Tactic:
apply le_antisymm _ (Ideal.le_toIdeal_homogeneousHull _ _)

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ (homogeneousHull 𝒜 I).toIdeal ≤ I
-- Mathlib/Data/Matroid/Restrict.lean
theorem finite_setOf_isRestriction (M : Matroid α) [M.Finite] : {N | N ≤r M}.Finite :=
  (M.ground_finite.finite_subsets.image (fun R ↦ M ↾ R)).subset <|
    by rintro _ ⟨R, hR, rfl⟩; exact ⟨_, hR, rfl⟩

Proof state:
α : Type u_1
M : Matroid α
inst✝ : M.Finite
⊢ {N | N ≤r M} ⊆ (fun R => M ↾ R) '' {b | b ⊆ M.E}

Tactic:
rintro _ ⟨R, hR, rfl⟩

Result:
case intro.intro
α : Type u_1
M : Matroid α
inst✝ : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ∈ (fun R => M ↾ R) '' {b | b ⊆ M.E}

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
inst✝ : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ∈ (fun R => M ↾ R) '' {b | b ⊆ M.E}

Tactic:
exact ⟨_, hR, rfl⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem support_toSubring : support (toSubring p T hp) = support p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).support = p.support

Tactic:
ext i

Result:
case h
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
⊢ i ∈ (p.toSubring T hp).support ↔ i ∈ p.support

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
H : (p.toSubring T hp).coeff i = 0
⊢ ↑((p.toSubring T hp).coeff i) = 0

Tactic:
rw [H, ZeroMemClass.coe_zero]

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
⊢ (p.toSubring T hp).coeff i = 0 ↔ p.coeff i = 0

Tactic:
conv_rhs => rw [← coeff_toSubring p T hp]

Result:
case h
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
⊢ (p.toSubring T hp).coeff i = 0 ↔ ↑((p.toSubring T hp).coeff i) = 0

Proof state:
case h
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
⊢ (p.toSubring T hp).coeff i = 0 ↔ ↑((p.toSubring T hp).coeff i) = 0

Tactic:
exact ⟨fun H => by rw [H, ZeroMemClass.coe_zero], fun H => Subtype.coe_injective H⟩

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
⊢ i ∈ (p.toSubring T hp).support ↔ i ∈ p.support

Tactic:
simp only [mem_support_iff, not_iff_not, Ne]

Result:
case h
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
⊢ (p.toSubring T hp).coeff i = 0 ↔ p.coeff i = 0
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem nextCoeffUp_C_eq_zero (c : R) : nextCoeffUp (C c) = 0

Proof state:
R : Type u
inst✝ : Semiring R
c : R
⊢ (C c).nextCoeffUp = 0

Tactic:
rw [nextCoeffUp]

Result:
R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natTrailingDegree = 0 then 0 else (C c).coeff ((C c).natTrailingDegree + 1)) = 0

Proof state:
R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natTrailingDegree = 0 then 0 else (C c).coeff ((C c).natTrailingDegree + 1)) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_append {l₁ l₂ : List α} (i : Nat) (h : i < (l₁ ++ l₂).length) :
    (l₁ ++ l₂)[i] = if h' : i < l₁.length then l₁[i] else l₂[i - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h)

Proof state:
case isTrue
α : Type u_1
l₁ l₂ : List α
i : Nat
h : i < (l₁ ++ l₂).length
h' : i < l₁.length
⊢ (l₁ ++ l₂)[i] = l₁[i]

Tactic:
rw [getElem_append_left h']

Result:
no goals

Proof state:
α : Type ?u.179437
l₁ l₂ : List α
i : Nat
h : i < l₁.length + l₂.length
h' : l₁.length ≤ i
⊢ i - l₁.length < l₂.length

Tactic:
exact Nat.sub_lt_left_of_lt_add h' h

Result:
no goals

Proof state:
α : Type ?u.179437
l₁ l₂ : List α
i : Nat
h : i < (l₁ ++ l₂).length
h' : ¬i < l₁.length
⊢ i - l₁.length < l₂.length

Tactic:
simp at h h'

Result:
α : Type ?u.179437
l₁ l₂ : List α
i : Nat
h : i < l₁.length + l₂.length
h' : l₁.length ≤ i
⊢ i - l₁.length < l₂.length

Proof state:
α : Type u_1
l₁ l₂ : List α
i : Nat
h : i < (l₁ ++ l₂).length
⊢ (l₁ ++ l₂)[i] = if h' : i < l₁.length then l₁[i] else l₂[i - l₁.length]

Tactic:
split <;> rename_i h'

Result:
case isTrue
α : Type u_1
l₁ l₂ : List α
i : Nat
h : i < (l₁ ++ l₂).length
h' : i < l₁.length
⊢ (l₁ ++ l₂)[i] = l₁[i]

case isFalse
α : Type u_1
l₁ l₂ : List α
i : Nat
h : i < (l₁ ++ l₂).length
h' : ¬i < l₁.length
⊢ (l₁ ++ l₂)[i] = l₂[i - l₁.length]

Proof state:
case isFalse
α : Type u_1
l₁ l₂ : List α
i : Nat
h : i < (l₁ ++ l₂).length
h' : ¬i < l₁.length
⊢ (l₁ ++ l₂)[i] = l₂[i - l₁.length]

Tactic:
rw [getElem_append_right (by simpa using h')]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
i : Nat
h : i < (l₁ ++ l₂).length
h' : ¬i < l₁.length
⊢ l₁.length ≤ i

Tactic:
simpa using h'

Result:
no goals
-- Mathlib/Data/Matrix/Reflection.lean
theorem exists_iff : ∀ {m n} (P : Matrix (Fin m) (Fin n) α → Prop), Exists P ↔ ∃ x, P x
  | 0, _, _ => Iff.symm Fin.exists_fin_zero_pi
  | m + 1, n, P => by
    simp only [Exists, FinVec.exists_iff, exists_iff]
    exact Iff.symm Fin.exists_fin_succ_pi

Proof state:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∃ r A, P (of (vecCons r A))) ↔ ∃ x, P x

Tactic:
exact Iff.symm Fin.exists_fin_succ_pi

Result:
no goals

Proof state:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
simp only [Exists, FinVec.exists_iff, exists_iff]

Result:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∃ r A, P (of (vecCons r A))) ↔ ∃ x, P x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h : a ∈ m} :
    get? m a = some (get m a h)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h✝ : m.WF
a : α
h : a ∈ m
⊢ get? m a = some (get m a h)

Tactic:
simp_to_raw using Raw₀.Const.get?_eq_some_get

Result:
no goals