harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma _root_.MeasureTheory.AEStronglyMeasurable.integral_condKernel
    (hf : AEStronglyMeasurable f ρ) :
    AEStronglyMeasurable (fun x ↦ ∫ y, f (x, y) ∂ρ.condKernel x) ρ.fst

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : AEStronglyMeasurable f ρ
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst

Tactic:
rw [← ρ.disintegrate ρ.condKernel] at hf

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst

Tactic:
exact AEStronglyMeasurable.integral_kernel_compProd hf

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous iff the
family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is equicontinuous. -/
lemma IsUniformInducing.equicontinuous_iff {F : ι → X → α} {u : α → β} (hu : IsUniformInducing u) :
    Equicontinuous F ↔ Equicontinuous ((u ∘ ·) ∘ F)

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
⊢ Equicontinuous F ↔ Equicontinuous ((fun x => u ∘ x) ∘ F)

Tactic:
congrm ∀ x, ?_

Result:
case a
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
x : X
⊢ EquicontinuousAt F x ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x

Proof state:
case a
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
x : X
⊢ EquicontinuousAt F x ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x

Tactic:
rw [hu.equicontinuousAt_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_eq_append_iff {l : Array α} {f : Nat → α → β} {l₁ l₂ : Array β} :
    mapIdx f l = l₁ ++ l₂ ↔
      ∃ (l₁' : Array α) (l₂' : Array α), l = l₁' ++ l₂' ∧
        l₁'.mapIdx f = l₁ ∧
        l₂'.mapIdx (fun i => f (i + l₁'.size)) = l₂

Proof state:
case mk.mk.mk.mpr
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
l₁ l₂ : List β
⊢ (∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧
        mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = { toList := l₂ }) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ List.mapIdx f l₁' = l₁ ∧ List.mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

Tactic:
rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩

Result:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
β : Type u_2
f : Nat → α → β
l₁✝ l₂✝ : List β
l₁ l₂ : List α
h₁ : mapIdx f { toList := l₁ } = { toList := l₁✝ }
h₂ : mapIdx (fun i => f (i + { toList := l₁ }.size)) { toList := l₂ } = { toList := l₂✝ }
⊢ ∃ l₁' l₂',
    { toList := l₁ }.toList ++ { toList := l₂ }.toList = l₁' ++ l₂' ∧
      List.mapIdx f l₁' = l₁✝ ∧ List.mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂✝

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l₂ : Array β
l : List α
l₁ : List β
⊢ mapIdx f { toList := l } = { toList := l₁ } ++ l₂ ↔
    ∃ l₁' l₂',
      { toList := l } = l₁' ++ l₂' ∧ mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = l₂

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
l₁ l₂ : List β
⊢ mapIdx f { toList := l } = { toList := l₁ } ++ { toList := l₂ } ↔
    ∃ l₁' l₂',
      { toList := l } = l₁' ++ l₂' ∧
        mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = { toList := l₂ }
-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem sub (hf : UnifTight f p μ) (hg : UnifTight g p μ)
    (hf_meas : ∀ i, AEStronglyMeasurable (f i) μ) (hg_meas : ∀ i, AEStronglyMeasurable (g i) μ) :
    UnifTight (f - g) p μ

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
⊢ UnifTight (f - g) p μ

Tactic:
rw [sub_eq_add_neg]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
⊢ UnifTight (f + -g) p μ

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
⊢ UnifTight (f + -g) p μ

Tactic:
exact hf.add hg.neg hf_meas fun i => (hg_meas i).neg

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem eq_iff_modEq_nat (n : ℕ) {a b : ℕ} : (a : ZMod n) = b ↔ a ≡ b [MOD n]

Proof state:
case succ
a b n✝ : ℕ
⊢ ↑↑a = ↑↑b ↔ (↑a).val = (↑b).val

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
n a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD n]

Tactic:
cases n

Result:
case zero
a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD 0]

case succ
a b n✝ : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD n✝ + 1]

Proof state:
case zero
a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD 0]

Tactic:
simp [Nat.ModEq, Int.natCast_inj, Nat.mod_zero]

Result:
no goals

Proof state:
case succ
a b n✝ : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD n✝ + 1]

Tactic:
rw [Fin.ext_iff, Nat.ModEq, ← val_natCast, ← val_natCast]

