harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/AdicCompletion/Exactness.lean
theorem map_exact : Function.Exact (map I f) (map I g)

Proof state:
case refine_2
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
⊢ y ∈ ker (map I g) → y ∈ range (map I f)

Tactic:
apply AdicCompletion.induction_on I N y (fun b ↦ ?_)

Result:
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
b : AdicCauchySequence I N
⊢ (mk I N) b ∈ ker (map I g) → (mk I N) b ∈ range (map I f)

Proof state:
case intro.refine_1
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ ker (map I g)
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := AdicCompletion.mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ (fun n => ↑(a n)) (n + 1) ≡ (fun n => ↑(a n)) n [SMOD I ^ n • ⊤]

Tactic:
simp [a, mapExactAux, SModEq]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem div_lt_floor {x : ℝ} (hx : 2 / (1 - 2 / exp 1) ≤ x) : x / exp 1 < (⌊x / 2⌋₊ : ℝ)

Proof state:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 0 < 2

Tactic:
exact zero_lt_two

Result:
no goals

Proof state:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ x / rexp 1 < ↑⌊x / 2⌋₊

Tactic:
apply lt_of_le_of_lt _ (sub_one_lt_floor _)

Result:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ x / rexp 1 ≤ x / 2 - 1

Proof state:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 2 ≠ 0

Tactic:
exact two_ne_zero

Result:
no goals

Proof state:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 2 ≤ 2.7182818283

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 0 < 1 - 2 / rexp 1

Tactic:
rw [sub_pos, div_lt_one (exp_pos _)]

Result:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 2 < rexp 1

Proof state:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 2 < rexp 1

Tactic:
exact lt_of_le_of_lt (by norm_num) exp_one_gt_d9

Result:
no goals

Proof state:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ x / rexp 1 ≤ x / 2 - 1

Tactic:
have : 0 < 1 - 2 / exp 1 := by
  rw [sub_pos, div_lt_one (exp_pos _)]
  exact lt_of_le_of_lt (by norm_num) exp_one_gt_d9

Result:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ x / rexp 1 ≤ x / 2 - 1

Proof state:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ x / rexp 1 ≤ x / 2 - 1

