harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_one (h : i < w) : (1#w)[i] = decide (i = 0)

Proof state:
i w : Nat
h : i < w
⊢ 0 < w

Tactic:
omega

Result:
no goals

Proof state:
i w : Nat
h : i < w
⊢ (1#w)[i] = decide (i = 0)

Tactic:
simp [← getLsbD_eq_getElem, getLsbD_one, h, show 0 < w by omega]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma div_eq_iff_eq_of_dvd_dvd (hn : n ≠ 0) (ha : a ∣ n) (hb : b ∣ n) : n / a = n / b ↔ a = b

Proof state:
case mp
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : n / a = n / b
⊢ n * a = n * b

Tactic:
apply Nat.eq_mul_of_div_eq_left (Nat.dvd_trans hb (Nat.dvd_mul_right _ _))

Result:
case mp
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : n / a = n / b
⊢ n * a / b = n

Proof state:
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
⊢ n / a = n / b ↔ a = b

Tactic:
constructor <;> intro h

Result:
case mp
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : n / a = n / b
⊢ a = b

case mpr
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : a = b
⊢ n / a = n / b

Proof state:
case mpr
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : a = b
⊢ n / a = n / b

Tactic:
rw [h]

Result:
no goals

Proof state:
case mp
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : n / a = n / b
⊢ n * a / b = n

Tactic:
rw [eq_comm, Nat.mul_comm, Nat.mul_div_assoc _ hb]

Result:
case mp
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : n / a = n / b
⊢ n = a * (n / b)

Proof state:
case mp
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : n / a = n / b
⊢ a = b

Tactic:
rw [← Nat.mul_right_inj hn]

Result:
case mp
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : n / a = n / b
⊢ n * a = n * b

Proof state:
case mp
a b n : ℕ
hn : n ≠ 0
ha : a ∣ n
hb : b ∣ n
h : n / a = n / b
⊢ n = a * (n / b)

Tactic:
exact Nat.eq_mul_of_div_eq_right ha h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem toGraph_compl_eq [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) :
    h.compl.toGraph = h.toGraphᶜ

Proof state:
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
⊢ ⋯.toGraph = h.toGraphᶜ

Tactic:
ext v w

Result:
case Adj.h.h.a
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
v w : V
⊢ ⋯.toGraph.Adj v w ↔ h.toGraphᶜ.Adj v w

Proof state:
case Adj.h.h.a
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
v w : V
⊢ ⋯.toGraph.Adj v w ↔ h.toGraphᶜ.Adj v w

Tactic:
rcases h.zero_or_one v w with h | h <;> by_cases hvw : v = w <;> simp [Matrix.compl, h, hvw]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Norm.lean
theorem isPowMul {A : Type*} [Ring A] (f : MulRingNorm A) : IsPowMul f := fun x n hn => by
  cases n
  · omega
  · rw [map_pow]

Proof state:
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n : ℕ
hn : 1 ≤ n
⊢ f (x ^ n) = f x ^ n

Tactic:
cases n

Result:
case zero
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
hn : 1 ≤ 0
⊢ f (x ^ 0) = f x ^ 0

case succ
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n✝ : ℕ
hn : 1 ≤ n✝ + 1
⊢ f (x ^ (n✝ + 1)) = f x ^ (n✝ + 1)

Proof state:
case succ
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n✝ : ℕ
hn : 1 ≤ n✝ + 1
⊢ f (x ^ (n✝ + 1)) = f x ^ (n✝ + 1)

Tactic:
rw [map_pow]

Result:
no goals

Proof state:
case zero
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
hn : 1 ≤ 0
⊢ f (x ^ 0) = f x ^ 0

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter {f : α → ℝ} {t : Set α}
    (hf : IntegrableOn f t μ)
    (hf_zero : ∀ s, MeasurableSet s → μ (s ∩ t) < ∞ → 0 ≤ ∫ x in s ∩ t, f x ∂μ) :
    0 ≤ᵐ[μ.restrict t] f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f

Tactic:
refine ae_nonneg_of_forall_setIntegral_nonneg hf fun s hs h's => ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : (μ.restrict t) s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ.restrict t

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : (μ.restrict t) s < ⊤
⊢ μ (s ∩ t) < ⊤

Tactic:
rwa [Measure.restrict_apply hs] at h's

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : (μ.restrict t) s < ⊤
⊢ 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ

Tactic:
apply hf_zero s hs

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : (μ.restrict t) s < ⊤
⊢ μ (s ∩ t) < ⊤

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : (μ.restrict t) s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ.restrict t

Tactic:
simp_rw [Measure.restrict_restrict hs]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : (μ.restrict t) s < ⊤
⊢ 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem mul_eq_one_of_mul_eq_one [FiniteDimensional K V] {f g : V →ₗ[K] V} (hfg : f * g = 1) :
    g * f = 1

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
ginj : Injective ⇑g
i : V →ₗ[K] V
hi : g ∘ₗ i = id
⊢ g * f = 1

Tactic:
have : f * (g * i) = f * 1 := congr_arg _ hi

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
ginj : Injective ⇑g
i : V →ₗ[K] V
hi : g ∘ₗ i = id
this : f * (g * i) = f * 1
⊢ g * f = 1

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
ginj : Injective ⇑g
i : V →ₗ[K] V
hi : g ∘ₗ i = id
this : i = f
⊢ g * f = 1

Tactic:
rwa [← this]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
ginj : Injective ⇑g
i : V →ₗ[K] V
hi : g ∘ₗ i = id
this : f * (g * i) = f * 1
⊢ g * f = 1

Tactic:
rw [← mul_assoc, hfg, one_mul, mul_one] at this

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
ginj : Injective ⇑g
i : V →ₗ[K] V
hi : g ∘ₗ i = id
this : i = f
⊢ g * f = 1

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
x : V
⊢ (f * g) x = 1 x

Tactic:
rw [hfg]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
ginj : Injective ⇑g
⊢ g * f = 1

Tactic:
let ⟨i, hi⟩ := g.exists_rightInverse_of_surjective
  (range_eq_top.2 (injective_iff_surjective.1 ginj))

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
ginj : Injective ⇑g
i : V →ₗ[K] V
hi : g ∘ₗ i = id
⊢ g * f = 1

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
⊢ g * f = 1

Tactic:
have ginj : Injective g :=
  HasLeftInverse.injective ⟨f, fun x => show (f * g) x = (1 : V →ₗ[K] V) x by rw [hfg]⟩

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
ginj : Injective ⇑g
⊢ g * f = 1
-- Mathlib/Data/Nat/Lattice.lean
theorem sInf_upward_closed_eq_succ_iff {s : Set ℕ} (hs : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s)
    (k : ℕ) : sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Proof state:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
constructor

Result:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s

case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1

Proof state:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k

Tactic:
exact ⟨le_rfl, k.not_succ_le_self⟩

Result:
no goals

Proof state:
case mpr.intro
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ sInf s = k + 1

Tactic:
rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]

Result:
case mpr.intro
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ k + 1 ∈ s ∧ ∀ n < k + 1, n ∉ s

Proof state:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ∈ s ∧ k ∉ s

Tactic:
rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]

