harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_map (f : α → β) (a : Vector α n) :
    (a.map f).toList = a.toList.map f

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
a : Vector α n
⊢ (map f a).toList = List.map f a.toList

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : List α) (l' : List β) :
    map (Function.uncurry f) (l.zip l') = zipWith f l l'

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
hl : α
tl : List α
ih : ∀ (l' : List β), map (Function.uncurry f) (zipWith Prod.mk tl l') = zipWith f tl l'
l' : List β
⊢ map (Function.uncurry f) (zipWith Prod.mk (hl :: tl) l') = zipWith f (hl :: tl) l'

Tactic:
cases l' <;> simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l' : List β
⊢ map (Function.uncurry f) (zipWith Prod.mk [] l') = zipWith f [] l'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
⊢ map (Function.uncurry f) (l.zip l') = zipWith f l l'

Tactic:
rw [zip]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
⊢ map (Function.uncurry f) (zipWith Prod.mk l l') = zipWith f l l'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
⊢ map (Function.uncurry f) (zipWith Prod.mk l l') = zipWith f l l'

Tactic:
induction l generalizing l' with
| nil => simp
| cons hl tl ih =>
  cases l' <;> simp [ih]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem head_ofFn {n : ℕ} (f : Fin n.succ → α) : head (ofFn f) = f 0

Proof state:
α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).head = f 0

Tactic:
rw [← get_zero, get_ofFn]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
lemma orbit_submonoid_subset (S : Submonoid M) (a : α) : orbit S a ⊆ orbit M a

Proof state:
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
S : Submonoid M
a : α
⊢ orbit (↥S) a ⊆ orbit M a

Tactic:
rintro b ⟨g, rfl⟩

Result:
case intro
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
S : Submonoid M
a : α
g : ↥S
⊢ (fun m => m • a) g ∈ orbit M a

Proof state:
case intro
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
S : Submonoid M
a : α
g : ↥S
⊢ (fun m => m • a) g ∈ orbit M a

Tactic:
exact mem_orbit _ _

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem coordChange_model_space (b b' x : F) :
    (tangentBundleCore 𝓘(𝕜, F) F).coordChange (achart F b) (achart F b') x = 1

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
b b' x : F
⊢ (tangentBundleCore 𝓘(𝕜, F) F).coordChange (achart F b) (achart F b') x = 1

Tactic:
simpa only [tangentBundleCore_coordChange, mfld_simps] using
  fderivWithin_id uniqueDiffWithinAt_univ

Result:
no goals
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[simp]
lemma carrierEquiv_symm_fst (T : Triplet f g) (p : Spec T.tensor) :
    (pullback.fst f g).base (carrierEquiv.symm ⟨T, p⟩) = T.x

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst f g).base) (carrierEquiv.symm ⟨T, p⟩) = T.x

Tactic:
simp [carrierEquiv]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem iff_quotient_mvPolynomial' : FiniteType R S ↔
    ∃ (ι : Type uS) (_ : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S), Surjective f

Proof state:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f

Tactic:
rintro ⟨s, ⟨f, hsur⟩⟩

Result:
case mp.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
f : MvPolynomial { x // x ∈ s } R →ₐ[R] S
hsur : Surjective ⇑f
⊢ ∃ ι x f, Surjective ⇑f

Proof state:
case mp.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
f : MvPolynomial { x // x ∈ s } R →ₐ[R] S
hsur : Surjective ⇑f
⊢ ∃ ι x f, Surjective ⇑f

Tactic:
use { x : S // x ∈ s }, inferInstance, f

Result:
no goals

Proof state:
case mpr.intro.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
⊢ FiniteType R S

Tactic:
letI : Fintype ι := hfintype

Result:
case mpr.intro.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
this : Fintype ι := hfintype
⊢ FiniteType R S

Proof state:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ ι x f, Surjective ⇑f

Tactic:
rw [iff_quotient_mvPolynomial]

Result:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f

Proof state:
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S ↔ ∃ ι x f, Surjective ⇑f

Tactic:
constructor

Result:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ ι x f, Surjective ⇑f

case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R S

Proof state:
case mpr.intro.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
this : Fintype ι := hfintype
⊢ FiniteType R S

Tactic:
exact FiniteType.of_surjective (FiniteType.mvPolynomial R ι) f hsur

Result:
no goals

Proof state:
case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R S

Tactic:
rintro ⟨ι, ⟨hfintype, ⟨f, hsur⟩⟩⟩

Result:
case mpr.intro.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
⊢ FiniteType R S
-- Mathlib/Order/RelIso/Basic.lean
theorem wellFounded_lift₂_iff {_ : Setoid α} {r : α → α → Prop}
    {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} :
    WellFounded (Quotient.lift₂ r H) ↔ WellFounded r

Proof state:
case mpr.intro
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
exact acc_lift₂_iff.2 (wf.apply a)

Result:
no goals

Proof state:
case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) → WellFounded r

Tactic:
exact RelHomClass.wellFounded (Quotient.mkRelHom H)

Result:
no goals

Proof state:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
q : Quotient x✝
⊢ Acc (Quotient.lift₂ r H) q

Tactic:
obtain ⟨a, rfl⟩ := q.exists_rep

Result:
case mpr.intro
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧

Proof state:
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) ↔ WellFounded r

Tactic:
constructor

Result:
case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) → WellFounded r

case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)

Proof state:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)

Tactic:
refine fun wf => ⟨fun q => ?_⟩

Result:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
q : Quotient x✝
⊢ Acc (Quotient.lift₂ r H) q
-- Mathlib/Data/DFinsupp/Defs.lean
theorem equivFunOnFintype_symm_single [Fintype ι] (i : ι) (m : β i) :
    (@DFinsupp.equivFunOnFintype ι β _ _).symm (Pi.single i m) = DFinsupp.single i m

Proof state:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : β i
⊢ equivFunOnFintype.symm (Pi.single i m) = single i m

Tactic:
ext i'

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : β i
i' : ι
⊢ (equivFunOnFintype.symm (Pi.single i m)) i' = (single i m) i'

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : β i
i' : ι
⊢ (equivFunOnFintype.symm (Pi.single i m)) i' = (single i m) i'

Tactic:
simp only [← single_eq_pi_single, equivFunOnFintype_symm_coe]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsRelPrime.prod_left : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x

Tactic:
classical
refine Finset.induction_on t (fun _ ↦ isRelPrime_one_left) fun b t hbt ih H ↦ ?_
rw [Finset.prod_insert hbt]
rw [Finset.forall_mem_insert] at H
exact H.1.mul_left (ih H.2)

Result:
no goals

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x

Tactic:
refine Finset.induction_on t (fun _ ↦ isRelPrime_one_left) fun b t hbt ih H ↦ ?_

Result:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x

Tactic:
rw [Finset.prod_insert hbt]

Result:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x

Tactic:
exact H.1.mul_left (ih H.2)

Result:
no goals

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x

Tactic:
rw [Finset.forall_mem_insert] at H

Result:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem ae_empty_or_univ_of_preimage_ae_le' (hf : Ergodic f μ) (hs : NullMeasurableSet s μ)
    (hs' : f ⁻¹' s ≤ᵐ[μ] s) (h_fin : μ s ≠ ∞) : s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
refine hf.quasiErgodic.ae_empty_or_univ₀ hs ?_

Result:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : μ s ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : μ s ≠ ⊤
⊢ NullMeasurableSet (f ⁻¹' s) μ

Tactic:
exact hs.preimage hf.quasiMeasurePreserving

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : μ s ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s

Tactic:
refine ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).ge ?_ h_fin

Result:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : μ s ≠ ⊤
⊢ NullMeasurableSet (f ⁻¹' s) μ
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
lemma measure_preimage_fst_singleton_eq_tsum [Countable β] (μ : Measure (α × β)) (x : α) :
    μ (Prod.fst ⁻¹' {x}) = ∑' y, μ {(x, y)}

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable β
μ : Measure (α × β)
x : α
⊢ μ (Prod.fst ⁻¹' {x}) = ∑' (y : β), μ {(x, y)}

Tactic:
rw [← measure_iUnion (by simp [Pairwise]) fun _ ↦ .singleton _, iUnion_singleton_eq_range,
  preimage_fst_singleton_eq_range]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable β
μ : Measure (α × β)
x : α
⊢ Pairwise (Disjoint on fun x_1 => {(x, x_1)})

Tactic:
simp [Pairwise]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem _root_.Eq.sameCycle (h : x = y) (f : Perm α) : f.SameCycle x y

Proof state:
α : Type u_2
x y : α
h : x = y
f : Perm α
⊢ f.SameCycle x y

Tactic:
rw [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem twoBlockTriangular_det (M : Matrix m m R) (p : m → Prop) [DecidablePred p]
    (h : ∀ i, ¬p i → ∀ j, p j → M i j = 0) :
    M.det = (toSquareBlockProp M p).det * (toSquareBlockProp M fun i => ¬p i).det

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det

Tactic:
rw [det_toBlock M p]

Result:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ (fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
        (M.toBlock (fun j => ¬p j) fun j => ¬p j)).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det

Proof state:
case h.e'_2.h.e'_6.h.e'_8
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ M.toBlock (fun j => ¬p j) p = 0

Tactic:
ext i j

Result:
case h.e'_2.h.e'_6.h.e'_8.a
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
i : { a // ¬p a }
j : { a // p a }
⊢ M.toBlock (fun j => ¬p j) p i j = 0 i j

Proof state:
case h.e'_2.h.e'_6.h.e'_8.a
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
i : { a // ¬p a }
j : { a // p a }
⊢ M.toBlock (fun j => ¬p j) p i j = 0 i j

Tactic:
exact h (↑i) i.2 (↑j) j.2

Result:
no goals

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ (fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
        (M.toBlock (fun j => ¬p j) fun j => ¬p j)).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det

Tactic:
convert det_fromBlocks_zero₂₁ (toBlock M p p) (toBlock M p fun j => ¬p j)
    (toBlock M (fun j => ¬p j) fun j => ¬p j)

Result:
case h.e'_2.h.e'_6.h.e'_8
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ M.toBlock (fun j => ¬p j) p = 0
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBasis.isBase_of_spanning (hIX : M.IsBasis I X) (hX : M.Spanning X) : M.IsBase I :=
  hIX.indep.isBase_of_spanning <| by rwa [hIX.spanning_iff_spanning]

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
hX : M.Spanning X
⊢ M.Spanning I

Tactic:
rwa [hIX.spanning_iff_spanning]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma limsup_add_bot_of_ne_top (h : limsup u f = ⊥) (h' : limsup v f ≠ ⊤) :
    limsup (u + v) f = ⊥

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ ⊥ ≠ ⊤ ∨ limsup v f ≠ ⊥

Tactic:
exact .inl bot_ne_top

Result:
no goals

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥

Tactic:
rw [h]

Result:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ ⊥ ≠ ⊤ ∨ limsup v f ≠ ⊥

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥

Tactic:
rw [h, bot_add]

Result:
no goals

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup (u + v) f = ⊥

Tactic:
apply le_bot_iff.1 ((limsup_add_le (.inr h') _).trans _)

Result:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥

α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥
-- Mathlib/Tactic/Module.lean
theorem eval_neg [AddCommGroup M] [Ring R] [Module R M] (l : NF R M) : (-l).eval = - l.eval

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
⊢ (map ((fun x => x.1 • x.2) ∘ fun x => (-x.1, x.2)) l).sum = (map ((fun x => -x) ∘ fun x => x.1 • x.2) l).sum

Tactic:
congr

Result:
case e_a.e_f
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
⊢ ((fun x => x.1 • x.2) ∘ fun x => (-x.1, x.2)) = (fun x => -x) ∘ fun x => x.1 • x.2

Proof state:
case e_a.e_f
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
⊢ ((fun x => x.1 • x.2) ∘ fun x => (-x.1, x.2)) = (fun x => -x) ∘ fun x => x.1 • x.2

Tactic:
ext p

Result:
case e_a.e_f.h
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
p : R × M
⊢ ((fun x => x.1 • x.2) ∘ fun x => (-x.1, x.2)) p = ((fun x => -x) ∘ fun x => x.1 • x.2) p

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
⊢ (-l).eval = -l.eval

Tactic:
simp only [NF.eval, List.map_map, List.sum_neg, NF.instNeg]

Result:
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
⊢ (map ((fun x => x.1 • x.2) ∘ fun x => (-x.1, x.2)) l).sum = (map ((fun x => -x) ∘ fun x => x.1 • x.2) l).sum

Proof state:
case e_a.e_f.h
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
p : R × M
⊢ ((fun x => x.1 • x.2) ∘ fun x => (-x.1, x.2)) p = ((fun x => -x) ∘ fun x => x.1 • x.2) p

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem toComplex_def' (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ) = x + y * I

Proof state:
x y : ℤ
⊢ toComplex { re := x, im := y } = ↑x + ↑y * I

Tactic:
simp [toComplex_def]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc]
lemma comp_liftCycles {A' A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j)
    (hk : k ≫ K.d i j = 0) (α : A' ⟶ A) :
    α ≫ K.liftCycles k j hj hk = K.liftCycles (α ≫ k) j hj (by rw [assoc, hk, comp_zero])

Proof state:
C : Type u_1
inst✝² : Category.{?u.29980, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ (α ≫ k) ≫ K.d i j = 0

Tactic:
rw [assoc, hk, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ α ≫ K.liftCycles k j hj hk = K.liftCycles (α ≫ k) j hj ⋯

Tactic:
simp only [← cancel_mono (K.iCycles i), assoc, liftCycles_i]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : R →+* S) (hf : Function.Injective f)
    (s : ι → Subring R) : (iInf s).map f = ⨅ i, (s i).map f

Proof state:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Ioo_mem_nhdsGT_of_mem (H : b ∈ Ico a c) : Ioo a c ∈ 𝓝[>] b :=
  mem_nhdsWithin.2
    ⟨Iio c, isOpen_Iio, H.2, by rw [inter_comm, Ioi_inter_Iio]; exact Ioo_subset_Ioo_left H.1⟩

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIciTopology α
a b c : α
H : b ∈ Ico a c
⊢ Iio c ∩ Ioi b ⊆ Ioo a c

Tactic:
rw [inter_comm, Ioi_inter_Iio]

Result:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIciTopology α
a b c : α
H : b ∈ Ico a c
⊢ Ioo b c ⊆ Ioo a c

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIciTopology α
a b c : α
H : b ∈ Ico a c
⊢ Ioo b c ⊆ Ioo a c

Tactic:
exact Ioo_subset_Ioo_left H.1

Result:
no goals