harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem discr_odd_prime' [IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) (hodd : p ≠ 2) :
    discr ℚ (hζ.subOnePowerBasis ℚ).basis = (-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) - 2)

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Tactic:
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

Tactic:
rw [← discr_odd_prime hζ (cyclotomic.irreducible_rat hp.out.pos) hodd]

Result:
p : ℕ+
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_add_toIcoDiv_zsmul (a b : α) : toIcoMod hp a b + toIcoDiv hp a b • p = b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b + toIcoDiv hp a b • p = b

Tactic:
rw [toIcoMod, sub_add_cancel]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_floor (x : α) : ∃ fl : ℤ, ∀ z : ℤ, z ≤ fl ↔ (z : α) ≤ x

Proof state:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this : (a : Prop) → Decidable a
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

Tactic:
have : ∃ ub : ℤ, (ub : α) ≤ x ∧ ∀ z : ℤ, (z : α) ≤ x → z ≤ ub :=
  Int.exists_greatest_of_bdd
    (let ⟨n, hn⟩ := exists_int_gt x
    ⟨n, fun z h' => Int.cast_le.1 <| le_trans h' <| le_of_lt hn⟩)
    (let ⟨n, hn⟩ := exists_int_lt x
    ⟨n, le_of_lt hn⟩)

Result:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

Proof state:
case intro
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl z : ℤ
h₁ : ↑fl ≤ x
h₂ : ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
⊢ z ≤ fl ↔ ↑z ≤ x

Tactic:
exact ⟨fun h => le_trans (Int.cast_le.2 h) h₁, h₂ z⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

Tactic:
refine this.imp fun fl h z => ?_

Result:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl : ℤ
h : ↑fl ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
z : ℤ
⊢ z ≤ fl ↔ ↑z ≤ x

Proof state:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl : ℤ
h : ↑fl ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
z : ℤ
⊢ z ≤ fl ↔ ↑z ≤ x

Tactic:
obtain ⟨h₁, h₂⟩ := h

Result:
case intro
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl z : ℤ
h₁ : ↑fl ≤ x
h₂ : ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
⊢ z ≤ fl ↔ ↑z ≤ x

Proof state:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

Tactic:
haveI := Classical.propDecidable

Result:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this : (a : Prop) → Decidable a
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_prod {ι ι' α β} (s : ι → Set α) (t : ι' → Set β) :
    ⋃ x : ι × ι', s x.1 ×ˢ t x.2 = (⋃ i : ι, s i) ×ˢ ⋃ i : ι', t i

Proof state:
case h
ι : Type u_12
ι' : Type u_13
α : Type u_14
β : Type u_15
s : ι → Set α
t : ι' → Set β
x✝ : α × β
⊢ x✝ ∈ ⋃ x, s x.1 ×ˢ t x.2 ↔ x✝ ∈ (⋃ i, s i) ×ˢ ⋃ i, t i

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_12
ι' : Type u_13
α : Type u_14
β : Type u_15
s : ι → Set α
t : ι' → Set β
⊢ ⋃ x, s x.1 ×ˢ t x.2 = (⋃ i, s i) ×ˢ ⋃ i, t i

Tactic:
ext

Result:
case h
ι : Type u_12
ι' : Type u_13
α : Type u_14
β : Type u_15
s : ι → Set α
t : ι' → Set β
x✝ : α × β
⊢ x✝ ∈ ⋃ x, s x.1 ×ˢ t x.2 ↔ x✝ ∈ (⋃ i, s i) ×ˢ ⋃ i, t i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem reverse_attach (xs : Vector α n) :
    xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩

Proof state:
α : Type ?u.63302
n : Nat
xs : Vector α n
x✝ : { x // x ∈ xs.reverse }
x : α
h : x ∈ xs.reverse
⊢ x ∈ xs

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.reverse =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse.attach

Tactic:
simp [Array.map_attachWith]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
⊢ xs.attach.reverse =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.reverse.attach

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.reverse =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse.attach
-- Mathlib/Data/Rel.lean
theorem comp_right_id (r : Rel α β) : r • @Eq β = r

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ r • Eq = r

Tactic:
unfold comp

Result:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (fun x z => ∃ y, r x y ∧ y = z) = r

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
r : Rel α β
y : α
x✝ : β
⊢ (∃ y_1, r y y_1 ∧ y_1 = x✝) ↔ r y x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (fun x z => ∃ y, r x y ∧ y = z) = r

Tactic:
ext y

Result:
case a.h.a
α : Type u_1
β : Type u_2
r : Rel α β
y : α
x✝ : β
⊢ (∃ y_1, r y y_1 ∧ y_1 = x✝) ↔ r y x✝
-- Mathlib/Data/Nat/Nth.lean
theorem nth_of_forall_not {n : ℕ} (hp : ∀ n' ≥ n, ¬p n') : nth p n = 0

Proof state:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ ↑(range n)
⊢ ⋯.toFinset ⊆ range n

Tactic:
exact Set.Finite.toFinset_subset.mpr this

Result:
no goals

Proof state:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
⊢ setOf p ⊆ ↑(range n)

Tactic:
intro n' hn'

Result:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
n' : ℕ
hn' : n' ∈ setOf p
⊢ n' ∈ ↑(range n)

Proof state:
p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ setOf p
hp : n' ∉ ↑(range n)
⊢ n' ≥ n

Tactic:
simpa using hp

Result:
no goals

Proof state:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
n' : ℕ
hn' : n' ∈ setOf p
⊢ n' ∈ ↑(range n)

Tactic:
contrapose! hp

Result:
p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ setOf p
hp : n' ∉ ↑(range n)
⊢ ∃ n' ≥ n, p n'

Proof state:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ ↑(range n)
⊢ nth p n = 0

Tactic:
rw [nth_of_card_le ((finite_toSet _).subset this)]

Result:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ ↑(range n)
⊢ #⋯.toFinset ≤ n

Proof state:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ ↑(range n)
⊢ #⋯.toFinset ≤ n

Tactic:
refine (Finset.card_le_card ?_).trans_eq (Finset.card_range n)

Result:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ ↑(range n)
⊢ ⋯.toFinset ⊆ range n

Proof state:
p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ setOf p
hp : n' ∉ ↑(range n)
⊢ ∃ n' ≥ n, p n'

Tactic:
exact ⟨n', by simpa using hp, Set.mem_setOf.mp hn'⟩

Result:
no goals

Proof state:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
⊢ nth p n = 0

Tactic:
have : setOf p ⊆ Finset.range n := by
  intro n' hn'
  contrapose! hp
  exact ⟨n', by simpa using hp, Set.mem_setOf.mp hn'⟩

Result:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ ↑(range n)
⊢ nth p n = 0
-- Mathlib/Algebra/FreeMonoid/Count.lean
lemma count_of [DecidableEq α] (x y : α) : count x (of y) = (Pi.single x 1 : α → ℕ) y

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (if y = x then 1 else 0) = Pi.single x 1 y

Tactic:
simp [Pi.single, Function.update]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (count x) (of y) = Pi.single x 1 y

Tactic:
dsimp [count]

Result:
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (countP fun x_1 => x_1 = x) (of y) = Pi.single x 1 y

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (countP fun x_1 => x_1 = x) (of y) = Pi.single x 1 y

Tactic:
rw [countP_of]

Result:
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (if y = x then 1 else 0) = Pi.single x 1 y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem toList_attachWith {l : Array α} {P : α → Prop} {H : ∀ x ∈ l, P x} :
   (l.attachWith P H).toList = l.toList.attachWith P (by simpa [mem_toList] using H)

Proof state:
α : Type ?u.2437
l : Array α
P : α → Prop
H : ∀ (x : α), x ∈ l → P x
⊢ ∀ (x : α), x ∈ l.toList → P x

Tactic:
simpa [mem_toList] using H

Result:
no goals

Proof state:
α : Type u_1
l : Array α
P : α → Prop
H : ∀ (x : α), x ∈ l → P x
⊢ (l.attachWith P H).toList = l.toList.attachWith P ⋯

Tactic:
simp [attachWith]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_def (a b : Int) : a % b = a - b * (a / b)

Proof state:
a b : Int
⊢ a % b = a - b * (a / b)

Tactic:
rw [← Int.add_sub_cancel (a % b), emod_add_ediv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem sle_eq_carry (x y : BitVec w) :
    x.sle y = !((x.msb == y.msb).xor (carry w y (~~~x) true))

Proof state:
w : Nat
x y : BitVec w
⊢ x.sle y = !(x.msb == y.msb ^^ carry w y (~~~x) true)

Tactic:
rw [sle_eq_not_slt, slt_eq_not_carry, beq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_adjunction_id {L R : C ⥤ C} (adj : L ⊣ R) (α : 𝟭 C ⟶ L) (c : C) :
    (conjugateEquiv adj Adjunction.id α).app c = α.app (R.obj c) ≫ adj.counit.app c

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
L R : C ⥤ C
adj : L ⊣ R
α : 𝟭 C ⟶ L
c : C
⊢ ((conjugateEquiv adj Adjunction.id) α).app c = α.app (R.obj c) ≫ adj.counit.app c

Tactic:
simp [conjugateEquiv, mateEquiv, Adjunction.id]

Result:
no goals
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem IsOpen.exists_msmooth_support_eq {s : Set M} (hs : IsOpen s) :
    ∃ f : M → ℝ, f.support = s ∧ ContMDiff I 𝓘(ℝ) ∞ f ∧ ∀ x, 0 ≤ f x

Proof state:
case pos
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x c : M
Hx : x ∈ tsupport ⇑(f c)
hx : ↑(chartAt H c) x ∈ (chartAt H c).target ∧ x ∈ s
⊢ x ∈ s

Tactic:
exact hx.2

Result:
no goals
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem isUniversalColimit_extendCofan {n : ℕ} (f : Fin (n + 1) → C)
    {c₁ : Cofan fun i : Fin n ↦ f i.succ} {c₂ : BinaryCofan (f 0) c₁.pt}
    (t₁ : IsUniversalColimit c₁) (t₂ : IsUniversalColimit c₂)
    [∀ {Z} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i] :
    IsUniversalColimit (extendCofan c₁ c₂)

Proof state:
case refine_4.intro.refine_3.intro.mk.succ
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
H₁ :
  IsColimit
    (Cofan.mk (pullback c₂.inr i) fun j =>
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
H₂ : IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i))
i✝ : Fin n
a✝ : Fin.cases (c.ι.app { as := 0 }) (fun i => c.ι.app { as := i.succ }) i✝.castSucc = c.ι.app { as := i✝.castSucc }
⊢ Fin.cases (c.ι.app { as := 0 }) (fun i => c.ι.app { as := i.succ }) i✝.succ = c.ι.app { as := i✝.succ }

Tactic:
simp only [Fin.cases_succ]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_lt_one_of_one_lt_of_neg {x : ℝ≥0∞} {z : ℝ} (hx : 1 < x) (hz : z < 0) : x ^ z < 1

Proof state:
case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 < x✝
⊢ ↑x✝ ^ z < 1

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)),
  NNReal.rpow_lt_one_of_one_lt_of_neg hx hz]