Result:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k

s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = ?m.5765 + 1

Proof state:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = k + 1

Tactic:
assumption

Result:
no goals

Proof state:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s

Tactic:
intro H

Result:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ∈ s ∧ k ∉ s

Proof state:
case mpr.intro
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ k + 1 ∈ s ∧ ∀ n < k + 1, n ∉ s

Tactic:
exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩

Result:
no goals

Proof state:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

Tactic:
exact k

Result:
no goals

Proof state:
case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1

Tactic:
rintro ⟨H, H'⟩

Result:
case mpr.intro
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ sInf s = k + 1
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- The upper shadow of a family of `r`-sets is a family of `r + 1`-sets. -/
protected lemma _root_.Set.Sized.upShadow (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
    (∂⁺ 𝒜 : Set (Finset α)).Sized (r + 1)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r + 1) ↑(∂⁺ 𝒜)

Tactic:
intro A h

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
h : A ∈ ↑(∂⁺ 𝒜)
⊢ #A = r + 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
h : A ∈ ↑(∂⁺ 𝒜)
⊢ #A = r + 1

Tactic:
obtain ⟨A, hA, i, hi, rfl⟩ := mem_upShadow_iff.1 h

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∉ A
h : insert i A ∈ ↑(∂⁺ 𝒜)
⊢ #(insert i A) = r + 1

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∉ A
h : insert i A ∈ ↑(∂⁺ 𝒜)
⊢ #(insert i A) = r + 1

