harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Congruence/Defs.lean
theorem ext {c d : RingCon R} (H : ∀ x y, c x y ↔ d x y) : c = d :=
  ext' <| by ext; apply H

Proof state:
case h.h.a
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
H : ∀ (x y : R), c x y ↔ d x y
x✝¹ x✝ : R
⊢ c x✝¹ x✝ ↔ d x✝¹ x✝

Tactic:
apply H

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
H : ∀ (x y : R), c x y ↔ d x y
⊢ ⇑c = ⇑d

Tactic:
ext

Result:
case h.h.a
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
H : ∀ (x y : R), c x y ↔ d x y
x✝¹ x✝ : R
⊢ c x✝¹ x✝ ↔ d x✝¹ x✝
-- Mathlib/Algebra/Regular/Basic.lean
theorem IsUnit.isRegular (ua : IsUnit a) : IsRegular a

Proof state:
case intro
R : Type u_1
inst✝ : Monoid R
a : Rˣ
⊢ IsRegular ↑a

Tactic:
exact Units.isRegular a

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Monoid R
a : R
ua : IsUnit a
⊢ IsRegular a

Tactic:
rcases ua with ⟨a, rfl⟩

Result:
case intro
R : Type u_1
inst✝ : Monoid R
a : Rˣ
⊢ IsRegular ↑a
-- Mathlib/Algebra/Lie/Submodule.lean
theorem subset_lieSpan : s ⊆ lieSpan R L s

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
N : LieSubmodule R L M
hN : s ⊆ ↑N
⊢ m ∈ N

Tactic:
exact hN hm

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
⊢ m ∈ ↑(lieSpan R L s)

Tactic:
rw [SetLike.mem_coe, mem_lieSpan]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
⊢ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
⊢ s ⊆ ↑(lieSpan R L s)

Tactic:
intro m hm

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
⊢ m ∈ ↑(lieSpan R L s)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
⊢ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N

Tactic:
intro N hN

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
N : LieSubmodule R L M
hN : s ⊆ ↑N
⊢ m ∈ N
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma top_preconnected : (⊤ : SimpleGraph V).Preconnected := fun x y => by
  if h : x = y then rw [h] else exact Adj.reachable h

Proof state:
V : Type u
x y : V
h : ¬x = y
⊢ ⊤.Reachable x y

Tactic:
exact Adj.reachable h

Result:
no goals

Proof state:
V : Type u
x y : V
⊢ ⊤.Reachable x y

Tactic:
if h : x = y then rw [h] else exact Adj.reachable h

Result:
no goals

Proof state:
V : Type u
x y : V
h : x = y
⊢ ⊤.Reachable x y

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem sym2_toFinset [DecidableEq α] (m : Multiset α) :
    m.toFinset.sym2 = m.sym2.toFinset

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
z : Sym2 α
x y : α
⊢ s(x, y) ∈ m.toFinset.sym2 ↔ s(x, y) ∈ m.sym2.toFinset

Tactic:
simp only [mk_mem_sym2_iff, Multiset.mem_toFinset, Multiset.mk_mem_sym2_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.toFinset.sym2 = m.sym2.toFinset

Tactic:
ext z

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
z : Sym2 α
⊢ z ∈ m.toFinset.sym2 ↔ z ∈ m.sym2.toFinset

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
z : Sym2 α
⊢ z ∈ m.toFinset.sym2 ↔ z ∈ m.sym2.toFinset

Tactic:
refine z.ind fun x y ↦ ?_

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
z : Sym2 α
x y : α
⊢ s(x, y) ∈ m.toFinset.sym2 ↔ s(x, y) ∈ m.sym2.toFinset
-- Mathlib/Data/Set/Prod.lean
theorem pi_update_of_mem [DecidableEq ι] (hi : i ∈ s) (f : ∀ j, α j) (a : α i)
    (t : ∀ j, α j → Set (β j)) :
    (s.pi fun j => t j (update f i a j)) = { x | x i ∈ t i a } ∩ (s \ {i}).pi fun j => t j (f j) :=
  calc
    (s.pi fun j => t j (update f i a j)) = ({i} ∪ s \ {i}).pi fun j => t j (update f i a j)

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (s.pi fun j => t j (update f i a j)) = ({i} ∪ s \ {i}).pi fun j => t j (update f i a j)

Tactic:
rw [union_diff_self, union_eq_self_of_subset_left (singleton_subset_iff.2 hi)]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (({i} ∪ s \ {i}).pi fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi fun j => t j (f j)

Tactic:
rw [union_pi, singleton_pi', update_self, pi_update_of_not_mem]

Result:
case hi
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ i ∉ s \ {i}

Proof state:
case hi
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ i ∉ s \ {i}

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem mulRightMap_apply_single {M N : Submodule R S} {ι : Type*} (n : ι → N) (i : ι) (m : M) :
    mulRightMap M n (Finsupp.single i m) = m.1 * (n i).1

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : SMulCommClass R R S
inst✝ : IsScalarTower R S S
M N : Submodule R S
ι : Type u_5
n : ι → ↥N
i : ι
m : ↥M
⊢ (M.mulRightMap n) (single i m) = ↑m * ↑(n i)

Tactic:
simp [mulRightMap]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iUnion_le [Countable β] (s : β → Set α) (f : α → ℝ≥0∞) :
    ∫⁻ a in ⋃ i, s i, f a ∂μ ≤ ∑' i, ∫⁻ a in s i, f a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

Tactic:
rw [← lintegral_sum_measure]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∫⁻ (a : α), f a ∂sum fun i => μ.restrict (s i)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∫⁻ (a : α), f a ∂sum fun i => μ.restrict (s i)

Tactic:
exact lintegral_mono' restrict_iUnion_le le_rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem tendsto_iff_forall_integral_tendsto {γ : Type*} {F : Filter γ}
    {μs : γ → ProbabilityMeasure Ω} {μ : ProbabilityMeasure Ω} :
    Tendsto μs F (𝓝 μ) ↔
      ∀ f : Ω →ᵇ ℝ,
        Tendsto (fun i ↦ ∫ ω, f ω ∂(μs i : Measure Ω)) F (𝓝 (∫ ω, f ω ∂(μ : Measure Ω)))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔
    ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))

Tactic:
rw [FiniteMeasure.tendsto_iff_forall_integral_tendsto]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ),
      Tendsto (fun i => ∫ (x : Ω), f x ∂↑((toFiniteMeasure ∘ μs) i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ.toFiniteMeasure))) ↔
    ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))