Tactic:
rwa [le_sub_comm, div_eq_mul_one_div x, div_eq_mul_one_div x, ← mul_sub, div_sub', ←
  div_eq_mul_one_div, mul_div_assoc', one_le_div, ← div_le_iff₀ this]

Result:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 0 < 2

x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 2 ≠ 0
-- Mathlib/RingTheory/Radical.lean
theorem radical_ne_zero (a : M) [Nontrivial M] : radical a ≠ 0

Proof state:
case h
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ 0 ∉ (normalizedFactors a).toFinset.val

Tactic:
simp only [Multiset.toFinset_val, Multiset.mem_dedup]

Result:
case h
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ 0 ∉ normalizedFactors a

Proof state:
case h
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ 0 ∉ normalizedFactors a

Tactic:
exact zero_not_mem_normalizedFactors _

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ radical a ≠ 0

Tactic:
rw [radical, ← Finset.prod_val]

Result:
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ (primeFactors a).val.prod ≠ 0

Proof state:
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ (primeFactors a).val.prod ≠ 0

Tactic:
apply Multiset.prod_ne_zero

Result:
case h
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ 0 ∉ (primeFactors a).val

Proof state:
case h
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ 0 ∉ (primeFactors a).val

Tactic:
rw [primeFactors]

Result:
case h
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ 0 ∉ (normalizedFactors a).toFinset.val
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem eq_or_edist_eq_top_of_fixedPoints (hf : ContractingWith K f) {x y} (hx : IsFixedPt f x)
    (hy : IsFixedPt f y) : x = y ∨ edist x y = ∞

Proof state:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
⊢ x = y ∨ edist x y = ⊤

Tactic:
refine or_iff_not_imp_right.2 fun h ↦ edist_le_zero.1 ?_

Result:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
h : ¬edist x y = ⊤
⊢ edist x y ≤ 0

Proof state:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
h : ¬edist x y = ⊤
⊢ edist x y ≤ 0

Tactic:
simpa only [hx.eq, edist_self, add_zero, ENNReal.zero_div] using hf.edist_le_of_fixedPoint h hy

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem expand_card (f : K[X]) : expand K q f = f ^ q

Proof state:
case intro.intro.mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑⟨n, npos⟩
this : Fact (Nat.Prime p)
⊢ (expand K q) f = f ^ q

Tactic:
dsimp at hn

Result:
case intro.intro.mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ n
this : Fact (Nat.Prime p)
⊢ (expand K q) f = f ^ q

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp : CharP K p
⊢ (expand K q) f = f ^ q

Tactic:
letI := hp

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ (expand K q) f = f ^ q

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ (expand K q) f = f ^ q

Tactic:
rcases FiniteField.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩

Result:
case intro.intro.mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp✝ : CharP K p
this : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑⟨n, npos⟩
⊢ (expand K q) f = f ^ q

Proof state:
case intro.intro.mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ n
this : Fact (Nat.Prime p)
⊢ (expand K q) f = f ^ q

Tactic:
rw [hn, ← map_expand_pow_char, frobenius_pow hn, RingHom.one_def, map_id]

Result:
no goals

Proof state:
case intro.intro.mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp✝ : CharP K p
this : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑⟨n, npos⟩
⊢ (expand K q) f = f ^ q

Tactic:
haveI : Fact p.Prime := ⟨hp⟩

Result:
case intro.intro.mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑⟨n, npos⟩
this : Fact (Nat.Prime p)
⊢ (expand K q) f = f ^ q

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
⊢ (expand K q) f = f ^ q

Tactic:
obtain ⟨p, hp⟩ := CharP.exists K

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp : CharP K p
⊢ (expand K q) f = f ^ q
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem tendsto_Ioi_atTop [Preorder α] [IsDirected α (· ≤ ·)]
    {a : α} {f : β → Ioi a} {l : Filter β} :
    Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l atTop

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
f : β → ↑(Ioi a)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop

Tactic:
rw [atTop_Ioi_eq, tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma _root_.IsSl2Triple.h_eq_coroot {α : Weight K H L} (hα : α.IsNonZero)
    {h e f : L} (ht : IsSl2Triple h e f) (heα : e ∈ rootSpace H α) (hfα : f ∈ rootSpace H (- α)) :
    h = coroot α

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
this : ((killingForm K L) e) f = 0
⊢ ↑h = 0

Tactic:
simpa [this] using h_eq

Result:
no goals

Proof state:
case intro.e_self
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
⊢ ∃ s, s • h = coroot α

Tactic:
use (2 • (α α')⁻¹) * (killingForm K L e f)⁻¹

Result:
case h
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
⊢ (2 • (α α')⁻¹ * (((killingForm K L) e) f)⁻¹) • h = coroot α
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx

Proof state:
ctx : Context
e : Expr
⊢ Poly.denote ctx e.toPoly = denote ctx e

Tactic:
simp [toPoly, Expr.denote_toPoly_go]

Result:
no goals
-- Mathlib/Data/List/SplitLengths.lean
theorem length_splitLengths : (sz.splitLengths l).length = sz.length

Proof state:
α : Type u_1
l : List α
sz : List ℕ
⊢ (sz.splitLengths l).length = sz.length

Tactic:
induction sz generalizing l <;> simp [splitLengths, *]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem mk_conjugate_eq (φ : K →+* ℂ) : mk (ComplexEmbedding.conjugate φ) = mk φ

Proof state:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
⊢ mk (ComplexEmbedding.conjugate φ) = mk φ

Tactic:
refine DFunLike.ext _ _ (fun x => ?_)

Result:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
x : K
⊢ (mk (ComplexEmbedding.conjugate φ)) x = (mk φ) x

Proof state:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
x : K
⊢ (mk (ComplexEmbedding.conjugate φ)) x = (mk φ) x

Tactic:
rw [apply, apply, ComplexEmbedding.conjugate_coe_eq, Complex.norm_conj]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/OfSequence.lean
lemma map_le_succ (i : ℕ) : map f i (i + 1) (by omega) = f i

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ map f i (i + 1) ⋯ = f i

Tactic:
revert X f

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f i (i + 1) ⋯ = f i

Proof state:
case succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n✝ : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n✝ (n✝ + 1) ⋯ = f n✝
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ map f (n✝ + 1) (n✝ + 1 + 1) ⋯ = f (n✝ + 1)

Tactic:
apply hi

Result:
no goals

Proof state:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝ : ℕ → C
f✝ : (n : ℕ) → X✝ n ⟶ X✝ (n + 1)
⊢ map f✝ 0 (0 + 1) ⋯ = f✝ 0

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{?u.3471, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ i ≤ i + 1

Tactic:
omega

Result:
no goals

Proof state:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f 0 (0 + 1) ⋯ = f 0

Tactic:
intros

Result:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝ : ℕ → C
f✝ : (n : ℕ) → X✝ n ⟶ X✝ (n + 1)
⊢ map f✝ 0 (0 + 1) ⋯ = f✝ 0

Proof state:
case succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n✝ : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n✝ (n✝ + 1) ⋯ = f n✝
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f (n✝ + 1) (n✝ + 1 + 1) ⋯ = f (n✝ + 1)

Tactic:
intro X f

Result:
case succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n✝ : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n✝ (n✝ + 1) ⋯ = f n✝
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ map f (n✝ + 1) (n✝ + 1 + 1) ⋯ = f (n✝ + 1)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f i (i + 1) ⋯ = f i

Tactic:
induction i with
| zero => intros; rfl
| succ _ hi =>
    intro X f
    apply hi

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem foldl_const (f : α → α) (a : α) (l : List β) :
    l.foldl (fun b _ ↦ f b) a = f^[l.length] a

Proof state:
α : Type u
β : Type v
f : α → α
a : α
l : List β
⊢ foldl (fun b x => f b) a l = f^[l.length] a

Tactic:
induction l generalizing a with
| nil => rfl
| cons b l H => rw [length_cons, foldl, iterate_succ_apply, H]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
f : α → α
a : α
⊢ foldl (fun b x => f b) a [] = f^[[].length] a

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x => f b) a l = f^[l.length] a
a : α
⊢ foldl (fun b x => f b) a (b :: l) = f^[(b :: l).length] a

Tactic:
rw [length_cons, foldl, iterate_succ_apply, H]

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/Basic.lean
/-- For a Lie derivation from a Lie algebra to itself, the usual Leibniz rule holds. -/
lemma apply_lie_eq_add (D : LieDerivation R L L) (a b : L) :
    D ⁅a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
⊢ D ⁅a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆

Tactic:
rw [LieDerivation.apply_lie_eq_sub, sub_eq_add_neg, lie_skew]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem one_sub_le_one (x : Icc (0 : β) 1) : 1 - (x : β) ≤ 1

Proof state:
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Icc 0 1)
⊢ 1 - ↑x ≤ 1

Tactic:
simpa using x.2.1

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma lintegral_ofReal_ne_top_iff_integrable {f : α → ℝ}
    (hfm : AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f) :
    ∫⁻ a, ENNReal.ofReal (f a) ∂μ ≠ ∞ ↔ Integrable f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfm : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ⊤ ↔ Integrable f μ

Tactic:
rw [Integrable, hasFiniteIntegral_iff_ofReal hf]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfm : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ⊤ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfm : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ⊤ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤

Tactic:
simp [hfm]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem mem_divisorsAntidiagonal {x : ℕ × ℕ} :
    x ∈ divisorsAntidiagonal n ↔ x.fst * x.snd = n ∧ n ≠ 0

Proof state:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ n.divisorsAntidiagonal ↔ x.1 * x.2 = n ∧ n ≠ 0

Tactic:
obtain ⟨a, b⟩ := x

Result:
case mk
n a b : ℕ
⊢ (a, b) ∈ n.divisorsAntidiagonal ↔ (a, b).1 * (a, b).2 = n ∧ n ≠ 0

Proof state:
case mk.mp
n a b : ℕ
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b → a * b = n ∧ n ≠ 0

Tactic:
rintro ⟨han, ⟨ha, han'⟩, rfl⟩

Result:
case mk.mp.intro.intro.intro
n a : ℕ
han : a ∣ n
ha : a ≠ 0
han' : a ≤ n
⊢ a * (n / a) = n ∧ n ≠ 0

Proof state:
case mk.mp.intro.intro.intro
n a : ℕ
han : a ∣ n
ha : a ≠ 0
han' : a ≤ n
⊢ ¬n = 0

Tactic:
omega

Result:
no goals

Proof state:
case mk
n a b : ℕ
⊢ (a, b) ∈ n.divisorsAntidiagonal ↔ (a, b).1 * (a, b).2 = n ∧ n ≠ 0

Tactic:
simp only [divisorsAntidiagonal, mul_div_eq_iff_dvd, mem_filterMap, mem_Icc, one_le_iff_ne_zero,
  Option.ite_none_right_eq_some, Option.some.injEq, Prod.ext_iff, and_left_comm, exists_eq_left]

Result:
case mk
n a b : ℕ
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b ↔ a * b = n ∧ n ≠ 0

Proof state:
case mk.mp.intro.intro.intro
n a : ℕ
han : a ∣ n
ha : a ≠ 0
han' : a ≤ n
⊢ a * (n / a) = n ∧ n ≠ 0

Tactic:
simp [Nat.mul_div_eq_iff_dvd, han]

Result:
case mk.mp.intro.intro.intro
n a : ℕ
han : a ∣ n
ha : a ≠ 0
han' : a ≤ n
⊢ ¬n = 0

Proof state:
case mk
n a b : ℕ
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b ↔ a * b = n ∧ n ≠ 0

Tactic:
constructor

Result:
case mk.mp
n a b : ℕ
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b → a * b = n ∧ n ≠ 0

case mk.mpr
n a b : ℕ
⊢ a * b = n ∧ n ≠ 0 → a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b

Proof state:
case mk.mpr
n a b : ℕ
⊢ a * b = n ∧ n ≠ 0 → a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b

Tactic:
rintro ⟨rfl, hab⟩

Result:
case mk.mpr.intro
a b : ℕ
hab : a * b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b

Proof state:
case mk.mpr.intro
a b : ℕ
hab : a * b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b

Tactic:
rw [mul_ne_zero_iff] at hab

Result:
case mk.mpr.intro
a b : ℕ
hab : a ≠ 0 ∧ b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b

Proof state:
case mk.mpr.intro
a b : ℕ
hab : a ≠ 0 ∧ b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b

Tactic:
simpa [hab.1, hab.2] using Nat.le_mul_of_pos_right _ hab.2.bot_lt

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
/-- If there are no vertices then the `minDegree` is zero. -/
@[simp]
lemma minDegree_of_isEmpty [DecidableRel G.Adj] [IsEmpty V] : G.minDegree = 0

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : IsEmpty V
⊢ G.minDegree = 0

Tactic:
rw [minDegree, WithTop.untopD_eq_self_iff]

Result:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : IsEmpty V
⊢ (image (fun v => G.degree v) univ).min = ↑0 ∨ (image (fun v => G.degree v) univ).min = ⊤

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : IsEmpty V
⊢ (image (fun v => G.degree v) univ).min = ↑0 ∨ (image (fun v => G.degree v) univ).min = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Monotone.lean
theorem MonotoneOn.ae_differentiableWithinAt {f : ℝ → ℝ} {s : Set ℝ} (hf : MonotoneOn f s)
    (hs : MeasurableSet s) : ∀ᵐ x ∂volume.restrict s, DifferentiableWithinAt ℝ f s x

Proof state:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict s, DifferentiableWithinAt ℝ f s x

Tactic:
rw [ae_restrict_iff' hs]

Result:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Proof state:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
exact hf.ae_differentiableWithinAt_of_mem

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean
theorem Matrix.rank_vecMulVec {K m n : Type u} [CommRing K] [Fintype n]
    [DecidableEq n] (w : m → K) (v : n → K) : (Matrix.vecMulVec w v).toLin'.rank ≤ 1

Proof state:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ Module.rank K (Fin 1 → K) = 1

Tactic:
rw [rank_fun', Fintype.card_ofSubsingleton, Nat.cast_one]

Result:
no goals

Proof state:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ (toLin' (vecMulVec w v)).rank ≤ 1

Tactic:
nontriviality K

Result:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ (toLin' (vecMulVec w v)).rank ≤ 1

Proof state:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ (toLin' (col (Fin 1) w)).rank ≤ 1

Tactic:
refine (LinearMap.rank_le_domain _).trans_eq ?_

Result:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ Module.rank K (Fin 1 → K) = 1

Proof state:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ (toLin' (vecMulVec w v)).rank ≤ 1

Tactic:
rw [Matrix.vecMulVec_eq (Fin 1), Matrix.toLin'_mul]

Result:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ (toLin' (col (Fin 1) w) ∘ₗ toLin' (row (Fin 1) v)).rank ≤ 1

Proof state:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ (toLin' (col (Fin 1) w) ∘ₗ toLin' (row (Fin 1) v)).rank ≤ 1

Tactic:
refine le_trans (LinearMap.rank_comp_le_left _ _) ?_

Result:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ (toLin' (col (Fin 1) w)).rank ≤ 1