harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Satisfiability.lean
theorem ModelsBoundedFormula.realize_boundedFormula
    {φ : L.BoundedFormula α n} (h : T ⊨ᵇ φ) (M : Type*)
    [L.Structure M] [M ⊨ T] [Nonempty M] {v : α → M} {xs : Fin n → M} : φ.Realize v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
xs : Fin n → M
h' : φ.toFormula.Realize (Sum.elim v xs)
⊢ φ.Realize v xs

Tactic:
simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
xs : Fin n → M
h' : φ.Realize v xs
⊢ φ.Realize v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
xs : Fin n → M
h' : φ.Realize v xs
⊢ φ.Realize v xs

Tactic:
exact h'

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs

Tactic:
have h' : φ.toFormula.Realize (Sum.elim v xs) := (models_toFormula_iff.2 h).realize_formula M

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
xs : Fin n → M
h' : φ.toFormula.Realize (Sum.elim v xs)
⊢ φ.Realize v xs
-- Mathlib/LinearAlgebra/Dual.lean
theorem finrank_add_finrank_dualAnnihilator_eq (W : Subspace K V) :
    finrank K W + finrank K W.dualAnnihilator = finrank K V

Proof state:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
⊢ finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V

Tactic:
rw [← W.quotEquivAnnihilator.finrank_eq (M₂ := dualAnnihilator W),
  add_comm, Submodule.finrank_quotient_add_finrank]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
lemma MonoOver.subobjectMk_le_mk_of_hom {P Q : MonoOver X} (f : P ⟶ Q) :
    Subobject.mk P.obj.hom ≤ Subobject.mk Q.obj.hom :=
  Subobject.mk_le_mk_of_comm f.left (by simp)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P Q : MonoOver X
f : P ⟶ Q
⊢ f.left ≫ Q.obj.hom = P.obj.hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem prod_multiset_X_sub_C_of_monic_of_roots_card_eq (hp : p.Monic)
    (hroots : Multiset.card p.roots = p.natDegree) : (p.roots.map fun a => X - C a).prod = p

Proof state:
case h.e'_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hroots : p.roots.card = p.natDegree
⊢ (Multiset.map (fun a => X - C a) p.roots).prod = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod

Tactic:
rw [hp.leadingCoeff, C_1, one_mul]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hroots : p.roots.card = p.natDegree
⊢ (Multiset.map (fun a => X - C a) p.roots).prod = p

Tactic:
convert C_leadingCoeff_mul_prod_multiset_X_sub_C hroots

Result:
case h.e'_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hroots : p.roots.card = p.natDegree
⊢ (Multiset.map (fun a => X - C a) p.roots).prod = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem none_eq_getElem?_iff {a : Array α} {i : Nat} : none = a[i]? ↔ a.size ≤ i

Proof state:
α : Type u_1
a : Array α
i : Nat
⊢ none = a[i]? ↔ a.size ≤ i