Tactic:
rw [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔
    ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ),
      Tendsto (fun i => ∫ (x : Ω), f x ∂↑((toFiniteMeasure ∘ μs) i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ.toFiniteMeasure))) ↔
    ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearMap.lean
theorem compl₁₂_inj {f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {g : Qₗ →ₗ[R] Mₗ} {g' : Qₗ' →ₗ[R] Nₗ}
    (hₗ : Function.Surjective g) (hᵣ : Function.Surjective g') :
    f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂

Proof state:
case mp.h.h
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x : Mₗ
y : Nₗ
⊢ (f₁ x) y = (f₂ x) y

Tactic:
obtain ⟨x', hx⟩ := hₗ x

Result:
case mp.h.h.intro
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x : Mₗ
y : Nₗ
x' : Qₗ
hx : g x' = x
⊢ (f₁ x) y = (f₂ x) y

Proof state:
case mpr
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'

Tactic:
subst h

Result:
case mpr
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
⊢ f₁.compl₁₂ g g' = f₁.compl₁₂ g g'
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_eq_some_getValueCastD [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
    {fallback : β a} (h : containsKey a l = true) :
    getValueCast? a l = some (getValueCastD a l fallback)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
fallback : β a
h : containsKey a l = true
⊢ getValueCast? a l = some (getValueCastD a l fallback)

Tactic:
rw [getValueCast?_eq_some_getValueCast h, getValueCast_eq_getValueCastD]

Result:
no goals
-- Mathlib/Data/NNReal/Basic.lean
theorem finset_sup_div {α} {f : α → ℝ≥0} {s : Finset α} (r : ℝ≥0) :
    s.sup f / r = s.sup fun a => f a / r

Proof state:
α : Type u_2
f : α → ℝ≥0
s : Finset α
r : ℝ≥0
⊢ s.sup f / r = s.sup fun a => f a / r

Tactic:
simp only [div_eq_inv_mul, mul_finset_sup]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem uncurry {f : α → β → σ} : Primrec (Function.uncurry f) ↔ Primrec₂ f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun p => f p.1 p.2) ↔ Primrec₂ f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec (Function.uncurry f) ↔ Primrec₂ f

Tactic:
rw [show Function.uncurry f = fun p : α × β => f p.1 p.2 from funext fun ⟨a, b⟩ => rfl]

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun p => f p.1 p.2) ↔ Primrec₂ f
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem Functor.map_isPushout [PreservesColimit (span f g) F] (s : IsPushout f g h i) :
    IsPushout (F.map f) (F.map g) (F.map h) (F.map i)

Proof state:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      (Iso.refl ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt).hom =
    ⋯.cocone.ι.app WalkingCospan.right

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅ ⋯.cocone.pt

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ IsPushout (F.map f) (F.map g) (F.map h) (F.map i)

Tactic:
refine
  IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)
      (isColimitOfPreserves F s.isColimit))

Result:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅ ⋯.cocone.pt

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      Iso.hom ?refine_1 =
    ⋯.cocone.ι.app WalkingCospan.left

case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      Iso.hom ?refine_1 =
    ⋯.cocone.ι.app WalkingCospan.right

