harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_replicate_of_isSome {f : α → Option β} (h : (f a).isSome) :
    (replicate n a).filterMap f = replicate n (Option.get _ h)

Proof state:
α : Type u_1
β : Type u_2
a : α
n : Nat
f : α → Option β
h✝ : (f a).isSome = true
h : ∃ a_1, f a = some a_1
⊢ filterMap f (replicate n a) = replicate n ((f a).get h✝)

Tactic:
obtain ⟨b, h⟩ := h

Result:
case intro
α : Type u_1
β : Type u_2
a : α
n : Nat
f : α → Option β
h✝ : (f a).isSome = true
b : β
h : f a = some b
⊢ filterMap f (replicate n a) = replicate n ((f a).get h✝)

Proof state:
α : Type u_1
β : Type u_2
a : α
n : Nat
f : α → Option β
h : (f a).isSome = true
⊢ filterMap f (replicate n a) = replicate n ((f a).get h)

Tactic:
rw [Option.isSome_iff_exists] at h

Result:
α : Type u_1
β : Type u_2
a : α
n : Nat
f : α → Option β
h✝ : (f a).isSome = true
h : ∃ a_1, f a = some a_1
⊢ filterMap f (replicate n a) = replicate n ((f a).get h✝)

Proof state:
case intro
α : Type u_1
β : Type u_2
a : α
n : Nat
f : α → Option β
h✝ : (f a).isSome = true
b : β
h : f a = some b
⊢ filterMap f (replicate n a) = replicate n ((f a).get h✝)

Tactic:
simp [filterMap_replicate, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_sub_self_right (a b : Nat) : (a + b) - b = a

Proof state:
a b : Nat
⊢ b + a - b = a

Tactic:
apply add_sub_self_left

Result:
no goals

Proof state:
a b : Nat
⊢ a + b - b = a

Tactic:
rw [Nat.add_comm]

Result:
a b : Nat
⊢ b + a - b = a
-- Mathlib/Algebra/Central/Basic.lean
lemma baseField_essentially_unique
    (k K D : Type*) [Field k] [Field K] [Ring D] [Nontrivial D]
    [Algebra k K] [Algebra K D] [Algebra k D] [IsScalarTower k K D]
    [IsCentral k D] :
    Function.Bijective (algebraMap k K)

Proof state:
k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
x : D
⊢ ∀ (x_1 : k), (algebraMap k D) x_1 = x → ∃ y, (algebraMap K D) y = x

Tactic:
rintro x rfl

Result:
k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
x : k
⊢ ∃ y, (algebraMap K D) y = (algebraMap k D) x
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem fg_iSup {ι : Sort*} [Finite ι] (N : ι → Submodule R M) (h : ∀ i, (N i).FG) :
    (iSup N).FG

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_3
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), (N i).FG
⊢ (iSup N).FG

Tactic:
cases nonempty_fintype (PLift ι)

Result:
case intro
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_3
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), (N i).FG
val✝ : Fintype (PLift ι)
⊢ (iSup N).FG

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_3
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), (N i).FG
val✝ : Fintype (PLift ι)
⊢ (iSup N).FG

Tactic:
simpa [iSup_plift_down] using fg_biSup Finset.univ (N ∘ PLift.down) fun i _ => h i.down

Result:
no goals
-- Mathlib/LinearAlgebra/Pi.lean
theorem update_apply (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i j : ι) (b : M₂ →ₗ[R] φ i) :
    (update f i b j) c = update (fun i => f i c) i (b c) j

Proof state:
case pos
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ (update f i b j) c = update (fun i => (f i) c) i (b c) j

Tactic:
rw [h, update_self, update_self]

Result:
no goals

Proof state:
case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (update f i b j) c = update (fun i => (f i) c) i (b c) j

Tactic:
rw [update_of_ne h, update_of_ne h]

Result:
no goals

Proof state:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
⊢ (update f i b j) c = update (fun i => (f i) c) i (b c) j

Tactic:
by_cases h : j = i