Result:
case succ
a b n✝ : ℕ
⊢ ↑↑a = ↑↑b ↔ (↑a).val = (↑b).val
-- Mathlib/Order/Filter/Pointwise.lean
theorem bot_pow {n : ℕ} (hn : n ≠ 0) : (⊥ : Filter α) ^ n = ⊥

Proof state:
α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ⊥ ^ n = ⊥

Tactic:
rw [← Nat.sub_one_add_one hn, pow_succ', bot_mul]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma zpow_lt_one_iff_right₀ (ha : 1 < a) : a ^ n < 1 ↔ n < 0

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha : 1 < a
⊢ a ^ n < 1 ↔ n < 0

Tactic:
simp [← zpow_lt_zpow_iff_right₀ ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
  Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)

Proof state:
x m n : Nat
lt : x < 2 ^ m
le : m ≤ n
⊢ 0 < 2

Tactic:
trivial

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem numeratorHom_inj (hS : S ≤ nonZeroDivisorsRight R) :
    Function.Injective (numeratorHom : R → R[S⁻¹]) :=
  fun r₁ r₂ h => by
  rw [numeratorHom_apply, numeratorHom_apply, oreDiv_eq_iff] at h
  rcases h with ⟨u, v, h₁, h₂⟩
  simp only [S.coe_one, mul_one, Submonoid.smul_def, smul_eq_mul] at h₁ h₂
  rw [← h₂, ← sub_eq_zero, ← mul_sub] at h₁
  exact (sub_eq_zero.mp (hS u.2 _ h₁)).symm

Proof state:
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsRight R
r₁ r₂ : R
u : ↥S
v : R
h₁ : ↑u * r₂ = v * r₁
h₂ : ↑u = v
⊢ r₁ = r₂

Tactic:
rw [← h₂, ← sub_eq_zero, ← mul_sub] at h₁

Result:
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsRight R
r₁ r₂ : R
u : ↥S
v : R
h₁ : ↑u * (r₂ - r₁) = 0
h₂ : ↑u = v
⊢ r₁ = r₂

Proof state:
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsRight R
r₁ r₂ : R
u : ↥S
v : R
h₁ : u • r₂ = v • r₁
h₂ : ↑u * ↑1 = v * ↑1
⊢ r₁ = r₂

Tactic:
simp only [S.coe_one, mul_one, Submonoid.smul_def, smul_eq_mul] at h₁ h₂

Result:
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsRight R
r₁ r₂ : R
u : ↥S
v : R
h₁ : ↑u * r₂ = v * r₁
h₂ : ↑u = v
⊢ r₁ = r₂

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsRight R
r₁ r₂ : R
h : ∃ u v, u • r₂ = v • r₁ ∧ ↑u * ↑1 = v * ↑1
⊢ r₁ = r₂

Tactic:
rcases h with ⟨u, v, h₁, h₂⟩

Result:
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsRight R
r₁ r₂ : R
u : ↥S
v : R
h₁ : u • r₂ = v • r₁
h₂ : ↑u * ↑1 = v * ↑1
⊢ r₁ = r₂

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsRight R
r₁ r₂ : R
h : numeratorHom r₁ = numeratorHom r₂
⊢ r₁ = r₂

Tactic:
rw [numeratorHom_apply, numeratorHom_apply, oreDiv_eq_iff] at h

Result:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsRight R
r₁ r₂ : R
h : ∃ u v, u • r₂ = v • r₁ ∧ ↑u * ↑1 = v * ↑1
⊢ r₁ = r₂

Proof state:
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsRight R
r₁ r₂ : R
u : ↥S
v : R
h₁ : ↑u * (r₂ - r₁) = 0
h₂ : ↑u = v
⊢ r₁ = r₂

Tactic:
exact (sub_eq_zero.mp (hS u.2 _ h₁)).symm

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem apply_lt_nfpFamily_iff [Nonempty ι] [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} :
    (∀ i, f i b < nfpFamily f a) ↔ b < nfpFamily f a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b < nfpFamily f a
⊢ b < nfpFamily f a

Tactic:
let ⟨l, hl⟩ := lt_nfpFamily_iff.1 (h (Classical.arbitrary ι))

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b < nfpFamily f a
l : List ι
hl : f (Classical.arbitrary ι) b < List.foldr f a l
⊢ b < nfpFamily f a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Tactic:
refine ⟨fun h ↦ ?_, apply_lt_nfpFamily H⟩

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b < nfpFamily f a
⊢ b < nfpFamily f a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b < nfpFamily f a
l : List ι
hl : f (Classical.arbitrary ι) b < List.foldr f a l
⊢ b < nfpFamily f a

Tactic:
exact lt_nfpFamily_iff.2 <| ⟨l, (H _).le_apply.trans_lt hl⟩

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem fib_golden_exp' (n : ℕ) : φ * Nat.fib (n + 1) + Nat.fib n = φ ^ (n + 1)

Proof state:
n : ℕ
⊢ φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)