Result:
no goals

Proof state:
case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 < ↑x✝
⊢ ↑x✝ ^ z < 1

Tactic:
simp only [some_eq_coe, one_lt_coe_iff] at hx

Result:
case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 < x✝
⊢ ↑x✝ ^ z < 1

Proof state:
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1

Tactic:
cases x

Result:
case top
z : ℝ
hz : z < 0
hx : 1 < ⊤
⊢ ⊤ ^ z < 1

case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 < ↑x✝
⊢ ↑x✝ ^ z < 1

Proof state:
case top
z : ℝ
hz : z < 0
hx : 1 < ⊤
⊢ ⊤ ^ z < 1

Tactic:
simp [top_rpow_of_neg hz, zero_lt_one]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem eq_of_mem_ordConnectedSection_of_uIcc_subset (hx : x ∈ ordConnectedSection s)
    (hy : y ∈ ordConnectedSection s) (h : [[x, y]] ⊆ s) : x = y

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : α
hx : x ∈ s.ordConnectedSection
hy : y ∈ s.ordConnectedSection
h : [[x, y]] ⊆ s
⊢ x = y

Tactic:
rcases hx with ⟨x, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
y : α
hy : y ∈ s.ordConnectedSection
x : ↑s
h : [[s.ordConnectedProj x, y]] ⊆ s
⊢ s.ordConnectedProj x = y