Proof state:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      (Iso.refl ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt).hom =
    ⋯.cocone.ι.app WalkingCospan.left

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_toArray (f : Nat → α → β) (l : List α) :
    l.toArray.mapIdx f = (l.mapIdx f).toArray

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
⊢ Array.mapIdx f l.toArray = (mapIdx f l).toArray

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem forIn_none [Monad m] (b : β) (f : α → β → m (ForInStep β)) :
    forIn none b f = pure b

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
b : β
f : α → β → m (ForInStep β)
⊢ forIn none b f = pure b

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_nonpos_iff (hx : 0 < x) : logb b x ≤ 0 ↔ x ≤ 1

Proof state:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
rw [← not_lt, logb_pos_iff hb hx, not_lt]

Result:
no goals
-- Mathlib/Analysis/Complex/Polynomial/Basic.lean
theorem exists_root {f : ℂ[X]} (hf : 0 < degree f) : ∃ z : ℂ, IsRoot f z

Proof state:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
⊢ False

Tactic:
obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]

Result:
hf : 0 < (C 0).degree
hf' : ∀ (z : ℂ), ¬(C 0).IsRoot z
this : ∀ (z : ℂ), (eval z (C 0))⁻¹ = 0
⊢ False

Proof state:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
z : ℂ
⊢ (eval z f)⁻¹ = (eval z (C 0))⁻¹

Tactic:
simp [this]

Result:
no goals

Proof state:
hf : 0 < (C 0).degree
hf' : ∀ (z : ℂ), ¬(C 0).IsRoot z
this : ∀ (z : ℂ), (eval z (C 0))⁻¹ = 0
⊢ False

Tactic:
simp at hf

Result:
no goals

Proof state:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
⊢ False

Tactic:
have (z : ℂ) : (f.eval z)⁻¹ = 0 :=
  (f.differentiable.inv hf').apply_eq_of_tendsto_cocompact z <|
    Metric.cobounded_eq_cocompact (α := ℂ) ▸ (Filter.tendsto_inv₀_cobounded.comp <| by
      simpa only [tendsto_norm_atTop_iff_cobounded]
        using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop)

Result:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
⊢ False

Proof state:
f : ℂ[X]
hf : 0 < f.degree
⊢ ∃ z, f.IsRoot z

Tactic:
by_contra! hf'

Result:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
⊢ False

Proof state:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
z : ℂ
⊢ Filter.Tendsto (fun x => eval x f) (cobounded ℂ) (cobounded ℂ)

Tactic:
simpa only [tendsto_norm_atTop_iff_cobounded]
  using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sdiv_zero {x : BitVec n} : x.sdiv 0#n = 0#n

Proof state:
n : Nat
x : BitVec n
⊢ x.sdiv 0#n = 0#n

Tactic:
simp only [sdiv_eq, msb_zero]

Result:
n : Nat
x : BitVec n
⊢ (match x.msb, false with
    | false, false => x.udiv 0#n
    | false, true => -x.udiv (-0#n)
    | true, false => -(-x).udiv 0#n
    | true, true => (-x).udiv (-0#n)) =
    0#n

Proof state:
n : Nat
x : BitVec n
⊢ (match x.msb, false with
    | false, false => x.udiv 0#n
    | false, true => -x.udiv (-0#n)
    | true, false => -(-x).udiv 0#n
    | true, true => (-x).udiv (-0#n)) =
    0#n

Tactic:
rcases x.msb with msb | msb <;> apply eq_of_toNat_eq <;> simp

Result:
no goals
-- Mathlib/Order/Heyting/Boundary.lean
theorem boundary_le_boundary_sup_sup_boundary_inf_left : ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)

Proof state:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ b

Tactic:
rw [hnot_le_iff_codisjoint_right, codisjoint_left_comm]

Result:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)

Tactic:
simp only [boundary, sup_inf_left, sup_inf_right, sup_right_idem, le_inf_iff, sup_assoc,
  sup_comm _ a]

Result:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Proof state:
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊓ b)

Tactic:
rw [hnot_le_iff_codisjoint_right]

Result:
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢(a ⊓ b))

Proof state:
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢(a ⊓ b))

Tactic:
exact codisjoint_hnot_right.mono_right (hnot_anti inf_le_left)

Result:
no goals

Proof state:
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
refine le_sup_of_le_right ?_

Result:
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊓ b)

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩ <;> try { exact le_sup_of_le_left inf_le_left } <;>
  refine inf_le_of_right_le ?_

Result:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ b

case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Proof state:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)

Tactic:
exact codisjoint_hnot_left

Result:
no goals

Proof state:
case refine_5
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))

Tactic:
exact le_sup_of_le_left inf_le_left

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma inv_le_dual :
    I⁻¹ ≤ dual A K I

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I = 0
⊢ I⁻¹ ≤ dual A K I

Tactic:
simp [hI]

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ I⁻¹ ≤ dual A K I

Tactic:
exact if hI : I = 0 then by simp [hI] else le_dual_inv_aux A K hI (le_of_eq (mul_inv_cancel₀ hI))

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ I⁻¹ ≤ dual A K I

Tactic:
classical
exact if hI : I = 0 then by simp [hI] else le_dual_inv_aux A K hI (le_of_eq (mul_inv_cancel₀ hI))

Result:
no goals