Tactic:
rw [card_insert_of_not_mem hi, h𝒜 hA]

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Wequiv.symm (x y : q.P.W) : Wequiv x y → Wequiv y x

Proof state:
case trans
F : Type u → Type u
q : QPF F
x✝ y✝ x y z : (P F).W
a✝¹ : Wequiv x y
a✝ : Wequiv y z
ih₁ : Wequiv y x
ih₂ : Wequiv z y
⊢ Wequiv z x

Tactic:
exact QPF.Wequiv.trans _ _ _ ih₂ ih₁

Result:
no goals

Proof state:
case abs
F : Type u → Type u
q : QPF F
x y : (P F).W
a : (P F).A
f : (P F).B a → (P F).W
a' : (P F).A
f' : (P F).B a' → (P F).W
h : QPF.abs ⟨a, f⟩ = QPF.abs ⟨a', f'⟩
⊢ Wequiv (WType.mk a' f') (WType.mk a f)

Tactic:
exact Wequiv.abs _ _ _ _ h.symm

Result:
no goals

Proof state:
case ind
F : Type u → Type u
q : QPF F
x y : (P F).W
a : (P F).A
f f' : (P F).B a → (P F).W
a✝ : ∀ (x : (P F).B a), Wequiv (f x) (f' x)
ih : ∀ (x : (P F).B a), Wequiv (f' x) (f x)
⊢ Wequiv (WType.mk a f') (WType.mk a f)

Tactic:
exact Wequiv.ind _ _ _ ih

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
x y : (P F).W
⊢ Wequiv x y → Wequiv y x

Tactic:
intro h

Result:
F : Type u → Type u
q : QPF F
x y : (P F).W
h : Wequiv x y
⊢ Wequiv y x

Proof state:
F : Type u → Type u
q : QPF F
x y : (P F).W
h : Wequiv x y
⊢ Wequiv y x

Tactic:
induction h with
| ind a f f' _ ih => exact Wequiv.ind _ _ _ ih
| abs a f a' f' h => exact Wequiv.abs _ _ _ _ h.symm
| trans x y z _ _ ih₁ ih₂ => exact QPF.Wequiv.trans _ _ _ ih₂ ih₁

Result:
no goals
-- Mathlib/LinearAlgebra/Charpoly/BaseChange.lean
lemma LinearMap.det_eq_sign_charpoly_coeff {R M} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :
    LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
a✝ : Nontrivial R
⊢ LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0

Tactic:
rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff,
  ← Module.finrank_eq_card_chooseBasisIndex, charpoly_def]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0

Tactic:
nontriviality R

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
a✝ : Nontrivial R
⊢ LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem find?_toArray (p : α → Bool) (v : Vector α n) :
    v.toArray.find? p = v.find? p

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.find? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type
n : Nat
p : α → Bool
v : Vector α n
⊢ Array.find? p v.toArray = find? p v

Tactic:
cases v

Result:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.find? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem iSup_lintegral_le {ι : Sort*} (f : ι → α → ℝ≥0∞) :
    ⨆ i, ∫⁻ a, f i a ∂μ ≤ ∫⁻ a, ⨆ i, f i a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
f : ι → α → ℝ≥0∞
⊢ ⨆ i, ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), (⨆ i, f i) a ∂μ

Tactic:
exact (monotone_lintegral μ).le_map_iSup

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
f : ι → α → ℝ≥0∞
⊢ ⨆ i, ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), ⨆ i, f i a ∂μ

Tactic:
simp only [← iSup_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
f : ι → α → ℝ≥0∞
⊢ ⨆ i, ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), (⨆ i, f i) a ∂μ
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem of'_dvd_iff_modOf_eq_zero {x : k[G]} {g : G} :
    of' k G g ∣ x ↔ x %ᵒᶠ g = 0

Proof state:
case mp.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
⊢ of' k G g * x %ᵒᶠ g = 0