Tactic:
simp [eq_comm (a := none)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem map_snd_add_zipIdx_eq_zipIdx (l : Vector α n) (m k : Nat) :
    map (Prod.map id (· + m)) (zipIdx l k) = zipIdx l (m + k)

Proof state:
α : Type u_1
n : Nat
l : Vector α n
m k : Nat
⊢ map (Prod.map id fun x => x + m) (l.zipIdx k) = l.zipIdx (m + k)

Tactic:
ext <;> simp <;> omega

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/FunctorCategory.lean
theorem app_sum {ι : Type*} (s : Finset ι) (X : C) (α : ι → (F ⟶ G)) :
    (∑ i ∈ s, α i).app X = ∑ i ∈ s, (α i).app X

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_5, u_1} C
inst✝¹ : Category.{u_4, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
ι : Type u_3
s : Finset ι
X : C
α : ι → (F ⟶ G)
⊢ (∑ i ∈ s, α i).app X = ∑ i ∈ s, (α i).app X

Tactic:
simp only [← appHom_apply, map_sum]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_eq_top_iff_zero {a : Associates α} : a.factors = ⊤ ↔ a = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
a✝ : Nontrivial α
⊢ a.factors = ⊤ ↔ a = 0

Tactic:
exact ⟨fun h ↦ by rwa [← factors_prod a, FactorSet.prod_eq_zero_iff], fun h ↦ h ▸ factors_zero⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
a✝ : Nontrivial α
h : a.factors = ⊤
⊢ a = 0

Tactic:
rwa [← factors_prod a, FactorSet.prod_eq_zero_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors = ⊤ ↔ a = 0

Tactic:
nontriviality α

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
a✝ : Nontrivial α
⊢ a.factors = ⊤ ↔ a = 0
-- Mathlib/Data/Rat/Floor.lean
theorem cast_fract (x : ℚ) : (↑(fract x) : α) = fract (x : α)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ ↑(fract x) = fract ↑x

Tactic:
simp only [fract, cast_sub, cast_intCast, floor_cast]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem inv_single {R} [DivisionRing R] {a b : R}
    (_ : (a : R)⁻¹ = b) : (a + 0)⁻¹ = b + 0

Proof state:
R : Type u_2
inst✝ : DivisionRing R
a b : R
x✝ : a⁻¹ = b
⊢ (a + 0)⁻¹ = b + 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 < a
h : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
simpa using inv_anti₀ ha h

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_lt [LinearOrderedRing α] {m n : ZNum} : (m : α) < n ↔ m < n

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
m n : ZNum
⊢ ↑m < ↑n ↔ m < n

Tactic:
rw [← cast_to_int m, ← cast_to_int n, Int.cast_lt, lt_to_int]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma comp_apply {R S T : SemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) :
    (f ≫ g) r = g (f r)

Proof state:
R S T : SemiRingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem imageMonoIsoSource_inv_ι [Mono f] : (imageMonoIsoSource f).inv ≫ image.ι f = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).inv ≫ image.ι f = f

Tactic:
simp [imageMonoIsoSource]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem clusterPt_principal_iff_frequently :
    ClusterPt x (𝓟 s) ↔ ∃ᶠ y in 𝓝 x, y ∈ s

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ ClusterPt x (𝓟 s) ↔ ∃ᶠ (y : X) in 𝓝 x, y ∈ s

Tactic:
simp only [clusterPt_principal_iff, frequently_iff, Set.Nonempty, exists_prop, mem_inter_iff]

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem toSpanSingleton_surjective {m : M} (hm : m ≠ 0) :
    Function.Surjective (toSpanSingleton R M m)

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Function.Surjective ⇑(toSpanSingleton R M m)

Tactic:
rw [← range_eq_top, ← span_singleton_eq_range, span_singleton_eq_top R hm]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_two : dickson k a 2 = X ^ 2 - C a * (3 - k : R[X])

Proof state:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
⊢ dickson k a 2 = X ^ 2 - C a * (3 - ↑k)

Tactic:
simp only [dickson, sq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_eq_append_iff {l₁ : Array α} {l₂ : Array β} :
    zip l₁ l₂ = l₁' ++ l₂' ↔
      ∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z

Proof state:
α : Type u_1
β : Type u_2
l₁' l₂' : Array (α × β)
l₁ : Array α
l₂ : Array β
⊢ l₁.zip l₂ = l₁' ++ l₂' ↔ ∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = w.zip y ∧ l₂' = x.zip z

Tactic:
simp [zip_eq_zipWith, zipWith_eq_append_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem conjugate_lt_conjugate {a b : R} (hab : a < b) {c : R} (hc : IsRegular c) :
    star c * a * c < star c * b * c

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ a ≠ b

Tactic:
exact hab.ne

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ star c * a * c < star c * b * c

Tactic:
rw [(conjugate_le_conjugate hab.le _).lt_iff_ne, hc.right.ne_iff, hc.star.left.ne_iff]

Result:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ a ≠ b
-- Mathlib/RingTheory/MvPolynomial/Groebner.lean
theorem div_set {B : Set (MvPolynomial σ R)}
    (hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)) (f : MvPolynomial σ R) :
    ∃ (g : B →₀ (MvPolynomial σ R)) (r : MvPolynomial σ R),
      f = Finsupp.linearCombination _ (fun (b : B) ↦ (b : MvPolynomial σ R)) g + r ∧
        (∀ (b : B), m.degree ((b : MvPolynomial σ R) * (g b)) ≼[m] m.degree f) ∧
        (∀ c ∈ r.support, ∀ b ∈ B, ¬ (m.degree b ≤ c))

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
B : Set (MvPolynomial σ R)
hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) fun b => ↑b) g + r ∧
      (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c

Tactic:
obtain ⟨g, r, H⟩ := m.div (b := fun (p : B) ↦ p) (fun b ↦ hB b b.prop) f

Result:
case intro.intro
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
B : Set (MvPolynomial σ R)
hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑B →₀ MvPolynomial σ R
r : MvPolynomial σ R
H :
  f = (Finsupp.linearCombination (MvPolynomial σ R) fun p => ↑p) g + r ∧
    (∀ (i : ↑B), m.toSyn (m.degree (↑i * g i)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ (i : ↑B), ¬m.degree ↑i ≤ c
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) fun b => ↑b) g + r ∧
      (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c

Proof state:
case intro.intro
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
B : Set (MvPolynomial σ R)
hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑B →₀ MvPolynomial σ R
r : MvPolynomial σ R
H :
  f = (Finsupp.linearCombination (MvPolynomial σ R) fun p => ↑p) g + r ∧
    (∀ (i : ↑B), m.toSyn (m.degree (↑i * g i)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ (i : ↑B), ¬m.degree ↑i ≤ c
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) fun b => ↑b) g + r ∧
      (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c

Tactic:
exact ⟨g, r, H.1, H.2.1, fun c hc b hb ↦ H.2.2 c hc ⟨b, hb⟩⟩

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem eqOn_univ (f₁ f₂ : α → β) : EqOn f₁ f₂ univ ↔ f₁ = f₂

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
⊢ EqOn f₁ f₂ univ ↔ f₁ = f₂

Tactic:
simp [EqOn, funext_iff]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem append_comm (s : Sym α n') (s' : Sym α n') :
    s.append s' = Sym.cast (add_comm _ _) (s'.append s)

Proof state:
α : Type u_1
n' : ℕ
s s' : Sym α n'
⊢ s.append s' = (Sym.cast ⋯) (s'.append s)

Tactic:
ext

Result:
case h
α : Type u_1
n' : ℕ
s s' : Sym α n'
⊢ ↑(s.append s') = ↑((Sym.cast ⋯) (s'.append s))

Proof state:
case h
α : Type u_1
n' : ℕ
s s' : Sym α n'
⊢ ↑(s.append s') = ↑((Sym.cast ⋯) (s'.append s))

