harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_add (a b : α) : |a + b| ≤ |a| + |b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |a + b| ≤ |a| + |b|

Tactic:
rw [abs_le, neg_add]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ -|a| + -|b| ≤ a + b ∧ a + b ≤ |a| + |b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ -|a| + -|b| ≤ a + b ∧ a + b ≤ |a| + |b|

Tactic:
constructor <;> gcongr <;> apply_rules [neg_abs_le, le_abs_self]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Center.lean
theorem leftUnitor_inv_f (X : Center C) : Hom.f (λ_ X).inv = (λ_ X.1).inv

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (λ_ X).inv.f = (λ_ X.fst).inv

Tactic:
apply Iso.inv_ext'

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (λ_ X.fst).hom ≫ (λ_ X).inv.f = 𝟙 (𝟙_ (Center C) ⊗ X).fst

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (𝟙 (𝟙_ (Center C) ⊗ X)).f = 𝟙 (𝟙_ (Center C) ⊗ X).fst

Tactic:
rfl

Result:
no goals

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (λ_ X.fst).hom ≫ (λ_ X).inv.f = 𝟙 (𝟙_ (Center C) ⊗ X).fst

Tactic:
rw [← leftUnitor_hom_f, ← comp_f, Iso.hom_inv_id]

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (𝟙 (𝟙_ (Center C) ⊗ X)).f = 𝟙 (𝟙_ (Center C) ⊗ X).fst
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesSummable.of_smul {f : ℕ → ℂ} {c s : ℂ} (hc : c ≠ 0) (hf : LSeriesSummable (c • f) s) :
    LSeriesSummable f s

Proof state:
f : ℕ → ℂ
c s : ℂ
hc : c ≠ 0
hf : LSeriesSummable (c • f) s
⊢ LSeriesSummable f s

Tactic:
simpa [hc] using hf.smul (c⁻¹)

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem mono_inl_of_isColimit [Mono g] {s : PushoutCocone f g} (hs : IsColimit s) : Mono s.inl

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
s : PushoutCocone f g
hs : IsColimit s
⊢ Mono s.inl

Tactic:
haveI : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.left) :=
  Abelian.mono_pushout_of_mono_g f g

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
s : PushoutCocone f g
hs : IsColimit s
this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.left)
⊢ Mono s.inl

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
s : PushoutCocone f g
hs : IsColimit s
this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.left)
⊢ Mono s.inl

Tactic:
apply
  mono_of_mono_fac (IsColimit.comp_coconePointUniqueUpToIso_hom hs (colimit.isColimit _) _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_eq_foldl_reverse (l : List α) (f : α → β → β) (b) :
    l.foldr f b = l.reverse.foldl (fun x y => f y x) b

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
b : β
⊢ foldr f b l = foldl (fun x y => f y x) b l.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem Algebra.IsAlgebraic.perfectField {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L] [PerfectField K] : PerfectField L := ⟨fun {f} hf ↦ by
  obtain ⟨_, _, hi, h⟩ := hf.exists_dvd_monic_irreducible_of_isIntegral (K := K)
  exact (PerfectField.separable_of_irreducible hi).map |>.of_dvd h⟩

Proof state:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : PerfectField K
f : L[X]
hf : Irreducible f
⊢ f.Separable

Tactic:
obtain ⟨_, _, hi, h⟩ := hf.exists_dvd_monic_irreducible_of_isIntegral (K := K)

Result:
case intro.intro.intro
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : PerfectField K
f : L[X]
hf : Irreducible f
w✝ : K[X]
left✝ : w✝.Monic
hi : Irreducible w✝
h : f ∣ map (algebraMap K L) w✝
⊢ f.Separable

Proof state:
case intro.intro.intro
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : PerfectField K
f : L[X]
hf : Irreducible f
w✝ : K[X]
left✝ : w✝.Monic
hi : Irreducible w✝
h : f ∣ map (algebraMap K L) w✝
⊢ f.Separable

Tactic:
exact (PerfectField.separable_of_irreducible hi).map |>.of_dvd h

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.openSegment_interior_closure_subset_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E}
    (hx : x ∈ interior s) (hy : y ∈ closure s) : openSegment 𝕜 x y ⊆ interior s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ closure s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
