harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma pow_lt_one₀ (h₀ : 0 ≤ a) (h₁ : a < 1) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < 1
  | 0, h => (h rfl).elim
  | n + 1, _ => by
    rw [pow_succ']; exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one₀ h₀ h₁.le)

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a * a ^ n < 1

Tactic:
exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one₀ h₀ h₁.le)

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ^ (n + 1) < 1

Tactic:
rw [pow_succ']

Result:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a * a ^ n < 1
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_prime_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) :
    (∀ p : ℕ, p.Prime → d.factorization p ≤ n.factorization p) ↔ d ∣ n

Proof state:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p
p : ℕ
hp : ¬Prime p
⊢ 0 ≤ 0

Tactic:
rfl

Result:
no goals

Proof state:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n

Tactic:
rw [← factorization_le_iff_dvd hd hn]

Result:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d.factorization ≤ n.factorization

Proof state:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p
p : ℕ
hp : ¬Prime p
⊢ d.factorization p ≤ n.factorization p

Tactic:
simp_rw [factorization_eq_zero_of_non_prime _ hp]

Result:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p
p : ℕ
hp : ¬Prime p
⊢ 0 ≤ 0

Proof state:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d.factorization ≤ n.factorization

Tactic:
refine ⟨fun h p => (em p.Prime).elim (h p) fun hp => ?_, fun h p _ => h p⟩