Tactic:
simp [append, add_comm]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem mem_resolventSet_of_left_right_inverse {r : R} {a b c : A} (h₁ : (↑ₐ r - a) * b = 1)
    (h₂ : c * (↑ₐ r - a) = 1) : r ∈ resolventSet R a :=
  Units.isUnit ⟨↑ₐ r - a, b, h₁, by rwa [← left_inv_eq_right_inv h₂ h₁]⟩

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a b c : A
h₁ : (↑ₐ r - a) * b = 1
h₂ : c * (↑ₐ r - a) = 1
⊢ b * (↑ₐ r - a) = 1

Tactic:
rwa [← left_inv_eq_right_inv h₂ h₁]

Result:
no goals
-- Mathlib/Analysis/Convex/Extreme.lean
theorem IsExtreme.extremePoints_subset_extremePoints (hAB : IsExtreme 𝕜 A B) :
    B.extremePoints 𝕜 ⊆ A.extremePoints 𝕜 :=
  fun _ ↦ by simpa only [← isExtreme_singleton] using hAB.trans

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B : Set E
hAB : IsExtreme 𝕜 A B
x✝ : E
⊢ x✝ ∈ extremePoints 𝕜 B → x✝ ∈ extremePoints 𝕜 A

Tactic:
simpa only [← isExtreme_singleton] using hAB.trans

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.IsOpen.exists_eq_add_of_deriv_eq {f g : 𝕜 → G} (hs : IsOpen s)
    (hs' : IsPreconnected s)
    (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s)
    (hf' : s.EqOn (deriv f) (deriv g)) : ∃ a, s.EqOn f (g · + a) :=
  hs.exists_eq_add_of_fderiv_eq hs' hf hg (fun x hx ↦ by ext; simp [← deriv_fderiv, hf' hx])

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set 𝕜
f g : 𝕜 → G
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (deriv f) (deriv g) s
x : 𝕜
hx : x ∈ s
⊢ fderiv 𝕜 f x = fderiv 𝕜 g x