rintro _ ⟨a, b, ha, hb, hab, rfl⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ closure s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ closure s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
exact hs.combo_interior_closure_mem_interior hx hy ha hb.le hab

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_comp_lTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (f.rTensor Q).comp (g.lTensor M) = map f g

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ rTensor Q f ∘ₗ lTensor M g = map f g

Tactic:
simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem append_assoc {u v w x : V} (p : G.Walk u v) (q : G.Walk v w) (r : G.Walk w x) :
    p.append (q.append r) = (p.append q).append r

Proof state:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk w x
⊢ p.append (q.append r) = (p.append q).append r

Tactic:
induction p with
| nil => rw [nil_append, nil_append]
| cons h p' ih => rw [cons_append, cons_append, cons_append, ih]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ : V
q : G.Walk u✝ w
⊢ nil.append (q.append r) = (nil.append q).append r

Tactic:
rw [nil_append, nil_append]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (q : G.Walk w✝ w), p'.append (q.append r) = (p'.append q).append r
q : G.Walk w✝ w
⊢ (cons h p').append (q.append r) = ((cons h p').append q).append r

Tactic:
rw [cons_append, cons_append, cons_append, ih]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem init_snoc : init (snoc p x) = p

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ p (i.castSucc.castLT ⋯) = p i

Tactic:
convert cast_eq rfl (p i)

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
⊢ init (snoc p x) = p

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ init (snoc p x) i = p i

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ init (snoc p x) i = p i

Tactic:
simp only [init, snoc, coe_castSucc, is_lt, cast_eq, dite_true]

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ p (i.castSucc.castLT ⋯) = p i
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.inf (hf : ωScottContinuous f) (hg : ωScottContinuous g) :
    ωScottContinuous (f ⊓ g)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (f ⊓ g) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := f ⊓ g, monotone' := ⋯ }) ≤ a

Tactic:
simp only [Pi.inf_apply, hf.map_ωSup c, hg.map_ωSup c, inf_le_iff, ωSup_le_iff, Chain.map_coe,
  Function.comp, OrderHom.coe_mk, ← forall_or_left, ← forall_or_right]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (∀ (x x_1 : ℕ), f (c x_1) ≤ a ∨ g (c x) ≤ a) ↔ ∀ (i : ℕ), f (c i) ≤ a ∨ g (c i) ≤ a

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (∀ (x x_1 : ℕ), f (c x_1) ≤ a ∨ g (c x) ≤ a) ↔ ∀ (i : ℕ), f (c i) ≤ a ∨ g (c i) ≤ a

Tactic:
exact ⟨fun h _ ↦ h _ _, fun h i j ↦
  (h (max j i)).imp (le_trans <| hf.monotone <| c.mono <| le_max_left _ _)
    (le_trans <| hg.monotone <| c.mono <| le_max_right _ _)⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (f ⊓ g)

Tactic:
refine ωScottContinuous.of_monotone_map_ωSup
  ⟨hf.monotone.inf hg.monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩

Result:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (f ⊓ g) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := f ⊓ g, monotone' := ⋯ }) ≤ a
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_eq_prod' {s : Finset β} (hf : mulSupport f ⊆ s) :
    ∏' b, f b = ∏ b ∈ s, f b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
s : Finset β
hf : mulSupport f ⊆ ↑s
⊢ ∏' (b : β), f b = ∏ b ∈ s, f b

Tactic:
rw [tprod_eq_finprod (s.finite_toSet.subset hf), finprod_eq_prod_of_mulSupport_subset _ hf]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLinearMapRight'_one :
    Matrix.toLinearMapRight' (1 : Matrix m m R) = LinearMap.id

Proof state:
R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
⊢ toLinearMapRight' 1 = LinearMap.id

Tactic:
ext