Result:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p
p : ℕ
hp : ¬Prime p
⊢ d.factorization p ≤ n.factorization p
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_transPartialEquiv (e : α ≃ β) (e' : β ≃ γ) (f'' : PartialEquiv γ δ) :
    (e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
e' : β ≃ γ
f'' : PartialEquiv γ δ
⊢ (e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')

Tactic:
simp only [transPartialEquiv_eq_trans, PartialEquiv.trans_assoc, trans_toPartialEquiv]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem next_mem (s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) : s.next hs x hx ∈ s

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ next (Quot.mk (⇑(IsRotated.setoid α)) a✝) hs x hx ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝

Tactic:
apply next_mem

Result:
case h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ x ∈ a✝

Proof state:
case h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ x ∈ a✝

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.next hs x hx ∈ s

Tactic:
induction s using Quot.inductionOn

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ next (Quot.mk (⇑(IsRotated.setoid α)) a✝) hs x hx ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
-- Mathlib/Data/Finsupp/Basic.lean
theorem some_single_some [Zero M] (a : α) (m : M) :
    (single (Option.some a) m : Option α →₀ M).some = single a m

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
⊢ (single (Option.some a) m).some = single a m

Tactic:
ext b

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
b : α
⊢ (single (Option.some a) m).some b = (single a m) b

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
b : α
⊢ (single (Option.some a) m).some b = (single a m) b

Tactic:
simp [single_apply]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
⊢ (single (Option.some a) m).some = single a m

Tactic:
classical
  ext b
  simp [single_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_C (x : R) : taylor r (C x) = C x

Proof state:
R : Type u_1
inst✝ : Semiring R
r x : R
⊢ (taylor r) (C x) = C x

Tactic:
simp only [taylor_apply, C_comp]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integrableOn_Ioo_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) :
    IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioo (0 : ℝ) t) ↔ -1 < s.re

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume
⊢ -1 < s.re

Tactic:
have B : IntegrableOn (fun a ↦ a ^ s.re) (Ioo 0 t) := by
  apply (integrableOn_congr_fun _ measurableSet_Ioo).1 h.norm
  intro a ha
  simp [Complex.norm_cpow_eq_rpow_re_of_pos ha.1]

Result:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume
B : IntegrableOn (fun a => a ^ s.re) (Set.Ioo 0 t) volume
⊢ -1 < s.re

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume
B : IntegrableOn (fun a => a ^ s.re) (Set.Ioo 0 t) volume
⊢ -1 < s.re

Tactic:
rwa [integrableOn_Ioo_rpow_iff ht] at B

Result:
no goals

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
⊢ IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume ↔ -1 < s.re

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simpa [intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
  using intervalIntegrable_cpow' h (a := 0) (b := t)⟩

Result:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume
⊢ -1 < s.re

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume
a : ℝ
ha : a ∈ Set.Ioo 0 t
⊢ (fun a => ‖↑a ^ s‖) a = (fun a => a ^ s.re) a

Tactic:
simp [Complex.norm_cpow_eq_rpow_re_of_pos ha.1]

Result:
no goals

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume
⊢ EqOn (fun a => ‖↑a ^ s‖) (fun a => a ^ s.re) (Set.Ioo 0 t)

Tactic:
intro a ha

Result:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume
a : ℝ
ha : a ∈ Set.Ioo 0 t
⊢ (fun a => ‖↑a ^ s‖) a = (fun a => a ^ s.re) a

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume
⊢ IntegrableOn (fun a => a ^ s.re) (Set.Ioo 0 t) volume

Tactic:
apply (integrableOn_congr_fun _ measurableSet_Ioo).1 h.norm

Result:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume
⊢ EqOn (fun a => ‖↑a ^ s‖) (fun a => a ^ s.re) (Set.Ioo 0 t)

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
h : -1 < s.re
⊢ IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume

Tactic:
simpa [intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
using intervalIntegrable_cpow' h (a := 0) (b := t)

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem arith_mean_weighted_of_constant (w z : ι → ℝ) (x : ℝ) (hw' : ∑ i ∈ s, w i = 1)
    (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) : ∑ i ∈ s, w i * z i = x :=
  calc
    ∑ i ∈ s, w i * z i = ∑ i ∈ s, w i * x

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
⊢ ∑ i ∈ s, w i * z i = ∑ i ∈ s, w i * x

Tactic:
refine sum_congr rfl fun i hi => ?_

Result:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
⊢ w i * z i = w i * x

Proof state:
case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i = 0
⊢ w i * z i = w i * x

Tactic:
rw [hwi, zero_mul, zero_mul]

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
⊢ w i * z i = w i * x

Tactic:
rcases eq_or_ne (w i) 0 with hwi | hwi

Result:
case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i = 0
⊢ w i * z i = w i * x

case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i ≠ 0
⊢ w i * z i = w i * x

Proof state:
case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i ≠ 0
⊢ w i * z i = w i * x

Tactic:
rw [hx i hi hwi]

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
⊢ ∑ i ∈ s, w i * x = x

Tactic:
rw [← sum_mul, hw', one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
theorem NatTrans.leftDerived_comp {F G H : C ⥤ D} [F.Additive] [G.Additive] [H.Additive]
    (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) :
    NatTrans.leftDerived (α ≫ β) n = NatTrans.leftDerived α n ≫ NatTrans.leftDerived β n

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_1
inst✝⁶ : Category.{u_2, u_1} D
inst✝⁵ : Abelian C
inst✝⁴ : HasProjectiveResolutions C
inst✝³ : Abelian D
F G H : C ⥤ D
inst✝² : F.Additive
inst✝¹ : G.Additive
inst✝ : H.Additive
α : F ⟶ G
β : G ⟶ H
n : ℕ
⊢ leftDerived (α ≫ β) n = leftDerived α n ≫ leftDerived β n

Tactic:
simp [NatTrans.leftDerived]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
theorem chromaticNumber_cycleGraph_of_even (n : ℕ) (h : 2 ≤ n) (hEven : Even n) :
    (cycleGraph n).chromaticNumber = 2

Proof state:
case a
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
hadj : (cycleGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩
⊢ 2 ≤ (cycleGraph n).chromaticNumber

Tactic:
exact two_le_chromaticNumber_of_adj hadj

Result:
no goals

Proof state:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).chromaticNumber = 2

Tactic:
apply le_antisymm

Result:
case a
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).chromaticNumber ≤ 2

case a
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ 2 ≤ (cycleGraph n).chromaticNumber

Proof state:
case a
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).chromaticNumber ≤ 2

Tactic:
apply hc.chromaticNumber_le

Result:
no goals

Proof state:
case a
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ 2 ≤ (cycleGraph n).chromaticNumber

Tactic:
have hadj : (cycleGraph n).Adj ⟨0, Nat.zero_lt_of_lt h⟩ ⟨1, h⟩ := by
  simp [cycleGraph_adj', Fin.sub_val_of_le]

Result:
case a
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
hadj : (cycleGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩
⊢ 2 ≤ (cycleGraph n).chromaticNumber

Proof state:
n : ℕ
h : 2 ≤ n
hEven : Even n
⊢ (cycleGraph n).chromaticNumber = 2

Tactic:
have hc := (cycleGraph.bicoloring_of_even n hEven).colorable

Result:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).chromaticNumber = 2

Proof state:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩

Tactic:
simp [cycleGraph_adj', Fin.sub_val_of_le]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Odd.add_odd : Odd a → Odd b → Even (a + b)

Proof state:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd a → Odd b → Even (a + b)

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

Result:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Even (2 * a + 1 + (2 * b + 1))

Proof state:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a + a + 1 + (b + b + 1) = a + b + 1 + (a + b + 1)

Tactic:
ac_rfl

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a + 1 + (2 * b + 1) = a + b + 1 + (a + b + 1)

Tactic:
rw [two_mul, two_mul]

Result:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a + a + 1 + (b + b + 1) = a + b + 1 + (a + b + 1)

Proof state:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Even (2 * a + 1 + (2 * b + 1))

Tactic:
refine ⟨a + b + 1, ?_⟩

Result:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a + 1 + (2 * b + 1) = a + b + 1 + (a + b + 1)
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap'_f_of_not_rel_left {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀)
    (hk₀ : ∀ l : ι, ¬c.Rel k₀ l) (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) :
    (nullHomotopicMap' h).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Tactic:
simp only [nullHomotopicMap']

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (dite (c.Rel k₁ k₀) (h k₀ k₁) fun x => 0) ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Tactic:
split_ifs

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ h k₀ k₁ r₁₀ ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ h k₀ k₁ r₁₀ ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Tactic:
rw [nullHomotopicMap_f_of_not_rel_left r₁₀ hk₀]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (dite (c.Rel k₁ k₀) (h k₀ k₁) fun x => 0) ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem conj_cong_is_cong (g : ConjAct SL(2, ℤ)) (Γ : Subgroup SL(2, ℤ))
    (h : IsCongruenceSubgroup Γ) : IsCongruenceSubgroup (g • Γ)

Proof state:
case intro
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Γ(↑N) ≤ Γ
⊢ IsCongruenceSubgroup (g • Γ)

Tactic:
refine ⟨N, ?_⟩

Result:
case intro
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Γ(↑N) ≤ Γ
⊢ Γ(↑N) ≤ g • Γ

Proof state:
case intro
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Γ(↑N) ≤ Γ
⊢ Γ(↑N) ≤ g • Γ

Tactic:
rw [← Gamma_cong_eq_self N g, Subgroup.pointwise_smul_le_pointwise_smul_iff]

Result:
case intro
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Γ(↑N) ≤ Γ
⊢ Γ(↑N) ≤ Γ

Proof state:
case intro
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Γ(↑N) ≤ Γ
⊢ Γ(↑N) ≤ Γ

Tactic:
exact HN

Result:
no goals

Proof state:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
h : IsCongruenceSubgroup Γ
⊢ IsCongruenceSubgroup (g • Γ)

Tactic:
obtain ⟨N, HN⟩ := h

Result:
case intro
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Γ(↑N) ≤ Γ
⊢ IsCongruenceSubgroup (g • Γ)
-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
/-- If the vector field `v` vanishes at `x₀`, then the constant curve at `x₀`
is a global integral curve of `v`. -/
lemma isIntegralCurve_const {x : M} (h : v x = 0) : IsIntegralCurve (fun _ ↦ x) v

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
v : (x : M) → TangentSpace I x
x : M
h : v x = 0
⊢ IsIntegralCurve (fun x_1 => x) v

Tactic:
intro t

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
v : (x : M) → TangentSpace I x
x : M
h : v x = 0
t : ℝ
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (fun x_1 => x) t (ContinuousLinearMap.smulRight 1 (v ((fun x_1 => x) t)))

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
v : (x : M) → TangentSpace I x
x : M
h : v x = 0
t : ℝ
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (fun x_1 => x) t (ContinuousLinearMap.smulRight 1 (v ((fun x_1 => x) t)))

Tactic:
rw [h, ← ContinuousLinearMap.zero_apply (R₁ := ℝ) (R₂ := ℝ) (1 : ℝ),
  ContinuousLinearMap.smulRight_one_one]

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
v : (x : M) → TangentSpace I x
x : M
h : v x = 0
t : ℝ
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (fun x_1 => x) t 0

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
v : (x : M) → TangentSpace I x
x : M
h : v x = 0
t : ℝ
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (fun x_1 => x) t 0

Tactic:
exact hasMFDerivAt_const ..

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_true_imp_eq_false : ∀ {b : Bool}, (b = true → b = false) ↔ (b = false)

Proof state:
⊢ ∀ {b : Bool}, b = true → b = false ↔ b = false

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Order/Group/Basic.lean
@[to_additive zsmul_left_strictMono]
lemma zpow_right_strictMono (ha : 1 < a) : StrictMono fun n : ℤ ↦ a ^ n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 < a
⊢ StrictMono fun n => a ^ n

Tactic:
refine strictMono_int_of_lt_succ fun n ↦ ?_

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ (n + 1)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ (n + 1)

Tactic:
rw [zpow_add_one]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Tactic:
exact lt_mul_of_one_lt_right' (a ^ n) ha

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem disjoint_nhds_atBot_iff : Disjoint (𝓝 a) atBot ↔ ¬IsBot a

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot ↔ ¬IsBot a

Tactic:
constructor

Result:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot → ¬IsBot a

case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ ¬IsBot a → Disjoint (𝓝 a) atBot

Proof state:
case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ (∃ x, ¬a ≤ x) → Disjoint (𝓝 a) atBot

Tactic:
rintro ⟨b, hb⟩

Result:
case mpr.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
⊢ Disjoint (𝓝 a) atBot

Proof state:
case mpr.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
⊢ (Iic b)ᶜ ∈ 𝓝 a

Tactic:
exact isClosed_Iic.isOpen_compl.mem_nhds hb

Result:
no goals

Proof state:
case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ ¬IsBot a → Disjoint (𝓝 a) atBot

Tactic:
simp only [IsBot, not_forall]

Result:
case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ (∃ x, ¬a ≤ x) → Disjoint (𝓝 a) atBot

Proof state:
case mpr.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
⊢ Disjoint (𝓝 a) atBot

Tactic:
refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)

Result:
case mpr.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
⊢ (Iic b)ᶜ ∈ 𝓝 a

Proof state:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) atBot
hbot : IsBot a
⊢ False

Tactic:
rw [hbot.atBot_eq, disjoint_principal_right] at hd

Result:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : (Iic a)ᶜ ∈ 𝓝 a
hbot : IsBot a
⊢ False

Proof state:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : (Iic a)ᶜ ∈ 𝓝 a
hbot : IsBot a
⊢ False

Tactic:
exact mem_of_mem_nhds hd le_rfl

Result:
no goals

Proof state:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot → ¬IsBot a

Tactic:
intro hd hbot

Result:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) atBot
hbot : IsBot a
⊢ False
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem nhdsWithin_Iio_neBot' {b c : α} (H₁ : (Iio c).Nonempty) (H₂ : b ≤ c) :
    NeBot (𝓝[Iio c] b) :=
  mem_closure_iff_nhdsWithin_neBot.1 <| by rwa [closure_Iio' H₁]

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b c : α
H₁ : (Iio c).Nonempty
H₂ : b ≤ c
⊢ b ∈ closure (Iio c)

Tactic:
rwa [closure_Iio' H₁]

Result:
no goals