Tactic:
induction n with
| zero => norm_num
| succ n ih =>
  calc
    _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
      simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub, tsub_zero,
        Nat.cast_add, gold_sq]; ring
    _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
    _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring

Result:
no goals

Proof state:
case zero

⊢ φ * ↑(Nat.fib (0 + 1)) + ↑(Nat.fib 0) = φ ^ (0 + 1)

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * (↑(Nat.fib n) + ↑(Nat.fib n.succ)) + ↑(Nat.fib (n + 1)) = φ * ↑(Nat.fib n) + (φ + 1) * ↑(Nat.fib (n + 1))

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * φ ^ (n + 1) = φ ^ (n + 2)

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * ↑(Nat.fib (n + 1 + 1)) + ↑(Nat.fib (n + 1)) = φ * ↑(Nat.fib n) + φ ^ 2 * ↑(Nat.fib (n + 1))

Tactic:
simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub, tsub_zero,
  Nat.cast_add, gold_sq]

Result:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * (↑(Nat.fib n) + ↑(Nat.fib n.succ)) + ↑(Nat.fib (n + 1)) = φ * ↑(Nat.fib n) + (φ + 1) * ↑(Nat.fib (n + 1))

Proof state:
case succ
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * ↑(Nat.fib (n + 1 + 1)) + ↑(Nat.fib (n + 1)) = φ ^ (n + 1 + 1)

Tactic:
calc
  _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
    simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub, tsub_zero,
      Nat.cast_add, gold_sq]; ring
  _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
  _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring

Result:
no goals

Proof state:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * ↑(Nat.fib n) + φ ^ 2 * ↑(Nat.fib (n + 1)) = φ * (↑(Nat.fib n) + φ * ↑(Nat.fib (n + 1)))

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * (↑(Nat.fib n) + φ * ↑(Nat.fib (n + 1))) = φ ^ (n + 2)

Tactic:
rw [add_comm, ih]

Result:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * φ ^ (n + 1) = φ ^ (n + 2)
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem constantCoeff_wittStructureRat (Φ : MvPolynomial idx ℚ) (h : constantCoeff Φ = 0) (n : ℕ) :
    constantCoeff (wittStructureRat p Φ n) = 0

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
h : constantCoeff Φ = 0
n : ℕ
⊢ constantCoeff (wittStructureRat p Φ n) = 0

Tactic:
simp only [wittStructureRat, eval₂Hom_zero'_apply, h, bind₁, map_aeval, constantCoeff_rename,
  constantCoeff_wittPolynomial, constantCoeff_comp_algebraMap, RingHom.id_apply,
  constantCoeff_xInTermsOfW]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem prodLift_fst_comp_snd_comp (f : α →. γ) (g : β →. δ) :
    prodLift (f.comp ((Prod.fst : α × β → α) : α × β →. α))
        (g.comp ((Prod.snd : α × β → β) : α × β →. β)) =
      prodMap f g :=
  ext fun a => by simp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
a : α × β
⊢ ∀ (b : γ × δ), b ∈ (f.comp ↑Prod.fst).prodLift (g.comp ↑Prod.snd) a ↔ b ∈ f.prodMap g a

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem reachable_deleteEdges_iff_exists_cycle.aux [DecidableEq V] {u v w : V}
    (hb : ∀ p : G.Walk v w, s(v, w) ∈ p.edges) (c : G.Walk u u) (hc : c.IsTrail)
    (he : s(v, w) ∈ c.edges)
    (hw : w ∈ (c.takeUntil v (c.fst_mem_support_of_mem_edges he)).support) : False

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.reverse.edges
⊢ False

Tactic:
rw [Walk.edges_reverse, List.mem_reverse] at hpq'

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False
-- Mathlib/Data/Matroid/Loop.lean
lemma isBasis_iff_empty_of_subset_loops (hX : X ⊆ M.loops) : M.IsBasis I X ↔ I = ∅

Proof state:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
this : M.IsBasis I M.loops
⊢ I = ∅

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis I X ↔ I = ∅