Result:
case h.h.h
R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
i✝ x✝ : m
⊢ (toLinearMapRight' 1 ∘ₗ single R (fun i => R) i✝) 1 x✝ = (LinearMap.id ∘ₗ single R (fun i => R) i✝) 1 x✝

Proof state:
case h.h.h
R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
i✝ x✝ : m
⊢ (toLinearMapRight' 1 ∘ₗ single R (fun i => R) i✝) 1 x✝ = (LinearMap.id ∘ₗ single R (fun i => R) i✝) 1 x✝

Tactic:
simp [LinearMap.one_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem mkAndCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
    {h2} :
    (aig.mkAndCached input).aig.decls[idx]'h2 = aig.decls[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkAndCached input).aig.decls.size
⊢ (aig.mkAndCached input).aig.decls[idx] = aig.decls[idx]

Tactic:
simp only [mkAndCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkAndCached input).aig.decls.size
⊢ (aig.mkGateCached (input.asGateInput false false)).aig.decls[idx] = aig.decls[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkAndCached input).aig.decls.size
⊢ (aig.mkGateCached (input.asGateInput false false)).aig.decls[idx] = aig.decls[idx]

Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem tail_think (s : WSeq α) : tail (think s) = (tail s).think

Proof state:
α : Type u
s : WSeq α
⊢ s.think.tail = s.tail.think

Tactic:
simp [tail]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem of_nat {n : ℕ} : padicValRat p n = padicValNat p n

Proof state:
p n : ℕ
⊢ padicValRat p ↑n = ↑(padicValNat p n)

Tactic:
simp [padicValRat]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem dist_inv_inv₀ {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) :
    dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)

Proof state:
α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)

Tactic:
rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
  mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.move_right_left {Γ} [Inhabited Γ] (T : Tape Γ) :
    (T.move Dir.right).move Dir.left = T

Proof state:
case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ move Dir.left (move Dir.right { head := head✝, left := left✝, right := right✝ }) =
    { head := head✝, left := left✝, right := right✝ }

Tactic:
simp [Tape.move]

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ move Dir.left (move Dir.right T) = T

Tactic:
cases T

Result:
case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ move Dir.left (move Dir.right { head := head✝, left := left✝, right := right✝ }) =
    { head := head✝, left := left✝, right := right✝ }
-- Mathlib/RingTheory/Smooth/Kaehler.lean
theorem Algebra.FormallySmooth.iff_injective_and_projective' :
    letI : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra
    Algebra.FormallySmooth R S ↔
        Function.Injective (kerCotangentToTensor R (MvPolynomial S R) S) ∧
        Module.Projective S (Ω[S⁄R])

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ FormallySmooth R S ↔ Function.Injective ⇑(kerCotangentToTensor R (MvPolynomial S R) S) ∧ Module.Projective S (Ω[S⁄R])

Tactic:
letI : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
this : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra
⊢ FormallySmooth R S ↔ Function.Injective ⇑(kerCotangentToTensor R (MvPolynomial S R) S) ∧ Module.Projective S (Ω[S⁄R])

Proof state:
case hs
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
this✝ : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra
this : Surjective ⇑(algebraMap (MvPolynomial S R) S)
⊢ Surjective ⇑(mapBaseChange R (MvPolynomial S R) S)

Tactic:
exact KaehlerDifferential.mapBaseChange_surjective _ _ _ this

Result:
no goals

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
this : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra
⊢ FormallySmooth R S ↔ Function.Injective ⇑(kerCotangentToTensor R (MvPolynomial S R) S) ∧ Module.Projective S (Ω[S⁄R])

Tactic:
have : Function.Surjective (algebraMap (MvPolynomial S R) S) :=
  fun x ↦ ⟨.X x, MvPolynomial.aeval_X _ _⟩

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
this✝ : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra
this : Surjective ⇑(algebraMap (MvPolynomial S R) S)
⊢ FormallySmooth R S ↔ Function.Injective ⇑(kerCotangentToTensor R (MvPolynomial S R) S) ∧ Module.Projective S (Ω[S⁄R])

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
this✝ : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra
this : Surjective ⇑(algebraMap (MvPolynomial S R) S)
⊢ FormallySmooth R S ↔ Function.Injective ⇑(kerCotangentToTensor R (MvPolynomial S R) S) ∧ Module.Projective S (Ω[S⁄R])

Tactic:
rw [Algebra.FormallySmooth.iff_injective_and_split this,
  ← Module.Projective.iff_split_of_projective]

Result:
case hs
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
this✝ : Algebra (MvPolynomial S R) S := (MvPolynomial.aeval _root_.id).toAlgebra
this : Surjective ⇑(algebraMap (MvPolynomial S R) S)
⊢ Surjective ⇑(mapBaseChange R (MvPolynomial S R) S)
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_add_le (a b : α) : fract (a + b) ≤ fract a + fract b

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

Tactic:
exact le_floor_add _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ fract (a + b) ≤ fract a + fract b

Tactic:
rw [fract, fract, fract, sub_add_sub_comm, sub_le_sub_iff_left, ← Int.cast_add, Int.cast_le]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma map_prod_map {α' : Type*} [MeasurableSpace α'] {β' : Type*} [MeasurableSpace β']
    {f : α → α'} {g : β → β'} (f_mble : Measurable f) (g_mble : Measurable g) :
    (μ.map f_mble.aemeasurable).prod (ν.map g_mble.aemeasurable)
      = (μ.prod ν).map (f_mble.prod_map g_mble).aemeasurable

Proof state:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ ↑((μ.map ⋯).prod (ν.map ⋯)) = ↑((μ.prod ν).map ⋯)

Tactic:
simp only [val_eq_to_measure, toMeasure_prod, toMeasure_map]

Result:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (Measure.map f ↑μ).prod (Measure.map g ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (μ.map ⋯).prod (ν.map ⋯) = (μ.prod ν).map ⋯

Tactic:
apply Subtype.ext

Result:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ ↑((μ.map ⋯).prod (ν.map ⋯)) = ↑((μ.prod ν).map ⋯)

Proof state:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (Measure.map f ↑μ).prod (Measure.map g ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)

Tactic:
rw [Measure.map_prod_map _ _ f_mble g_mble]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma iInf_eq_zero_iff {ι : Sort*} {f : ι → Cardinal} :
    (⨅ i, f i) = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0

Proof state:
ι : Sort u_1
f : ι → Cardinal.{u_2}
⊢ ⨅ i, f i = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0

Tactic:
simp [iInf, sInf_eq_zero_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_and_epi_g_iff_of_iso (e : S₁ ≅ S₂) :
    S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g

Tactic:
have : Epi S₁.g ↔ Epi S₂.g :=
  (MorphismProperty.epimorphisms C).arrow_mk_iso_iff
    (Arrow.isoMk (ShortComplex.π₂.mapIso e) (ShortComplex.π₃.mapIso e) e.hom.comm₂₃)

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
this : Epi S₁.g ↔ Epi S₂.g
⊢ S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
this : Epi S₁.g ↔ Epi S₂.g
⊢ S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g

Tactic:
rw [exact_iff_of_iso e, this]

Result:
no goals
-- Mathlib/RingTheory/FinitePresentation.lean
theorem of_surjective (f : A →ₐ[R] B) (hf : Surjective f) (hker : f.toRingHom.ker.FG) :
    f.FinitePresentation

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
hker : (RingHom.ker f.toRingHom).FG
⊢ f.FinitePresentation

Tactic:
convert RingHom.FinitePresentation.of_surjective f hf hker

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem ext_of_Ioc' {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α}
    [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α]
    (μ ν : Measure α) (hμ : ∀ ⦃a b⦄, a < b → μ (Ioc a b) ≠ ∞)
    (h : ∀ ⦃a b⦄, a < b → μ (Ioc a b) = ν (Ioc a b)) : μ = ν

Proof state:
case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ⊤
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) ≠ ⊤

case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ⊤
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) = ν (⇑OrderDual.ofDual ⁻¹' Ioc b a)

Tactic:
exacts [hμ hab, h hab]

Result:
no goals

Proof state:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ⊤
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
⊢ μ = ν

Tactic:
refine @ext_of_Ico' αᵒᵈ _ _ _ _ _ ‹_› _ μ ν ?_ ?_ <;> intro a b hab <;> erw [dual_Ico (α := α)]

Result:
case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ⊤
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) ≠ ⊤

case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ⊤
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) = ν (⇑OrderDual.ofDual ⁻¹' Ioc b a)