Proof state:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[s.ordConnectedProj x, s.ordConnectedProj y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
exact
  ordConnectedProj_eq.2
    (mem_ordConnectedComponent_trans
      (mem_ordConnectedComponent_trans (ordConnectedProj_mem_ordConnectedComponent _ _) h)
      (mem_ordConnectedComponent_ordConnectedProj _ _))

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
y : α
hy : y ∈ s.ordConnectedSection
x : ↑s
h : [[s.ordConnectedProj x, y]] ⊆ s
⊢ s.ordConnectedProj x = y

Tactic:
rcases hy with ⟨y, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[s.ordConnectedProj x, s.ordConnectedProj y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem length_eraseIdx (l : List α) (i : Nat) :
    (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length

Proof state:
case cons.zero
α : Type u_1
x : α
l : List α
ih : ∀ (i : Nat), (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
⊢ ((x :: l).eraseIdx 0).length = if 0 < (x :: l).length then (x :: l).length - 1 else (x :: l).length

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
i : Nat
⊢ ([].eraseIdx i).length = if i < [].length then [].length - 1 else [].length

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ.isTrue
α : Type u_1
x : α
l : List α
ih : ∀ (i : Nat), (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
i : Nat
h✝ : i < l.length
⊢ l.length - 1 + 1 = l.length

Tactic:
cases l <;> simp_all

Result:
no goals

Proof state:
case cons.succ.isFalse
α : Type u_1
x : α
l : List α
ih : ∀ (i : Nat), (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
i : Nat
h✝ : ¬i < l.length
⊢ l.length + 1 = l.length + 1

Tactic:
rfl

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
x : α
l : List α
ih : ∀ (i : Nat), (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
i : Nat
⊢ ((x :: l).eraseIdx (i + 1)).length = if i + 1 < (x :: l).length then (x :: l).length - 1 else (x :: l).length

Tactic:
simp only [eraseIdx, length_cons, ih, add_one_lt_add_one_iff, Nat.add_one_sub_one]

Result:
case cons.succ
α : Type u_1
x : α
l : List α
ih : ∀ (i : Nat), (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
i : Nat
⊢ (if i < l.length then l.length - 1 else l.length) + 1 = if i < l.length then l.length else l.length + 1

Proof state:
case cons.succ
α : Type u_1
x : α
l : List α
ih : ∀ (i : Nat), (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
i : Nat
⊢ (if i < l.length then l.length - 1 else l.length) + 1 = if i < l.length then l.length else l.length + 1

Tactic:
split

Result:
case cons.succ.isTrue
α : Type u_1
x : α
l : List α
ih : ∀ (i : Nat), (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
i : Nat
h✝ : i < l.length
⊢ l.length - 1 + 1 = l.length

case cons.succ.isFalse
α : Type u_1
x : α
l : List α
ih : ∀ (i : Nat), (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
i : Nat
h✝ : ¬i < l.length
⊢ l.length + 1 = l.length + 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_nil :
    m.insertMany [] = m

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ (m.insertMany []).val = m

Tactic:
simp [insertMany, Id.run]

Result:
no goals
-- Mathlib/Data/Real/Sign.lean
theorem sign_neg {r : ℝ} : sign (-r) = -sign r

Proof state:
case inr.inr
r : ℝ
hp : 0 < r
⊢ (-r).sign = -r.sign

Tactic:
rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]

Result:
no goals

Proof state:
case inr.inl

⊢ (-0).sign = -sign 0

Tactic:
rw [sign_zero, neg_zero, sign_zero]

Result:
no goals

Proof state:
case inl
r : ℝ
hn : r < 0
⊢ (-r).sign = -r.sign

Tactic:
rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]

Result:
no goals

Proof state:
r : ℝ
⊢ (-r).sign = -r.sign

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Result:
case inl
r : ℝ
hn : r < 0
⊢ (-r).sign = -r.sign

case inr.inl

⊢ (-0).sign = -sign 0

case inr.inr
r : ℝ
hp : 0 < r
⊢ (-r).sign = -r.sign
-- Mathlib/GroupTheory/Perm/Finite.lean
theorem perm_mapsTo_inl_iff_mapsTo_inr {m n : Type*} [Finite m] [Finite n] (σ : Perm (m ⊕ n)) :
    Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl) ↔
      Set.MapsTo σ (Set.range Sum.inr) (Set.range Sum.inr)

Proof state:
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)

Tactic:
constructor <;>
  ( intro h
    classical
      rw [← perm_inv_mapsTo_iff_mapsTo] at h
      intro x
      rcases hx : σ x with l | r)

Result:
case mp.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr

case mp.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr

case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl

Proof state:
case mpr.inr.intro
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : σ (Sum.inl a) = Sum.inr r
⊢ Sum.inr r ∈ Set.range Sum.inl

Tactic:
obtain ⟨y, hy⟩ := h ⟨r, rfl⟩

Result:
case mpr.inr.intro.intro
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : σ (Sum.inl a) = Sum.inr r
y : n
hy : Sum.inr y = σ⁻¹ (Sum.inr r)
⊢ Sum.inr r ∈ Set.range Sum.inl

Proof state:
case mp.inl.intro.intro
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : σ (Sum.inr a) = Sum.inl l
y : m
hy : Sum.inl y = σ⁻¹ (Sum.inl l)
⊢ Sum.inl l ∈ Set.range Sum.inr

Tactic:
rw [← hx, σ.inv_apply_self] at hy

Result:
case mp.inl.intro.intro
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : σ (Sum.inr a) = Sum.inl l
y : m
hy : Sum.inl y = Sum.inr a
⊢ Sum.inl l ∈ Set.range Sum.inr
-- Mathlib/Data/Nat/Log.lean
theorem log_eq_logC : log = logC

Proof state:
case h.h
b m : ℕ
⊢ log b m = logC b m

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case h.h.inl
b m : ℕ
hb : b ≤ 1
⊢ log b m = logC b m

case h.h.inr
b m : ℕ
hb : 1 < b
⊢ log b m = logC b m

Proof state:
case h.h.inl
b m : ℕ
hb : b ≤ 1
⊢ log b m = logC b m

case h.h.inr
b m : ℕ
hb : 1 < b
⊢ log b m = logC b m

Tactic:
case inl => rw [logC_of_left_le_one hb, Nat.log_of_left_le_one hb]

Result:
case h.h.inr
b m : ℕ
hb : 1 < b
⊢ log b m = logC b m

Proof state:
b m : ℕ
hb : 1 < b
hm : m ≠ 0
⊢ log b m = logC b m

Tactic:
rw [Nat.log_eq_iff (Or.inr ⟨hb, hm⟩)]

Result:
b m : ℕ
hb : 1 < b
hm : m ≠ 0
⊢ b ^ logC b m ≤ m ∧ m < b ^ (logC b m + 1)

Proof state:
b m : ℕ
hb : 1 < b
⊢ log b m = logC b m

Tactic:
rcases eq_or_ne m 0 with rfl | hm

Result:
case inl
b : ℕ
hb : 1 < b
⊢ log b 0 = logC b 0

case inr
b m : ℕ
hb : 1 < b
hm : m ≠ 0
⊢ log b m = logC b m

Proof state:
case inl
b : ℕ
hb : 1 < b
⊢ log b 0 = logC b 0

case inr
b m : ℕ
hb : 1 < b
hm : m ≠ 0
⊢ log b m = logC b m

Tactic:
case inl => rw [Nat.log_zero_right, logC_zero]

Result:
case inr
b m : ℕ
hb : 1 < b
hm : m ≠ 0
⊢ log b m = logC b m

Proof state:
b : ℕ
hb : 1 < b
⊢ log b 0 = logC b 0

Tactic:
rw [Nat.log_zero_right, logC_zero]

Result:
no goals

Proof state:
⊢ log = logC

Tactic:
ext b m

Result:
case h.h
b m : ℕ
⊢ log b m = logC b m

Proof state:
b m : ℕ
hb : 1 < b
hm : m ≠ 0
⊢ b ^ logC b m ≤ m ∧ m < b ^ (logC b m + 1)

Tactic:
exact logC_spec hb (zero_lt_of_ne_zero hm)

Result:
no goals

Proof state:
case h.h.inr
b m : ℕ
hb : 1 < b
⊢ log b m = logC b m

Tactic:
case inr =>
  rcases eq_or_ne m 0 with rfl | hm
  case inl => rw [Nat.log_zero_right, logC_zero]
  case inr =>
    rw [Nat.log_eq_iff (Or.inr ⟨hb, hm⟩)]
    exact logC_spec hb (zero_lt_of_ne_zero hm)

Result:
no goals

Proof state:
case inr
b m : ℕ
hb : 1 < b
hm : m ≠ 0
⊢ log b m = logC b m

Tactic:
case inr =>
  rw [Nat.log_eq_iff (Or.inr ⟨hb, hm⟩)]
  exact logC_spec hb (zero_lt_of_ne_zero hm)

Result:
no goals

Proof state:
b m : ℕ
hb : b ≤ 1
⊢ log b m = logC b m

Tactic:
rw [logC_of_left_le_one hb, Nat.log_of_left_le_one hb]

Result:
no goals