Tactic:
rw [of'_mul_modOf]

Result:
no goals

Proof state:
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x

Tactic:
intro h

Result:
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ x

Proof state:
case mp
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
⊢ of' k G g ∣ x → x %ᵒᶠ g = 0

Tactic:
rintro ⟨x, rfl⟩

Result:
case mp.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
⊢ of' k G g * x %ᵒᶠ g = 0

Proof state:
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ x

Tactic:
rw [← divOf_add_modOf x g, h, add_zero]

Result:
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
⊢ of' k G g ∣ x ↔ x %ᵒᶠ g = 0

Tactic:
constructor

Result:
case mp
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
⊢ of' k G g ∣ x → x %ᵒᶠ g = 0

case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x

Proof state:
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)

Tactic:
exact dvd_mul_right _ _

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vadd_left_mem_affineSpan_pair {p₁ p₂ : P} {v : V} :
    v +ᵥ p₁ ∈ line[k, p₁, p₂] ↔ ∃ r : k, r • (p₂ -ᵥ p₁) = v

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
v : V
⊢ v +ᵥ p₁ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v

Tactic:
rw [vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan,
  mem_vectorSpan_pair_rev]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem preAleph_isNormal : IsNormal (ord ∘ preAleph)

Proof state:
⊢ IsNormal (ord ∘ ⇑preAleph)

Tactic:
convert isNormal_preOmega

Result:
case h.e'_1

⊢ ord ∘ ⇑preAleph = ⇑preOmega

Proof state:
case h.e'_1

⊢ ord ∘ ⇑preAleph = ⇑preOmega

Tactic:
exact funext ord_preAleph

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsBigO.of_pow {f : α → 𝕜} {g : α → R} {n : ℕ} (hn : n ≠ 0) (h : (f ^ n) =O[l] (g ^ n)) :
    f =O[l] g

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
⊢ f =O[l] g

Tactic:
rcases h.exists_pos with ⟨C, _hC₀, hC⟩

Result:
case intro.intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
⊢ f =O[l] g

Proof state:
case intro.intro.intro.intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
c : ℝ
hc₀ : 0 ≤ c
hc : C ≤ c ^ n
⊢ f =O[l] g

Tactic:
exact (hC.of_pow hn hc hc₀).isBigO

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
⊢ f =O[l] g

Tactic:
obtain ⟨c : ℝ, hc₀ : 0 ≤ c, hc : C ≤ c ^ n⟩ :=
  ((eventually_ge_atTop _).and <| (tendsto_pow_atTop hn).eventually_ge_atTop C).exists

Result:
case intro.intro.intro.intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
c : ℝ
hc₀ : 0 ≤ c
hc : C ≤ c ^ n
⊢ f =O[l] g
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_le_zpow_of_nonpos₀ (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hn : n ≤ 0) : 1 ≤ a ^ n

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

Tactic:
simpa using zpow_right_anti₀ ha₀ ha₁ hn

Result:
no goals
-- Mathlib/RingTheory/RingHom/FinitePresentation.lean
theorem finitePresentation_localizationPreserves : LocalizationPreserves @FinitePresentation

Proof state:
case mk.intro.intro.intro
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
this✝² : Algebra R S := f.toAlgebra
this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝ : Algebra R' S' := f'.toAlgebra
this : IsScalarTower R R' S'
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
hgsurj : Function.Surjective ⇑g
hgker : (ker g.toRingHom).FG
⊢ (IsLocalization.map S' f ⋯).FinitePresentation

Tactic:
let MX : Submonoid (MvPolynomial (Fin n) R) :=
  Algebra.algebraMapSubmonoid (MvPolynomial (Fin n) R) M

Result:
case mk.intro.intro.intro
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
this✝² : Algebra R S := f.toAlgebra
this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝ : Algebra R' S' := f'.toAlgebra
this : IsScalarTower R R' S'
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
hgsurj : Function.Surjective ⇑g
hgker : (ker g.toRingHom).FG
MX : Submonoid (MvPolynomial (Fin n) R) := Algebra.algebraMapSubmonoid (MvPolynomial (Fin n) R) M
⊢ (IsLocalization.map S' f ⋯).FinitePresentation