Tactic:
refine ⟨fun h ↦ ?_, by rintro rfl; simpa⟩

Result:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
⊢ I = ∅

Proof state:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
⊢ I = ∅ → M.IsBasis I X

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis ∅ X

Proof state:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
⊢ I = ∅

Tactic:
have := (closure_eq_loops_of_subset hX) ▸ h.isBasis_closure_right

Result:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
this : M.IsBasis I M.loops
⊢ I = ∅

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis ∅ X

Tactic:
simpa

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma nonsingular_iff' (x y : R) : W'.Nonsingular x y ↔ W'.Equation x y ∧
    (W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄) ≠ 0 ∨ 2 * y + W'.a₁ * x + W'.a₃ ≠ 0)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Nonsingular x y ↔
    W'.Equation x y ∧ (W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄) ≠ 0 ∨ 2 * y + W'.a₁ * x + W'.a₃ ≠ 0)

Tactic:
rw [Nonsingular, equation_iff', evalEval_polynomialX, evalEval_polynomialY]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem range_lt_top_of_det_eq_zero {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M}
    (hf : LinearMap.det f = 0) : LinearMap.range f < ⊤

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : IsUnit f
⊢ ¬LinearMap.det f = 0

Tactic:
exact isUnit_iff_ne_zero.1 (f.isUnit_det hf)

Result:
no goals

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f = 0
⊢ FiniteDimensional 𝕜 M

Tactic:
simp [f.finiteDimensional_of_det_ne_one, hf]

Result:
no goals

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f = 0
this : FiniteDimensional 𝕜 M
⊢ range f < ⊤

Tactic:
contrapose hf

Result:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : ¬range f < ⊤
⊢ ¬LinearMap.det f = 0

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f = 0
⊢ range f < ⊤

Tactic:
have : FiniteDimensional 𝕜 M := by simp [f.finiteDimensional_of_det_ne_one, hf]

Result:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f = 0
this : FiniteDimensional 𝕜 M
⊢ range f < ⊤

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : ¬range f < ⊤
⊢ ¬LinearMap.det f = 0

Tactic:
simp only [lt_top_iff_ne_top, Classical.not_not, ← isUnit_iff_range_eq_top] at hf

Result:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : IsUnit f
⊢ ¬LinearMap.det f = 0
-- Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean
lemma isIntegrallyClosed_of_isLocalization [IsIntegrallyClosed R] [IsDomain R] (M : Submonoid R)
    (hM : M ≤ R⁰) [IsLocalization M S] : IsIntegrallyClosed S

Proof state:
case intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ((algebraMap R K).comp (RingHom.id R)) z = ((algebraMap R K).comp (RingHom.id R)) ↑⟨y, y_mem⟩ * x

Tactic:
rw [RingHom.comp_id, hz, ← Algebra.smul_def, Submonoid.mk_smul]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
⊢ IsIntegrallyClosed S

Tactic:
letI := g.toAlgebra

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ IsIntegrallyClosed S

Proof state:
case intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ∃ y, (algebraMap S K) y = x

Tactic:
refine ⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩

Result:
case intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ((algebraMap R K).comp (RingHom.id R)) z = ((algebraMap R K).comp (RingHom.id R)) ↑⟨y, y_mem⟩ * x
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem coe_toNNReal_ae_eq {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x < ∞) :
    (fun x => ((f x).toNNReal : ℝ≥0∞)) =ᵐ[μ] f

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
x : α
hx : f x < ⊤
⊢ ↑(f x).toNNReal = f x

Tactic:
simp only [hx.ne, Ne, not_false_iff, coe_toNNReal]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ (fun x => ↑(f x).toNNReal) =ᶠ[ae μ] f

Tactic:
filter_upwards [hf]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ ∀ (a : α), f a < ⊤ → ↑(f a).toNNReal = f a

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ ∀ (a : α), f a < ⊤ → ↑(f a).toNNReal = f a

Tactic:
intro x hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
x : α
hx : f x < ⊤
⊢ ↑(f x).toNNReal = f x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatten_singleton (l : Vector α n) : #v[l].flatten = l.cast (by simp)

Proof state:
α : Type ?u.290436
n : Nat
l : Vector α n
⊢ n = 1 * n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
⊢ { toArray := #[l], size_toArray := ⋯ }.flatten = Vector.cast ⋯ l

Tactic:
simp [flatten]

Result:
no goals