harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem reflBEq_iff : ReflBEq (Option α) ↔ ReflBEq α

Proof state:
case mp
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq (Option α) → ReflBEq α

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Option α)
⊢ ReflBEq α

Proof state:
case mp
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Option α)
⊢ ReflBEq α

Tactic:
constructor

Result:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Option α)
⊢ ∀ {a : α}, (a == a) = true

Proof state:
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Option α)
a : α
this : (some a == some a) = true
⊢ (a == a) = true

Tactic:
simpa only [some_beq_some]

Result:
no goals

Proof state:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Option α)
a : α
⊢ (a == a) = true

Tactic:
suffices (some a == some a) = true by
  simpa only [some_beq_some]

Result:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Option α)
a : α
⊢ (some a == some a) = true

Proof state:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Option α)
⊢ ∀ {a : α}, (a == a) = true

Tactic:
intro a

Result:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Option α)
a : α
⊢ (a == a) = true

Proof state:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Option α)
a : α
⊢ (some a == some a) = true

Tactic:
simp

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq α → ReflBEq (Option α)

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ReflBEq (Option α)

Proof state:
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq (Option α) ↔ ReflBEq α

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq (Option α) → ReflBEq α

case mpr
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq α → ReflBEq (Option α)

Proof state:
case mpr
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ReflBEq (Option α)

Tactic:
constructor

Result:
case mpr.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ∀ {a : Option α}, (a == a) = true

Proof state:
case mpr.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ∀ {a : Option α}, (a == a) = true