Result:
case pos
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ (update f i b j) c = update (fun i => (f i) c) i (b c) j

case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (update f i b j) c = update (fun i => (f i) c) i (b c) j
-- Mathlib/MeasureTheory/Integral/Prod.lean
/-- A version of *Fubini theorem* for continuous functions with compact support: one may swap
the order of integration with respect to locally finite measures. One does not assume that the
measures are σ-finite, contrary to the usual Fubini theorem. -/
lemma integral_integral_swap_of_hasCompactSupport
    {f : X → Y → E} (hf : Continuous f.uncurry) (h'f : HasCompactSupport f.uncurry)
    {μ : Measure X} {ν : Measure Y} [IsFiniteMeasureOnCompacts μ] [IsFiniteMeasureOnCompacts ν] :
    ∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ y, (∫ x, f x y ∂μ) ∂ν

Proof state:
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ⊤)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ⊤)
⊢ ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν

Tactic:
calc
∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ x, (∫ y in V, f x y ∂ν) ∂μ := by
  congr 1 with x
  apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
  contrapose! hy
  have : (x, y) ∈ Function.support f.uncurry := hy
  exact mem_image_of_mem _ (subset_tsupport _ this)
_ = ∫ x in U, (∫ y in V, f x y ∂ν) ∂μ := by
  apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
  have : ∀ y, f x y = 0 := by
    intro y
    contrapose! hx
    have : (x, y) ∈ Function.support f.uncurry := hx
    exact mem_image_of_mem _ (subset_tsupport _ this)
  simp [this]
_ = ∫ y in V, (∫ x in U, f x y ∂μ) ∂ν := by
  apply integral_integral_swap
  apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
  refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
  obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
  exact hasFiniteIntegral_of_bounded (C := C) (Eventually.of_forall hC)
_ = ∫ y, (∫ x in U, f x y ∂μ) ∂ν := by
  apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
  have : ∀ x, f x y = 0 := by
    intro x
    contrapose! hy
    have : (x, y) ∈ Function.support f.uncurry := hy
    exact mem_image_of_mem _ (subset_tsupport _ this)
  simp [this]
_ = ∫ y, (∫ x, f x y ∂μ) ∂ν := by
  congr 1 with y
  apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
  contrapose! hx
  have : (x, y) ∈ Function.support f.uncurry := hx
  exact mem_image_of_mem _ (subset_tsupport _ this)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_range_inl {α : Type u} {β : Type v} : #(range (@Sum.inl α β)) = lift.{v} #α

Proof state:
α : Type u
β : Type v
⊢ #↑(range Sum.inl) = lift.{v, u} #α