Tactic:
ext

Result:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set 𝕜
f g : 𝕜 → G
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (deriv f) (deriv g) s
x : 𝕜
hx : x ∈ s
⊢ (fderiv 𝕜 f x) 1 = (fderiv 𝕜 g x) 1

Proof state:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set 𝕜
f g : 𝕜 → G
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (deriv f) (deriv g) s
x : 𝕜
hx : x ∈ s
⊢ (fderiv 𝕜 f x) 1 = (fderiv 𝕜 g x) 1

Tactic:
simp [← deriv_fderiv, hf' hx]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem zpow_comm (a : α) (m n : ℤ) : (a ^ m) ^ n = (a ^ n) ^ m

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℤ
⊢ (a ^ m) ^ n = (a ^ n) ^ m

Tactic:
rw [← zpow_mul, zpow_mul']

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem InjOn.encard_image (h : InjOn f s) : (f '' s).encard = s.encard

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
⊢ (f '' s).encard = s.encard

Tactic:
rw [encard, ENat.card_image_of_injOn h, encard]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem edist_one_left (a : E) : edist 1 a = ‖a‖₊

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ edist 1 a = ↑‖a‖₊

Tactic:
rw [edist_nndist, nndist_one_left]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_subset (x y : ∀ i, π i) : segment 𝕜 x y ⊆ s.pi fun i => segment 𝕜 (x i) (y i)

Proof state:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y : (i : ι) → π i
⊢ [x-[𝕜]y] ⊆ s.pi fun i => [x i-[𝕜]y i]

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y z : (i : ι) → π i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i => [x i-[𝕜]y i]) i

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y z : (i : ι) → π i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i => [x i-[𝕜]y i]) i

Tactic:
exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem zero_tmod (b : Int) : tmod 0 b = 0

Proof state:
b : Int
⊢ tmod 0 b = 0

Tactic:
cases b <;> simp [tmod]

Result:
no goals
-- Mathlib/Order/RelIso/Basic.lean
theorem toEquiv_injective : Injective (toEquiv : r ≃r s → α ≃ β)
  | ⟨e₁, o₁⟩, ⟨e₂, _⟩, h => by congr

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e₁ : α ≃ β
o₁ : ∀ {a b : α}, s (e₁ a) (e₁ b) ↔ r a b
e₂ : α ≃ β
map_rel_iff'✝ : ∀ {a b : α}, s (e₂ a) (e₂ b) ↔ r a b
h : { toEquiv := e₁, map_rel_iff' := o₁ }.toEquiv = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }.toEquiv
⊢ { toEquiv := e₁, map_rel_iff' := o₁ } = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
lemma WithZero.mulArchimedean_iff {α} [OrderedCommGroup α] :
    MulArchimedean (WithZero α) ↔ MulArchimedean α

Proof state:
case mp
α : Type u_2
inst✝ : OrderedCommGroup α
a✝ : MulArchimedean (WithZero α)
⊢ MulArchimedean α

Tactic:
exact OrderMonoidIso.unitsWithZero.mulArchimedean

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OrderedCommGroup α
⊢ MulArchimedean (WithZero α) ↔ MulArchimedean α

Tactic:
constructor <;> intro _

Result:
case mp
α : Type u_2
inst✝ : OrderedCommGroup α
a✝ : MulArchimedean (WithZero α)
⊢ MulArchimedean α

case mpr
α : Type u_2
inst✝ : OrderedCommGroup α
a✝ : MulArchimedean α
⊢ MulArchimedean (WithZero α)

Proof state:
case mpr
α : Type u_2
inst✝ : OrderedCommGroup α
a✝ : MulArchimedean α
⊢ MulArchimedean (WithZero α)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem pow_mono {f g : CircleDeg1Lift} (h : f ≤ g) (n : ℕ) : f ^ n ≤ g ^ n := fun x => by
  simp only [coe_pow, iterate_mono h n x]

Proof state:
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
x : ℝ
⊢ (f ^ n) x ≤ (g ^ n) x

Tactic:
simp only [coe_pow, iterate_mono h n x]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_lift_associator_inv {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) :
    lift f (lift g h) ≫ (α_ Y Z W).inv = lift (lift f g) h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
⊢ lift f (lift g h) ≫ (α_ Y Z W).inv = lift (lift f g) h

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem app_right_eq_ι_comp_snd (b) :
    K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.snd b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) =
    K.ι (J.snd b) ≫ I.snd b

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b

Tactic:
rw [← K.w (WalkingMulticospan.Hom.snd b)]

Result:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.snd b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) =
    K.ι (J.snd b) ≫ I.snd b