Tactic:
rintro (_ | a) <;> simp

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
@[reassoc (attr := simp)]
lemma homologyπ_extendHomologyIso_inv :
    K.homologyπ j ≫ (K.extendHomologyIso e hj').inv =
      (K.extendCyclesIso e hj').inv ≫ (K.extend e).homologyπ j'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.homologyπ j ≫ (K.extendHomologyIso e hj').inv = (K.extendCyclesIso e hj').inv ≫ (K.extend e).homologyπ j'

Tactic:
simp only [← cancel_mono (K.extendHomologyIso e hj').hom,
  assoc, Iso.inv_hom_id, comp_id, homologyπ_extendHomologyIso_hom, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
lemma hasDerivAt_log_sub_logTaylor (n : ℕ) {z : ℂ} (hz : 1 + z ∈ slitPlane) :
    HasDerivAt (fun z : ℂ ↦ log (1 + z) - logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z

Proof state:
case h.e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, (-1) ^ j * z ^ j

Tactic:
simp_rw [← mul_pow, neg_one_mul, geom_sum_eq hz', ← neg_add', div_neg, add_comm z]

Result:
case h.e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - -(((-z) ^ n - 1) / (1 + z))

Proof state:
n : ℕ
z : ℂ
H : z = -1
hz : 0 ∈ slitPlane
⊢ False

Tactic:
exact slitPlane_ne_zero hz rfl

Result:
no goals

Proof state:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ -z ≠ 1

Tactic:
intro H

Result:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : -z = 1
⊢ False

Proof state:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ HasDerivAt (fun z => log (1 + z) - logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z

Tactic:
convert ((hasDerivAt_log hz).comp_const_add 1 z).sub (hasDerivAt_logTaylor n z) using 1

Result:
case h.e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, (-1) ^ j * z ^ j

Proof state:
case h.e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, (-1) ^ j * z ^ j

Tactic:
have hz' : -z ≠ 1 := by
  intro H
  rw [neg_eq_iff_eq_neg] at H
  simp only [H, add_neg_cancel] at hz
  exact slitPlane_ne_zero hz rfl

Result:
case h.e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, (-1) ^ j * z ^ j

Proof state:
case h.e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - -(((-z) ^ n - 1) / (1 + z))

Tactic:
field_simp [slitPlane_ne_zero hz]

Result:
no goals

Proof state:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : -z = 1
⊢ False

Tactic:
rw [neg_eq_iff_eq_neg] at H

Result:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : z = -1
⊢ False

Proof state:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : z = -1
⊢ False

Tactic:
simp only [H, add_neg_cancel] at hz

Result:
n : ℕ
z : ℂ
H : z = -1
hz : 0 ∈ slitPlane
⊢ False
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_rel₁ {R : L.Relations 1} {t : L.Term _} :
    (R.formula₁ t).Realize v ↔ RelMap R ![t.realize v]

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
x✝ : Fin 1
⊢ Term.realize v (![t] x✝) = ![Term.realize v t] x✝

Tactic:
simp only [Matrix.cons_val_fin_one]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (RelMap R fun i => Term.realize v (![t] i)) = RelMap R ![Term.realize v t]

Tactic:
refine congr rfl (funext fun _ => ?_)

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
x✝ : Fin 1
⊢ Term.realize v (![t] x✝) = ![Term.realize v t] x✝

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (R.formula₁ t).Realize v ↔ RelMap R ![Term.realize v t]

Tactic:
rw [Relations.formula₁, realize_rel, iff_eq_eq]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (RelMap R fun i => Term.realize v (![t] i)) = RelMap R ![Term.realize v t]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = false) : x < 2^n

Proof state:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
not_lt : ¬x < 2 ^ n
x_ge_n : x ≥ 2 ^ n
i : Nat
i_ge_n : i ≥ n
test_true : x.testBit i = true
⊢ False

Tactic:
have test_false := p _ i_ge_n

Result:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
not_lt : ¬x < 2 ^ n
x_ge_n : x ≥ 2 ^ n
i : Nat
i_ge_n : i ≥ n
test_true : x.testBit i = true
test_false : x.testBit i = false
⊢ False

Proof state:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
not_lt : ¬x < 2 ^ n
x_ge_n : x ≥ 2 ^ n
i : Nat
i_ge_n : i ≥ n
test_true : x.testBit i = true
test_false : x.testBit i = false
⊢ False

Tactic:
simp [test_true] at test_false

Result:
no goals

Proof state:
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
⊢ x < 2 ^ n

Tactic:
apply Decidable.by_contra

Result:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
⊢ ¬x < 2 ^ n → False

Proof state:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
not_lt : ¬x < 2 ^ n
⊢ False

Tactic:
have x_ge_n := Nat.ge_of_not_lt not_lt

Result:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
not_lt : ¬x < 2 ^ n
x_ge_n : x ≥ 2 ^ n
⊢ False

Proof state:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
⊢ ¬x < 2 ^ n → False

Tactic:
intro not_lt

Result:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
not_lt : ¬x < 2 ^ n
⊢ False

Proof state:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
not_lt : ¬x < 2 ^ n
x_ge_n : x ≥ 2 ^ n
⊢ False

Tactic:
have ⟨i, ⟨i_ge_n, test_true⟩⟩ := ge_two_pow_implies_high_bit_true x_ge_n

Result:
case a
n x : Nat
p : ∀ (i : Nat), i ≥ n → x.testBit i = false
not_lt : ¬x < 2 ^ n
x_ge_n : x ≥ 2 ^ n
i : Nat
i_ge_n : i ≥ n
test_true : x.testBit i = true
⊢ False
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem AnalyticSet.measurableSet_of_compl [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α]
    {s : Set α} (hs : AnalyticSet s) (hsc : AnalyticSet sᶜ) : MeasurableSet s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
u : Set α
hsu : s ⊆ u
hdu : Disjoint sᶜ u
hmu : MeasurableSet u
⊢ MeasurableSet s

Tactic:
obtain rfl : s = u := hsu.antisymm (disjoint_compl_left_iff_subset.1 hdu)

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
hsu : s ⊆ s
hdu : Disjoint sᶜ s
hmu : MeasurableSet s
⊢ MeasurableSet s

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
⊢ MeasurableSet s

Tactic:
rcases hs.measurablySeparable hsc disjoint_compl_right with ⟨u, hsu, hdu, hmu⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
u : Set α
hsu : s ⊆ u
hdu : Disjoint sᶜ u
hmu : MeasurableSet u
⊢ MeasurableSet s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
hsu : s ⊆ s
hdu : Disjoint sᶜ s
hmu : MeasurableSet s
⊢ MeasurableSet s

Tactic:
exact hmu

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem summable_const_div_iff (h : a ≠ 0) : (Summable fun i ↦ a / f i) ↔ Summable (1 / f)

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
⊢ (Summable fun i => a / f i) ↔ Summable (1 / f)

Tactic:
simpa only [div_eq_mul_inv, one_mul] using summable_mul_left_iff h

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem valid_next {p : Pos} (h : p.Valid s) (h₂ : p < s.endPos) : (next s p).Valid s

Proof state:
s : String
p : Pos
h : Pos.Valid s p
cs : List Char
h₂ : { byteIdx := utf8ByteSize.go cs } < { data := cs ++ [] }.endPos
⊢ Pos.Valid { data := cs ++ [] } ({ data := cs ++ [] }.next { byteIdx := utf8ByteSize.go cs })

Tactic:
simp at h₂

Result:
no goals

Proof state:
s : String
p : Pos
h : Pos.Valid s p
cs : List Char
c : Char
cs' : List Char
h₂ : { byteIdx := utf8ByteSize.go cs } < { data := cs ++ c :: cs' }.endPos
⊢ Pos.Valid { data := cs ++ c :: cs' } ({ data := cs ++ c :: cs' }.next { byteIdx := utf8ByteSize.go cs })

Tactic:
rw [utf8ByteSize.go_eq, next_of_valid]

Result:
s : String
p : Pos
h : Pos.Valid s p
cs : List Char
c : Char
cs' : List Char
h₂ : { byteIdx := utf8ByteSize.go cs } < { data := cs ++ c :: cs' }.endPos
⊢ Pos.Valid { data := cs ++ c :: cs' } { byteIdx := utf8Len cs + c.utf8Size }

Proof state:
s : String
p : Pos
h : Pos.Valid s p
cs : List Char
c : Char
cs' : List Char
h₂ : { byteIdx := utf8ByteSize.go cs } < { data := cs ++ c :: cs' }.endPos
⊢ Pos.Valid { data := cs ++ c :: cs' } { byteIdx := utf8Len cs + c.utf8Size }

Tactic:
simpa using Pos.Valid.mk (cs ++ [c]) cs'

Result:
no goals

Proof state:
s : String
p : Pos
h : Pos.Valid s p
h₂ : p < s.endPos
⊢ Pos.Valid s (s.next p)

Tactic:
match s, p, h with
| ⟨_⟩, ⟨_⟩, ⟨cs, [], rfl, rfl⟩ => simp at h₂
| ⟨_⟩, ⟨_⟩, ⟨cs, c::cs', rfl, rfl⟩ =>
  rw [utf8ByteSize.go_eq, next_of_valid]
  simpa using Pos.Valid.mk (cs ++ [c]) cs'

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/LinearMap.lean
theorem rank_zero [Nontrivial K] : rank (0 : V →ₗ[K] V') = 0

Proof state:
K : Type u
V : Type v
V' : Type v'
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V'
inst✝ : Nontrivial K
⊢ rank 0 = 0

Tactic:
rw [rank, LinearMap.range_zero, rank_bot]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- The norm, relative to `ℤ`, of `ζ ^ p ^ s - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ`
is p ^ p ^ s` if `s ≤ k` and `p ^ (k - s + 1) ≠ 2`. -/
lemma norm_toInteger_pow_sub_one_of_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) {s : ℕ} (hs : s ≤ k) (htwo : p ^ (k - s + 1) ≠ 2) :
    Algebra.norm ℤ (hζ.toInteger ^ (p : ℕ) ^ s - 1) = p ^ (p : ℕ) ^ s

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s

Tactic:
rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) rfl.le]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ ↑p ^ s - 1)) = (algebraMap ℤ ℚ) (↑↑p ^ ↑p ^ s)

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ ↑p ^ s - 1)) = (algebraMap ℤ ℚ) (↑↑p ^ ↑p ^ s)

Tactic:
simp [hζ.norm_pow_sub_one_of_prime_pow_ne_two
        (cyclotomic.irreducible_rat (by simp only [PNat.pow_coe, gt_iff_lt, PNat.pos, pow_pos]))
        hs htwo]

Result:
no goals

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ 0 < ↑(p ^ (k + 1))

Tactic:
simp only [PNat.pow_coe, gt_iff_lt, PNat.pos, pow_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem lt_ediv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a / b + 1) * b

Proof state:
a b : Int
H : 0 < b
⊢ a < b * (a / b) + b

Tactic:
exact Int.lt_add_of_sub_left_lt <| Int.emod_def .. ▸ emod_lt_of_pos _ H

Result:
no goals

Proof state:
a b : Int
H : 0 < b
⊢ a < (a / b + 1) * b

Tactic:
rw [Int.add_mul, Int.one_mul, Int.mul_comm]

Result:
a b : Int
H : 0 < b
⊢ a < b * (a / b) + b
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
theorem LFunction_ne_zero_of_re_eq_one {s : ℂ} (hs : s.re = 1) (hχs : χ ≠ 1 ∨ s ≠ 1) :
    LFunction χ s ≠ 0

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
⊢ LFunction χ s ≠ 0

Tactic:
by_cases h : χ ^ 2 = 1 ∧ s = 1

Result:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : χ ^ 2 = 1 ∧ s = 1
⊢ LFunction χ s ≠ 0

case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
⊢ LFunction χ s ≠ 0

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
⊢ s = 1 + I * ↑s.im

Tactic:
conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : χ ^ 2 ≠ 1 ∨ I * ↑s.im ≠ 0
hs' : s = 1 + I * ↑s.im
H : I * ↑s.im ≠ 0
⊢ s.im ≠ 0

Tactic:
exact_mod_cast right_ne_zero_of_mul H

Result:
no goals

Proof state:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : χ ^ 2 = 1 ∧ s = 1
⊢ LFunction χ s ≠ 0

Tactic:
exact h.2 ▸ LFunction_apply_one_ne_zero_of_quadratic h.1 <| hχs.neg_resolve_right h.2

Result:
no goals

Proof state:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : χ ^ 2 ≠ 1 ∨ I * ↑s.im ≠ 0
hs' : s = 1 + I * ↑s.im
⊢ LFunction χ s ≠ 0

Tactic:
replace h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0 :=
  h.imp_right (fun H ↦ by exact_mod_cast right_ne_zero_of_mul H)

Result:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
hs' : s = 1 + I * ↑s.im
h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0
⊢ LFunction χ s ≠ 0

Proof state:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
hs' : s = 1 + I * ↑s.im
h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0
⊢ LFunction χ s ≠ 0

Tactic:
exact hs'.symm ▸ χ.LFunction_ne_zero_of_not_quadratic_or_ne_one h

Result:
no goals

Proof state:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
hs' : s = 1 + I * ↑s.im
⊢ LFunction χ s ≠ 0

Tactic:
rw [not_and_or, ← ne_eq, ← ne_eq, hs', add_right_ne_self] at h

Result:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : χ ^ 2 ≠ 1 ∨ I * ↑s.im ≠ 0
hs' : s = 1 + I * ↑s.im
⊢ LFunction χ s ≠ 0

Proof state:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
⊢ LFunction χ s ≠ 0

Tactic:
have hs' : s = 1 + I * s.im := by
  conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]

Result:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
hs' : s = 1 + I * ↑s.im
⊢ LFunction χ s ≠ 0
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
theorem card_parts_equitabilise (hm : m ≠ 0) : #(P.equitabilise h).parts = a + b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #(equitabilise h).parts = a + b

Tactic:
rw [← filter_true_of_mem fun x => card_eq_of_mem_parts_equitabilise, filter_or,
  card_union_of_disjoint, P.card_filter_equitabilise_small _ hm, P.card_filter_equitabilise_big]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ Disjoint (filter (fun x => #x = m) (equitabilise h).parts) (filter (fun x => #x = m + 1) (equitabilise h).parts)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ Disjoint (filter (fun x => #x = m) (equitabilise h).parts) (filter (fun x => #x = m + 1) (equitabilise h).parts)

Tactic:
exact disjoint_filter.2 fun x _ h₀ h₁ => Nat.succ_ne_self m <| h₁.symm.trans h₀

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem mul_generator_self_inv {R₁ : Type*} [CommRing R₁] [Algebra R₁ K] [IsLocalization R₁⁰ K]
    (I : FractionalIdeal R₁⁰ K) [Submodule.IsPrincipal (I : Submodule R₁ K)] (h : I ≠ 0) :
    I * spanSingleton _ (generator (I : Submodule R₁ K))⁻¹ = 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ generator ↑I ≠ 0

Tactic:
intro generator_I_eq_zero

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ False

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ I * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1

Tactic:
conv_lhs => congr; rw [eq_spanSingleton_of_principal I]

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ spanSingleton R₁⁰ (generator ↑I) * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ False

Tactic:
apply h

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ I = 0

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ I = 0

Tactic:
rw [eq_spanSingleton_of_principal I, generator_I_eq_zero, spanSingleton_zero]

Result:
no goals

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ spanSingleton R₁⁰ (generator ↑I) * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1

Tactic:
rw [spanSingleton_mul_spanSingleton, mul_inv_cancel₀, spanSingleton_one]

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ generator ↑I ≠ 0
-- Mathlib/Order/WithBot.lean
lemma forall_lt_iff_eq_bot : (∀ b : α, x < b) ↔ x = ⊥

Proof state:
α : Type u_1
inst✝ : Preorder α
x : WithBot α
⊢ (∀ (b : α), x < ↑b) ↔ x = ⊥

Tactic:
cases x <;> simp

Result:
case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ∃ x, ¬a✝ < x

Proof state:
case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ∃ x, ¬a✝ < x

Tactic:
simpa using ⟨_, lt_irrefl _⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp] lemma getVert_tail {u v n} (p : G.Walk u v) :
    p.tail.getVert n = p.getVert (n + 1)

Proof state:
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
⊢ (cons h q).tail.getVert n = (cons h q).getVert (n + 1)

Tactic:
simp only [getVert_cons_succ, tail_cons_eq, getVert_cons]

Result:
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
⊢ (q.copy ⋯ ⋯).getVert n = q.getVert n

Proof state:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
⊢ p.tail.getVert n = p.getVert (n + 1)

Tactic:
match p with
| .nil => rfl
| .cons h q =>
  simp only [getVert_cons_succ, tail_cons_eq, getVert_cons]
  exact getVert_copy q n (getVert_zero q).symm rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
⊢ (q.copy ⋯ ⋯).getVert n = q.getVert n

Tactic:
exact getVert_copy q n (getVert_zero q).symm rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
⊢ nil.tail.getVert n = nil.getVert (n + 1)

Tactic:
rfl

Result:
no goals