harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_baseChange (f : M₁ →ₗ[R] M₂) (i : ι₂) (A : Type*) [CommRing A] [Algebra R A] :
    (f.baseChange A).toMvPolynomial (basis A b₁) (basis A b₂) i =
      MvPolynomial.map (algebraMap R A) (f.toMvPolynomial b₁ b₂ i)

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Fintype ι₁
inst✝³ : Finite ι₂
inst✝² : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ toMvPolynomial (basis A b₁) (basis A b₂) (baseChange A f) i =
    (MvPolynomial.map (algebraMap R A)) (toMvPolynomial b₁ b₂ f i)

Tactic:
simp only [toMvPolynomial, toMatrix_baseChange, Matrix.toMvPolynomial_map]

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem powersetCard_eq_filter {n} {s : Finset α} :
    powersetCard n s = (powerset s).filter fun x => x.card = n

Proof state:
case h
α : Type u_1
n : ℕ
s a✝ : Finset α
⊢ a✝ ∈ powersetCard n s ↔ a✝ ∈ filter (fun x => #x = n) s.powerset

Tactic:
simp [mem_powersetCard]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = filter (fun x => #x = n) s.powerset

Tactic:
ext

Result:
case h
α : Type u_1
n : ℕ
s a✝ : Finset α
⊢ a✝ ∈ powersetCard n s ↔ a✝ ∈ filter (fun x => #x = n) s.powerset
-- Mathlib/Data/Set/Sups.lean
theorem image_inf_prod (s t : Set α) : Set.image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t

Proof state:
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
this : (uncurry fun x1 x2 => x1 ⊓ x2) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t
⊢ image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t

Tactic:
rw [← this]

Result:
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
this : (uncurry fun x1 x2 => x1 ⊓ x2) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t
⊢ (uncurry fun x1 x2 => x1 ⊓ x2) '' s ×ˢ t = s ⊼ t

Proof state:
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
⊢ (uncurry fun x1 x2 => x1 ⊓ x2) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t

Tactic:
simp only [Set.image_uncurry_prod]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
this : (uncurry fun x1 x2 => x1 ⊓ x2) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t
⊢ (uncurry fun x1 x2 => x1 ⊓ x2) '' s ×ˢ t = s ⊼ t

Tactic:
exact image_uncurry_prod _ _ _

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_pow (s : Finset ι) (f : ι → M) (n : ℕ) :
    (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun _ : Fin n ↦ s, ∏ i, f (p i)

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun x => s, ∏ i : Fin n, f (p i)

Tactic:
rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun x => s, ∏ i : Fin n, f (p i)

Tactic:
classical
rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]

Result:
no goals
-- Mathlib/AlgebraicTopology/CechNerve.lean
@[reassoc (attr := simp)]
lemma wideCospan.limitIsoPi_hom_comp_pi [Finite ι] (X : C) (j : ι) :
    (wideCospan.limitIsoPi ι X).hom ≫ Pi.π _ j = WidePullback.π _ j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j : ι
⊢ (limitIsoPi ι X).hom ≫ Pi.π (fun x => X) j = WidePullback.π (fun x => terminal.from X) j

Tactic:
rw [← wideCospan.limitIsoPi_inv_comp_pi, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem plusLift_unique {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q)
    (γ : J.plusObj P ⟶ Q) (hγ : J.toPlus P ≫ γ = η) : γ = J.plusLift η hQ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ ≫ (J.isoToPlus Q hQ).hom = J.plusMap (J.toPlus P) ≫ J.plusMap γ

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ = J.plusLift η hQ

Tactic:
dsimp only [plusLift]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ = J.plusMap η ≫ (J.isoToPlus Q hQ).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ = J.plusMap η ≫ (J.isoToPlus Q hQ).inv

Tactic:
rw [Iso.eq_comp_inv, ← hγ, plusMap_comp]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ ≫ (J.isoToPlus Q hQ).hom = J.plusMap (J.toPlus P) ≫ J.plusMap γ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem resolve_left_eq (a c d p x : Int) (h₁ : p ≤ a * x) :
    resolve_left a c d p x = resolve_left' a c d p x h₁

Proof state:
a c d p x : Int
h₁ : p ≤ a * x
⊢ resolve_left a c d p x = ↑(resolve_left' a c d p x h₁)

Tactic:
simp only [resolve_left, resolve_left', add_of_le, ofNat_emod, ofNat_toNat]

Result:
a c d p x : Int
h₁ : p ≤ a * x
⊢ (a * x - p) % ↑(a.lcm (a * d / ↑((a * d).gcd c))) = max (a * x - p) 0 % ↑(a.lcm (a * d / ↑((a * d).gcd c)))

Proof state:
a c d p x : Int
h₁ : p ≤ a * x
⊢ (a * x - p) % ↑(a.lcm (a * d / ↑((a * d).gcd c))) = max (a * x - p) 0 % ↑(a.lcm (a * d / ↑((a * d).gcd c)))

Tactic:
rw [Int.max_eq_left]

Result:
a c d p x : Int
h₁ : p ≤ a * x
⊢ 0 ≤ a * x - p

Proof state:
a c d p x : Int
h₁ : p ≤ a * x
⊢ 0 ≤ a * x - p

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
theorem _root_.Set.PairwiseDisjoint.exists_mem_filter {ι : Type*} {l : ι → Filter α} {t : Set ι}
    (hd : t.PairwiseDisjoint l) (ht : t.Finite) :
    ∃ s : ι → Set α, (∀ i, s i ∈ l i) ∧ t.PairwiseDisjoint s

Proof state:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩

Result:
case intro.intro
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
s : ↑t → Set α
hsl : ∀ (i : ↑t), s i ∈ l ↑i
hsd : Pairwise (Disjoint on s)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Proof state:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
haveI := ht.to_subtype

Result:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Proof state:
case intro.intro.intro
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
s : (i : ↑t) → { s // s ∈ l ↑i }
hsd : Pairwise (Disjoint on fun i => ↑(s i))
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
rcases @Subtype.exists_pi_extension ι (fun i => { s // s ∈ l i }) _ _ s with ⟨s, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
s : (i : ι) → { s // s ∈ l i }
hsd : Pairwise (Disjoint on fun i => ↑((fun i => s ↑i) i))
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Proof state:
case intro.intro
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
s : ↑t → Set α
hsl : ∀ (i : ↑t), s i ∈ l ↑i
hsd : Pairwise (Disjoint on s)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
lift s to (i : t) → {s // s ∈ l i} using hsl

Result:
case intro.intro.intro
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
s : (i : ↑t) → { s // s ∈ l ↑i }
hsd : Pairwise (Disjoint on fun i => ↑(s i))
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Proof state:
case intro.intro.intro.intro
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
s : (i : ι) → { s // s ∈ l i }
hsd : Pairwise (Disjoint on fun i => ↑((fun i => s ↑i) i))
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
exact ⟨fun i => s i, fun i => (s i).2, hsd.set_of_subtype _ _⟩

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem cast_toNat_eq_iff_lt_aleph0 {c : Cardinal} : (toNat c) = c ↔ c < ℵ₀

Proof state:
case mp
c : Cardinal.{u_1}
h : ↑0 = c
h' : ℵ₀ ≤ ↑0
⊢ False

Tactic:
absurd h'

Result:
case mp
c : Cardinal.{u_1}
h : ↑0 = c
h' : ℵ₀ ≤ ↑0
⊢ ¬ℵ₀ ≤ ↑0

Proof state:
case mpr
c : Cardinal.{u_1}
⊢ c < ℵ₀ → ↑(toNat c) = c

Tactic:
exact fun h ↦ (Cardinal.cast_toNat_of_lt_aleph0 h)

Result:
no goals

Proof state:
case mp
c : Cardinal.{u_1}
h : ↑0 = c
h' : ℵ₀ ≤ c
⊢ False

Tactic:
rw [← h] at h'

Result:
case mp
c : Cardinal.{u_1}
h : ↑0 = c
h' : ℵ₀ ≤ ↑0
⊢ False

Proof state:
case mp
c : Cardinal.{u_1}
h : ↑(toNat c) = c
h' : ℵ₀ ≤ c
⊢ False

Tactic:
rw [toNat_apply_of_aleph0_le h'] at h

Result:
case mp
c : Cardinal.{u_1}
h : ↑0 = c
h' : ℵ₀ ≤ c
⊢ False

Proof state:
case mp
c : Cardinal.{u_1}
⊢ ↑(toNat c) = c → c < ℵ₀

Tactic:
intro h

Result:
case mp
c : Cardinal.{u_1}
h : ↑(toNat c) = c
⊢ c < ℵ₀

Proof state:
c : Cardinal.{u_1}
⊢ ↑(toNat c) = c ↔ c < ℵ₀

Tactic:
constructor

Result:
case mp
c : Cardinal.{u_1}
⊢ ↑(toNat c) = c → c < ℵ₀

case mpr
c : Cardinal.{u_1}
⊢ c < ℵ₀ → ↑(toNat c) = c

Proof state:
case mp
c : Cardinal.{u_1}
h : ↑0 = c
h' : ℵ₀ ≤ ↑0
⊢ ↑0 < ℵ₀

Tactic:
exact nat_lt_aleph0 0

Result:
no goals

Proof state:
case mp
c : Cardinal.{u_1}
h : ↑0 = c
h' : ℵ₀ ≤ ↑0
⊢ ¬ℵ₀ ≤ ↑0

Tactic:
rw [not_le]

Result:
case mp
c : Cardinal.{u_1}
h : ↑0 = c
h' : ℵ₀ ≤ ↑0
⊢ ↑0 < ℵ₀

Proof state:
case mp
c : Cardinal.{u_1}
h : ↑(toNat c) = c
h' : ¬c < ℵ₀
⊢ False

Tactic:
rw [not_lt] at h'

Result:
case mp
c : Cardinal.{u_1}
h : ↑(toNat c) = c
h' : ℵ₀ ≤ c
⊢ False

Proof state:
case mp
c : Cardinal.{u_1}
h : ↑(toNat c) = c
⊢ c < ℵ₀

Tactic:
by_contra h'

Result:
case mp
c : Cardinal.{u_1}
h : ↑(toNat c) = c
h' : ¬c < ℵ₀
⊢ False
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem one_le_hausdorffMeasure_zero_of_nonempty {s : Set X} (h : s.Nonempty) : 1 ≤ μH[0] s

Proof state:
case intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
x : X
hx : x ∈ s
⊢ 1 ≤ μH[0] s

Tactic:
calc
  (1 : ℝ≥0∞) = μH[0] ({x} : Set X) := (hausdorffMeasure_zero_singleton x).symm
  _ ≤ μH[0] s := measure_mono (singleton_subset_iff.2 hx)

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
h : s.Nonempty
⊢ 1 ≤ μH[0] s

Tactic:
rcases h with ⟨x, hx⟩

Result:
case intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
x : X
hx : x ∈ s
⊢ 1 ≤ μH[0] s
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_ofNat_succ (a n : ℕ) [h : a.AtLeastTwo] :
    coeff (ofNat(a) : R[X]) (n + 1) = 0

Proof state:
R : Type u
inst✝ : Semiring R
a n : ℕ
h : a.AtLeastTwo
⊢ (OfNat.ofNat a).coeff (n + 1) = 0

Tactic:
rw [← Nat.cast_ofNat]

Result:
R : Type u
inst✝ : Semiring R
a n : ℕ
h : a.AtLeastTwo
⊢ (↑(OfNat.ofNat a)).coeff (n + 1) = 0

Proof state:
R : Type u
inst✝ : Semiring R
a n : ℕ
h : a.AtLeastTwo
⊢ (↑(OfNat.ofNat a)).coeff (n + 1) = 0

Tactic:
simp [-Nat.cast_ofNat]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_self_eq_norm_mul_norm (x : F) : ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖

Tactic:
have h := @inner_self_eq_norm_mul_norm ℝ F _ _ _ x

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
h : re ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
⊢ ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
h : re ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
⊢ ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖

Tactic:
simpa using h

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem tendsto_setLIntegral_zero {ι} {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ ≠ ∞) {l : Filter ι}
    {s : ι → Set α} (hl : Tendsto (μ ∘ s) l (𝓝 0)) :
    Tendsto (fun i => ∫⁻ x in s i, f x ∂μ) l (𝓝 0)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (⇑μ ∘ s) a < i
⊢ ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < i

Tactic:
intro ε ε0

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (⇑μ ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < ε

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ⊤
l : Filter ι
s : ι → Set α
hl : Tendsto (⇑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun i => ∫⁻ (x : α) in s i, f x ∂μ) l (𝓝 0)

Tactic:
simp only [ENNReal.nhds_zero, tendsto_iInf, tendsto_principal, mem_Iio,
  ← pos_iff_ne_zero] at hl ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (⇑μ ∘ s) a < i
⊢ ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < i

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (⇑μ ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < ε

Tactic:
rcases exists_pos_setLIntegral_lt_of_measure_lt h ε0.ne' with ⟨δ, δ0, hδ⟩

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (⇑μ ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
δ : ℝ≥0∞
δ0 : δ > 0
hδ : ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
⊢ ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < ε

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (⇑μ ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
δ : ℝ≥0∞
δ0 : δ > 0
hδ : ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
⊢ ∀ᶠ (a : ι) in l, ∫⁻ (x : α) in s a, f x ∂μ < ε

Tactic:
exact (hl δ δ0).mono fun i => hδ _

Result:
no goals
-- Mathlib/RingTheory/Localization/Integral.lean
theorem isFractionRing_of_algebraic [Algebra.IsAlgebraic A L]
    (inj : ∀ x, algebraMap A L x = 0 → x = 0) : IsFractionRing C L :=
  { map_units' := fun ⟨y, hy⟩ =>
      IsUnit.mk0 _
        (show algebraMap C L y ≠ 0 from fun h =>
          mem_nonZeroDivisors_iff_ne_zero.mp hy
            ((injective_iff_map_eq_zero (algebraMap C L)).mp (algebraMap_injective C A L) _ h))
    surj' := fun z =>
      let ⟨x, hx, int⟩ := (Algebra.IsAlgebraic.isAlgebraic z).exists_integral_multiple
      ⟨⟨mk' C _ int, algebraMap _ _ x, mem_nonZeroDivisors_of_ne_zero fun h ↦
        hx (inj _ <| by rw [IsScalarTower.algebraMap_apply A C L, h, RingHom.map_zero])⟩, by
        rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, Algebra.smul_def, mul_comm]⟩
    exists_of_eq := fun {x y} h => ⟨1, by simpa using algebraMap_injective C A L h⟩ }

Proof state:
A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
⊢ z * (algebraMap C L) ↑(mk' C (x • z) int, ⟨(algebraMap A C) x, ⋯⟩).2 =
    (algebraMap C L) (mk' C (x • z) int, ⟨(algebraMap A C) x, ⋯⟩).1

Tactic:
rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, Algebra.smul_def, mul_comm]

Result:
no goals

Proof state:
A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
x y : C
h : (algebraMap C L) x = (algebraMap C L) y
⊢ ↑1 * x = ↑1 * y

Tactic:
simpa using algebraMap_injective C A L h

Result:
no goals

Proof state:
A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
h : (algebraMap A C) x = 0
⊢ (algebraMap A L) x = 0

Tactic:
rw [IsScalarTower.algebraMap_apply A C L, h, RingHom.map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/DecidableEq.lean
theorem beq_toList [BEq α] (a b : Vector α n) : (a.toList == b.toList) = (a == b)

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a b : Vector α n
⊢ (a.toList == b.toList) = (a == b)

Tactic:
simp [beq_eq_decide, List.beq_eq_decide]

Result:
no goals
-- Mathlib/Computability/EpsilonNFA.lean
theorem isPath_singleton {a : Option α} : M.IsPath s t [a] ↔ t ∈ M.step s a where
  mp

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
⊢ M.IsPath s t [a] → t ∈ M.step s a

Tactic:
rintro (_ | ⟨_, _, _, _, _, _, ⟨⟩⟩)

Result:
case cons.nil
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
a✝ : t ∈ M.step s a
⊢ t ∈ M.step s a

Proof state:
case cons.nil
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
a✝ : t ∈ M.step s a
⊢ t ∈ M.step s a

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
⊢ t ∈ M.step s a → M.IsPath s t [a]

Tactic:
tauto

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_setIfInBounds_ne (v : Vector α n) (i : Nat) (x : α) (j : Nat)
    (hj : j < n) (h : i ≠ j) : (v.setIfInBounds i x)[j] = v[j]

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
x : α
j : Nat
hj : j < n
h : i ≠ j
⊢ (v.setIfInBounds i x)[j] = v[j]

Tactic:
simp [getElem_setIfInBounds, h]

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} {H}
    (hf : ∀ a ha b hb, f a ha = f b hb → a = b) (h : Nodup l) : Nodup (pmap f l H)

Proof state:
case e_val
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ a ∈ l, p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h✝ : l.Nodup
x✝¹ x✝ : { x // x ∈ l }
a : α
ha : a ∈ l
b : α
hb : b ∈ l
h : f ↑⟨a, ha⟩ ⋯ = f ↑⟨b, hb⟩ ⋯
⊢ a = b

Tactic:
exact hf a (H _ ha) b (H _ hb) h

Result:
no goals

Proof state:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ a ∈ l, p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : l.Nodup
⊢ (map (fun x => f ↑x ⋯) l.attach).Nodup

Tactic:
exact h.attach.map fun ⟨a, ha⟩ ⟨b, hb⟩ h => by congr; exact hf a (H _ ha) b (H _ hb) h

Result:
no goals

Proof state:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ a ∈ l, p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h✝ : l.Nodup
x✝¹ x✝ : { x // x ∈ l }
a : α
ha : a ∈ l
b : α
hb : b ∈ l
h : f ↑⟨a, ha⟩ ⋯ = f ↑⟨b, hb⟩ ⋯
⊢ ⟨a, ha⟩ = ⟨b, hb⟩

Tactic:
congr

Result:
case e_val
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ a ∈ l, p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h✝ : l.Nodup
x✝¹ x✝ : { x // x ∈ l }
a : α
ha : a ∈ l
b : α
hb : b ∈ l
h : f ↑⟨a, ha⟩ ⋯ = f ↑⟨b, hb⟩ ⋯
⊢ a = b

Proof state:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ a ∈ l, p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : l.Nodup
⊢ (List.pmap f l H).Nodup

Tactic:
rw [pmap_eq_map_attach]

Result:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ a ∈ l, p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : l.Nodup
⊢ (map (fun x => f ↑x ⋯) l.attach).Nodup
-- Mathlib/Geometry/Manifold/Diffeomorph.lean
theorem uniqueMDiffOn_image_aux (h : M ≃ₘ^n⟮I, J⟯ N) (hn : 1 ≤ n) {s : Set M}
    (hs : UniqueMDiffOn I s) : UniqueMDiffOn J (h '' s)

Proof state:
case h.e'_12
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁵ : TopologicalSpace H
G : Type u_7
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
hn : 1 ≤ n
s : Set M
hs : UniqueMDiffOn I s
⊢ ⇑h '' s = h.toHomeomorph.toPartialHomeomorph.target ∩ ↑h.toHomeomorph.toPartialHomeomorph.symm ⁻¹' s

Tactic:
simp [h.image_eq_preimage]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁵ : TopologicalSpace H
G : Type u_7
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
hn : 1 ≤ n
s : Set M
hs : UniqueMDiffOn I s
⊢ UniqueMDiffOn J (⇑h '' s)

Tactic:
convert hs.uniqueMDiffOn_preimage (h.toPartialHomeomorph_mdifferentiable hn)

Result:
case h.e'_12
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁵ : TopologicalSpace H
G : Type u_7
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
hn : 1 ≤ n
s : Set M
hs : UniqueMDiffOn I s
⊢ ⇑h '' s = h.toHomeomorph.toPartialHomeomorph.target ∩ ↑h.toHomeomorph.toPartialHomeomorph.symm ⁻¹' s