-- Mathlib/SetTheory/Game/Birthday.lean
theorem le_birthday : ∀ x : PGame, x ≤ x.birthday.toPGame
  | ⟨xl, _, xL, _⟩ =>
    le_def.2
      ⟨fun i =>
        Or.inl ⟨toLeftMovesToPGame ⟨_, birthday_moveLeft_lt i⟩, by simp [le_birthday (xL i)]⟩,
        isEmptyElim⟩

Proof state:
xl β✝ : Type u_1
xL : xl → PGame
a✝ : β✝ → PGame
i : (mk xl β✝ xL a✝).LeftMoves
⊢ (mk xl β✝ xL a✝).moveLeft i ≤
    (mk xl β✝ xL a✝).birthday.toPGame.moveLeft (toLeftMovesToPGame ⟨((mk xl β✝ xL a✝).moveLeft i).birthday, ⋯⟩)

Tactic:
simp [le_birthday (xL i)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem morphismRestrict_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V W e) :
    (f ∣_ U).appLE V W e = f.appLE (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W)
      ((Set.image_subset _ e).trans (image_morphismRestrict_preimage f U V).le)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
W : (↑(f ⁻¹ᵁ U)).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
⊢ Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯

Tactic:
rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map,
  Scheme.Hom.appLE_map]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_nonneg (hd : d ≤ 0) (n : ℤ√d) : 0 ≤ n.norm :=
  add_nonneg (mul_self_nonneg _)
    (by
      rw [mul_assoc, neg_mul_eq_neg_mul]
      exact mul_nonneg (neg_nonneg.2 hd) (mul_self_nonneg _))

Proof state:
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -d * (n.im * n.im)

Tactic:
exact mul_nonneg (neg_nonneg.2 hd) (mul_self_nonneg _)

Result:
no goals

Proof state:
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -(d * n.im * n.im)

Tactic:
rw [mul_assoc, neg_mul_eq_neg_mul]

Result:
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -d * (n.im * n.im)
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma lt_rpow_of_log_lt (hy : 0 < y) (h : log x < z * log y) : x < y ^ z

Proof state:
case inl
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : x ≤ 0
⊢ x < y ^ z

Tactic:
exact hx.trans_lt (rpow_pos_of_pos hy _)

Result:
no goals

Proof state:
x y z : ℝ
hy : 0 < y
h : log x < z * log y
⊢ x < y ^ z

Tactic:
obtain hx | hx := le_or_lt x 0

Result:
case inl
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : x ≤ 0
⊢ x < y ^ z

case inr
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z

Proof state:
case inr
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z

Tactic:
exact (lt_rpow_iff_log_lt hx hy).2 h

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Projective.lean
lemma measure_cylinder (h : IsProjectiveLimit μ P)
    (I : Finset ι) {s : Set (∀ i : I, α i)} (hs : MeasurableSet s) :
    μ (cylinder I s) = P I s

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit μ P
I : Finset ι
s : Set ((i : { x // x ∈ I }) → α ↑i)
hs : MeasurableSet s
⊢ μ (cylinder I s) = (P I) s

Tactic:
rw [cylinder, ← Measure.map_apply _ hs, h I]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit μ P
I : Finset ι
s : Set ((i : { x // x ∈ I }) → α ↑i)
hs : MeasurableSet s
⊢ Measurable I.restrict

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit μ P
I : Finset ι
s : Set ((i : { x // x ∈ I }) → α ↑i)
hs : MeasurableSet s
⊢ Measurable I.restrict

Tactic:
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Result:
no goals