Tactic:
rw [← lift_id'.{u, v} #_, (Equiv.Set.rangeInl α β).lift_cardinal_eq, lift_umax.{u, v}]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblY_of_Z_eq_zero {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.dblY P = (P x ^ 2) ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblY P = (P x ^ 2) ^ 3

Tactic:
rw [dblY, negY_eq, negDblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ - -(P x ^ 2) ^ 3 - W'.a₁ * W'.dblX P * 0 - W'.a₃ * 0 ^ 3 = (P x ^ 2) ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ - -(P x ^ 2) ^ 3 - W'.a₁ * W'.dblX P * 0 - W'.a₃ * 0 ^ 3 = (P x ^ 2) ^ 3

Tactic:
ring1

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_eq_one_of_infinite {f : α → M} {s : Set α} (hs : (s ∩ mulSupport f).Infinite) :
    ∏ᶠ i ∈ s, f i = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1

Tactic:
rw [finprod_mem_def]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ ∏ᶠ (a : α), s.mulIndicator f a = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ ∏ᶠ (a : α), s.mulIndicator f a = 1

Tactic:
apply finprod_of_infinite_mulSupport

Result:
case hf
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ (mulSupport (s.mulIndicator f)).Infinite

Proof state:
case hf
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ (mulSupport (s.mulIndicator f)).Infinite

Tactic:
rwa [← mulSupport_mulIndicator] at hs

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem trans_single_of_eq_none {b : β} (c : γ) {f : δ ≃. β} (h : f.symm b = none) :
    f.trans (single b c) = ⊥

Proof state:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝ : δ
a✝ : γ
h : ∀ (a : δ), ¬f a = some b
⊢ (a✝ ∈ (f x✝).bind fun x => if x = b then some c else none) ↔ a✝ ∈ none

Tactic:
simp only [mem_def, bind_eq_some, iff_false, not_exists, not_and, reduceCtorEq]

Result:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝ : δ
a✝ : γ
h : ∀ (a : δ), ¬f a = some b
⊢ ∀ (x : β), f x✝ = some x → ¬(if x = b then some c else none) = some a✝

Proof state:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝ : δ
a✝ : γ
h : ∀ (a : δ), ¬f a = some b
⊢ ∀ (x : β), f x✝ = some x → ¬(if x = b then some c else none) = some a✝

Tactic:
intros

Result:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝¹ : δ
a✝¹ : γ
h : ∀ (a : δ), ¬f a = some b
x✝ : β
a✝ : f x✝¹ = some x✝
⊢ ¬(if x✝ = b then some c else none) = some a✝¹

Proof state:
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : f.symm b = none
⊢ f.trans (single b c) = ⊥

Tactic:
ext

Result:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : f.symm b = none
x✝ : δ
a✝ : γ
⊢ a✝ ∈ (f.trans (single b c)) x✝ ↔ a✝ ∈ ⊥ x✝

Proof state:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : f.symm b = none
x✝ : δ
a✝ : γ
⊢ a✝ ∈ (f.trans (single b c)) x✝ ↔ a✝ ∈ ⊥ x✝

Tactic:
simp only [eq_none_iff_forall_not_mem, Option.mem_def, f.eq_some_iff] at h

Result:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝ : δ
a✝ : γ
h : ∀ (a : δ), ¬f a = some b
⊢ a✝ ∈ (f.trans (single b c)) x✝ ↔ a✝ ∈ ⊥ x✝

Proof state:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝¹ : δ
a✝¹ : γ
h : ∀ (a : δ), ¬f a = some b
x✝ : β
a✝ : f x✝¹ = some x✝
⊢ ¬(if x✝ = b then some c else none) = some a✝¹

Tactic:
split_ifs <;> simp_all

Result:
no goals

Proof state:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝ : δ
a✝ : γ
h : ∀ (a : δ), ¬f a = some b
⊢ a✝ ∈ (f.trans (single b c)) x✝ ↔ a✝ ∈ ⊥ x✝

Tactic:
dsimp [PEquiv.trans, single]

Result:
case h.a
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝ : δ
a✝ : γ
h : ∀ (a : δ), ¬f a = some b
⊢ (a✝ ∈ (f x✝).bind fun x => if x = b then some c else none) ↔ a✝ ∈ none
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem prod_primeFactors_dvd (n : ℕ) : ∏ p ∈ n.primeFactors, p ∣ n

Proof state:
case pos
n : ℕ
hn : n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
subst hn

Result:
case pos

⊢ ∏ p ∈ primeFactors 0, p ∣ 0

Proof state:
n : ℕ
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
by_cases hn : n = 0

Result:
case pos
n : ℕ
hn : n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Proof state:
case pos

⊢ ∏ p ∈ primeFactors 0, p ∣ 0

Tactic:
simp

Result:
no goals

Proof state:
case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
simpa [prod_primeFactorsList hn] using (n.primeFactorsList : Multiset ℕ).toFinset_prod_dvd_prod

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem setLIntegral_const {f : β → ℝ≥0∞} {μ : Measure β} {a : α} {s : Set β} :
    ∫⁻ x in s, f x ∂const α μ a = ∫⁻ x in s, f x ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
μ : Measure β
a : α
s : Set β
⊢ ∫⁻ (x : β) in s, f x ∂(const α μ) a = ∫⁻ (x : β) in s, f x ∂μ

Tactic:
rw [const_apply]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem apply_le_nfpBFamily (ho : o ≠ 0) (H : ∀ i hi, IsNormal (f i hi)) {a b} :
    (∀ i hi, f i hi b ≤ nfpBFamily.{u, v} o f a) ↔ b ≤ nfpBFamily.{u, v} o f a

Proof state:
case refine_1
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ o.nfpBFamily f a
ho' : 0 < o
⊢ b ≤ o.nfpBFamily f a

Tactic:
exact (H 0 ho').le_apply.trans (h 0 ho')

Result:
no goals

Proof state:
case refine_1
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ o.nfpBFamily f a
⊢ b ≤ o.nfpBFamily f a

Tactic:
have ho' : 0 < o := Ordinal.pos_iff_ne_zero.2 ho

Result:
case refine_1
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ o.nfpBFamily f a
ho' : 0 < o
⊢ b ≤ o.nfpBFamily f a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ o.nfpBFamily f a) ↔ b ≤ o.nfpBFamily f a

Tactic:
refine ⟨fun h => ?_, fun h i hi => ?_⟩

Result:
case refine_1
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ o.nfpBFamily f a
⊢ b ≤ o.nfpBFamily f a

case refine_2
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : b ≤ o.nfpBFamily f a
i : Ordinal.{u}
hi : i < o
⊢ f i hi b ≤ o.nfpBFamily f a

Proof state:
case refine_2
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : b ≤ o.nfpBFamily f a
i : Ordinal.{u}
hi : i < o
⊢ f i hi b ≤ o.nfpBFamily f a

Tactic:
rw [← nfpBFamily_fp (H i hi)]

Result:
case refine_2
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : b ≤ o.nfpBFamily f a
i : Ordinal.{u}
hi : i < o
⊢ f i hi b ≤ f i hi (o.nfpBFamily f a)

Proof state:
case refine_2
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : b ≤ o.nfpBFamily f a
i : Ordinal.{u}
hi : i < o
⊢ f i hi b ≤ f i hi (o.nfpBFamily f a)

Tactic:
exact (H i hi).monotone h

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sum_eq_iff_sum_smul_moebius_eq_on' [AddCommGroup R] {f g : ℕ → R}
    (s : Set ℕ) (hs : ∀ m n, m ∣ n → n ∈ s → m ∈ s) (hs₀ : 0 ∉ s) :
    (∀ n ∈ s, (∑ i ∈ n.divisors, f i) = g n) ↔
     ∀ n ∈ s, (∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd) = f n

Proof state:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
P : ℕ → Prop
n : ℕ
h : n > 0 → n ∈ s → P n
hn : n ∈ s
hs₀ : n ≤ 0
⊢ 0 ∈ s

Tactic:
simpa [nonpos_iff_eq_zero.mp hs₀] using hn

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
⊢ (∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
have : ∀ P : ℕ → Prop, ((∀ n ∈ s, P n) ↔ (∀ n > 0, n ∈ s → P n)) := fun P ↦ by
  refine forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)
  contrapose! hs₀
  simpa [nonpos_iff_eq_zero.mp hs₀] using hn

Result:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
this : ∀ (P : ℕ → Prop), (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n
⊢ (∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Proof state:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
this : ∀ (P : ℕ → Prop), (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n
⊢ (∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
simpa only [this] using sum_eq_iff_sum_smul_moebius_eq_on s hs

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
P : ℕ → Prop
n : ℕ
h : n > 0 → n ∈ s → P n
hn : n ∈ s
⊢ n > 0

Tactic:
contrapose! hs₀

Result:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
P : ℕ → Prop
n : ℕ
h : n > 0 → n ∈ s → P n
hn : n ∈ s
hs₀ : n ≤ 0
⊢ 0 ∈ s

Proof state:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
P : ℕ → Prop
⊢ (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n

Tactic:
refine forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)

Result:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
P : ℕ → Prop
n : ℕ
h : n > 0 → n ∈ s → P n
hn : n ∈ s
⊢ n > 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem one_and_eq_mod_two (n : Nat) : 1 &&& n = n % 2

Proof state:
n : Nat
n0 : n = 0
⊢ 1 &&& n = n % 2

Tactic:
subst n0

Result:
⊢ 1 &&& 0 = 0 % 2

Proof state:
⊢ 1 &&& 0 = 0 % 2

Tactic:
decide

Result:
no goals

Proof state:
n : Nat
n0 : ¬n = 0
⊢ bitwise and 1 n = n % 2

Tactic:
cases mod_two_eq_zero_or_one n with | _ h => simp [bitwise, n0, h]

Result:
no goals

Proof state:
n : Nat
n0 : ¬n = 0
⊢ 1 &&& n = n % 2

Tactic:
simp only [HAnd.hAnd, AndOp.and, land]

Result:
n : Nat
n0 : ¬n = 0
⊢ bitwise and 1 n = n % 2

Proof state:
n : Nat
⊢ 1 &&& n = n % 2

Tactic:
if n0 : n = 0 then
  subst n0; decide
else
  simp only [HAnd.hAnd, AndOp.and, land]
  cases mod_two_eq_zero_or_one n with | _ h => simp [bitwise, n0, h]

Result:
no goals

Proof state:
case inr
n : Nat
n0 : ¬n = 0
h : n % 2 = 1
⊢ bitwise and 1 n = n % 2

Tactic:
simp [bitwise, n0, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem boole_getElem_le_countP (p : α → Bool) (l : Array α) (i : Nat) (h : i < l.size) :
    (if p l[i] then 1 else 0) ≤ l.countP p

Proof state:
α : Type u_1
p : α → Bool
l : Array α
i : Nat
h : i < l.size
⊢ (if p l[i] = true then 1 else 0) ≤ countP p l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ (if p { toList := toList✝ }[i] = true then 1 else 0) ≤ countP p { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p : α → Bool
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ (if p { toList := toList✝ }[i] = true then 1 else 0) ≤ countP p { toList := toList✝ }

Tactic:
simp [List.boole_getElem_le_countP]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem div_four_left {a : ℤ} {b : ℕ} (ha4 : a % 4 = 0) (hb2 : b % 2 = 1) :
    J(a / 4 | b) = J(a | b)

Proof state:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : (↑2).gcd ↑b = 1
⊢ 4 = ↑2 ^ 2

Tactic:
decide

Result:
no goals

Proof state:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ (↑2).gcd ↑b = 1

Tactic:
rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
  Nat.gcd_one_right]

Result:
no goals

Proof state:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : (↑2).gcd ↑b = 1
⊢ 4 ≠ 0

Tactic:
decide

Result:
no goals

Proof state:
a : ℤ
b : ℕ
ha4 : a % 4 = 0
hb2 : b % 2 = 1
⊢ J(a / 4 | b) = J(a | b)

Tactic:
obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha4

Result:
case intro
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ J(4 * a / 4 | b) = J(4 * a | b)

Proof state:
case intro
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ J(4 * a / 4 | b) = J(4 * a | b)

Tactic:
have : Int.gcd (2 : ℕ) b = 1 := by
  rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
    Nat.gcd_one_right]

Result:
case intro
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : (↑2).gcd ↑b = 1
⊢ J(4 * a / 4 | b) = J(4 * a | b)

Proof state:
case intro
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : (↑2).gcd ↑b = 1
⊢ J(4 * a / 4 | b) = J(4 * a | b)

Tactic:
rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left,
  (by decide : (4 : ℤ) = (2 : ℕ) ^ 2), jacobiSym.sq_one' this, one_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem lt_inv_mul_iff_mul_lt : b < a⁻¹ * c ↔ a * b < c

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ a * b < a * (a⁻¹ * c) ↔ a * b < c

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ b < a⁻¹ * c ↔ a * b < c

Tactic:
rw [← mul_lt_mul_iff_left a]

Result:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ a * b < a * (a⁻¹ * c) ↔ a * b < c