harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
    (rupHints : Array Nat) (i : Fin rupHints.size)
    (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
    (ih : ∃ hsize : acc.1.size = n, DerivedLitsInvariant f f_assignments_size acc.1 hsize acc.2.1) :
    let rupHint_res := (confirmRupHint f.clauses) acc rupHints[i]
    ∃ hsize : rupHint_res.1.size = n, DerivedLitsInvariant f f_assignments_size rupHint_res.1 hsize rupHint_res.2.1

Proof state:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.DerivedLitsInvariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).snd.fst

Tactic:
simp only [h, ite_false]

Result:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.DerivedLitsInvariant f_assignments_size
    (if false = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).fst
    ⋯
    (if false = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).snd.fst
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
    (rupHints : Array Nat) (i : Fin rupHints.size)
    (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
    (ih : ∃ hsize : acc.1.size = n, DerivedLitsInvariant f f_assignments_size acc.1 hsize acc.2.1) :
    let rupHint_res := (confirmRupHint f.clauses) acc rupHints[i]
    ∃ hsize : rupHint_res.1.size = n, DerivedLitsInvariant f f_assignments_size rupHint_res.1 hsize rupHint_res.2.1

Proof state:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.DerivedLitsInvariant f_assignments_size
    (if false = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).fst
    ⋯
    (if false = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).snd.fst

Tactic:
exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
⊢ none = none ∨ none = some none ∨ ∃ c, none = some (some c)

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
⊢ ReduceResult.reducedToUnit l = ReduceResult.encounteredBoth ∨
    ReduceResult.reducedToUnit l = ReduceResult.reducedToEmpty ∨
      (∃ l_1, ReduceResult.reducedToUnit l = ReduceResult.reducedToUnit l_1) ∨
        ReduceResult.reducedToUnit l = ReduceResult.reducedToNonunit

Tactic:
exact (Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro l) rfl

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem Topology.IsEmbedding.completelyNormalSpace [TopologicalSpace Y] [CompletelyNormalSpace Y]
    {e : X → Y} (he : IsEmbedding e) : CompletelyNormalSpace X

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (closure (e '' s)) (e '' t)

Tactic:
rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
  ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
⊢ CompletelyNormalSpace X

Tactic:
refine ⟨fun s t hd₁ hd₂ => ?_⟩

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
simp only [he.isInducing.nhdsSet_eq_comap]

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))

Tactic:
refine disjoint_comap (completely_normal ?_ ?_)

Result:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (closure (e '' s)) (e '' t)

case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (e '' s) (closure (e '' t))

Proof state:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (e '' s) (closure (e '' t))

Tactic:
rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl,
  ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right]

Result:
no goals
-- Mathlib/Order/InitialSeg.lean
theorem isMin_apply_iff [PartialOrder α] (f : α ≤i β) : IsMin (f a) ↔ IsMin a

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsMin a
x : α
hb : x ≤ a
⊢ a ≤ x

Tactic:
exact h hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ IsMin (f a) ↔ IsMin a

Tactic:
refine ⟨StrictMono.isMin_of_apply f.strictMono, fun h b hb ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsMin a
b : β
hb : b ≤ f a
⊢ f a ≤ b

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsMin a
x : α
hb : f x ≤ f a
⊢ f a ≤ f x

Tactic:
rw [f.le_iff_le] at hb ⊢

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsMin a
x : α
hb : x ≤ a
⊢ a ≤ x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsMin a
b : β
hb : b ≤ f a
⊢ f a ≤ b

Tactic:
obtain ⟨x, rfl⟩ := f.mem_range_of_le hb

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : IsMin a
x : α
hb : f x ≤ f a
⊢ f a ≤ f x
-- Mathlib/LinearAlgebra/Projection.lean
theorem ofIsCompl_eq (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F}
    (hφ : ∀ u, φ u = χ u) (hψ : ∀ u, ψ u = χ u) : ofIsCompl h φ ψ = χ

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
⊢ ofIsCompl h φ ψ = χ

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
x : E
⊢ (ofIsCompl h φ ψ) x = χ x

Proof state:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
x : E
⊢ (ofIsCompl h φ ψ) x = χ x

Tactic:
obtain ⟨_, _, rfl, _⟩ := existsUnique_add_of_isCompl h x

Result:
case h.intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
w✝¹ : ↥p
w✝ : ↥q
right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = ↑w✝¹ + ↑w✝ → r = w✝¹ ∧ s = w✝
⊢ (ofIsCompl h φ ψ) (↑w✝¹ + ↑w✝) = χ (↑w✝¹ + ↑w✝)

Proof state:
case h.intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
w✝¹ : ↥p
w✝ : ↥q
right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = ↑w✝¹ + ↑w✝ → r = w✝¹ ∧ s = w✝
⊢ (ofIsCompl h φ ψ) (↑w✝¹ + ↑w✝) = χ (↑w✝¹ + ↑w✝)

Tactic:
simp [ofIsCompl, hφ, hψ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_add_erase (p : R[X]) (n : ℕ) : monomial n (coeff p n) + p.erase n = p :=
  toFinsupp_injective <| by
    rcases p with ⟨⟩
    rw [toFinsupp_add, toFinsupp_monomial, toFinsupp_erase, coeff]
    exact Finsupp.single_add_erase _ _

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ ((monomial n) ({ toFinsupp := toFinsupp✝ }.coeff n) + erase n { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝ }.toFinsupp

Tactic:
rw [toFinsupp_add, toFinsupp_monomial, toFinsupp_erase, coeff]

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ Finsupp.single n (toFinsupp✝ n) + Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp =
    { toFinsupp := toFinsupp✝ }.toFinsupp

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ Finsupp.single n (toFinsupp✝ n) + Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp =
    { toFinsupp := toFinsupp✝ }.toFinsupp

Tactic:
exact Finsupp.single_add_erase _ _

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ((monomial n) (p.coeff n) + erase n p).toFinsupp = p.toFinsupp

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ ((monomial n) ({ toFinsupp := toFinsupp✝ }.coeff n) + erase n { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝ }.toFinsupp
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
theorem zip_decl_eq {aig : AIG α} (target : ZipTarget aig len) :
    ∀ idx (h1 : idx < aig.decls.size) (h2),
      (zip aig target).1.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : ZipTarget aig len
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (zip aig target).aig.decls.size
⊢ (zip aig target).aig.decls[idx✝] = aig.decls[idx✝]

Tactic:
unfold zip

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : ZipTarget aig len
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (zip aig target).aig.decls.size
⊢ (zip.go aig 0 empty ⋯ target.input.lhs target.input.rhs target.func).aig.decls[idx✝] = aig.decls[idx✝]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : ZipTarget aig len
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (zip aig target).aig.decls.size
⊢ (zip.go aig 0 empty ⋯ target.input.lhs target.input.rhs target.func).aig.decls[idx✝] = aig.decls[idx✝]

Tactic:
apply zip.go_decl_eq

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : ZipTarget aig len
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (zip aig target).aig.decls.size),
    (zip aig target).aig.decls[idx] = aig.decls[idx]

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : ZipTarget aig len
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (zip aig target).aig.decls.size
⊢ (zip aig target).aig.decls[idx✝] = aig.decls[idx✝]
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem adjoin_le_subfield {K : Subfield E} (HF : Set.range (algebraMap F E) ⊆ K) (HS : S ⊆ K) :
    (adjoin F S).toSubfield ≤ K

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ⇑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ Set.range ⇑(algebraMap F E) ∪ S ⊆ ↑K

Tactic:
rw [Set.union_subset_iff]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ⇑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑K ∧ S ⊆ ↑K

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ⇑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑K ∧ S ⊆ ↑K

Tactic:
exact ⟨HF, HS⟩

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ⇑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ (adjoin F S).toSubfield ≤ K

Tactic:
apply Subfield.closure_le.mpr

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ⇑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ Set.range ⇑(algebraMap F E) ∪ S ⊆ ↑K
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem isProbabilityMeasure_map {f : α → β} (hf : AEMeasurable f μ) :
    IsProbabilityMeasure (map f μ) :=
  ⟨by simp [map_apply_of_aemeasurable, hf]⟩

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ (Measure.map f μ) univ = 1

Tactic:
simp [map_apply_of_aemeasurable, hf]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem res_mk_eq_mk_pullback {Y X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} (x : Meq P S) (f : Y ⟶ X) :
    (J.plusObj P).map f.op (mk x) = mk (x.pullback f)

Proof state:
case h.a
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (Meq.equiv P (S.pullback f)) ((ConcreteCategory.hom ((J.diagramPullback P f).app (op S))) ((Meq.equiv P S).symm x)) =
    (Meq.equiv P (S.pullback f)) ((Meq.equiv P (S.pullback f)).symm (x.pullback f))

Tactic:
rw [Equiv.apply_symm_apply]

Result:
case h.a
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (Meq.equiv P (S.pullback f)) ((ConcreteCategory.hom ((J.diagramPullback P f).app (op S))) ((Meq.equiv P S).symm x)) =
    x.pullback f

Proof state:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((J.diagramPullback P f).app (op S))) ((Meq.equiv P S).symm x) =
    (Meq.equiv P (S.pullback f)).symm (x.pullback f)

Tactic:
apply (Meq.equiv P _).injective

Result:
case h.a
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (Meq.equiv P (unop ((J.pullback f).op.obj (op S))))
      ((ConcreteCategory.hom ((J.diagramPullback P f).app (op S))) ((Meq.equiv P S).symm x)) =
    (Meq.equiv P (unop ((J.pullback f).op.obj (op S)))) ((Meq.equiv P (S.pullback f)).symm (x.pullback f))
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
lemma not_isNontrivial_iff (v : AbsoluteValue R S) :
    ¬ v.IsNontrivial ↔ ∀ x ≠ 0, v x = 1

Proof state:
R : Type u_5
inst✝¹ : Semiring R
S : Type u_6
inst✝ : OrderedSemiring S
v : AbsoluteValue R S
⊢ ¬v.IsNontrivial ↔ ∀ (x : R), x ≠ 0 → v x = 1

Tactic:
simp only [IsNontrivial]

Result:
R : Type u_5
inst✝¹ : Semiring R
S : Type u_6
inst✝ : OrderedSemiring S
v : AbsoluteValue R S
⊢ (¬∃ x, x ≠ 0 ∧ v x ≠ 1) ↔ ∀ (x : R), x ≠ 0 → v x = 1

Proof state:
R : Type u_5
inst✝¹ : Semiring R
S : Type u_6
inst✝ : OrderedSemiring S
v : AbsoluteValue R S
⊢ (¬∃ x, x ≠ 0 ∧ v x ≠ 1) ↔ ∀ (x : R), x ≠ 0 → v x = 1

Tactic:
push_neg

Result:
R : Type u_5
inst✝¹ : Semiring R
S : Type u_6
inst✝ : OrderedSemiring S
v : AbsoluteValue R S
⊢ (∀ (x : R), x ≠ 0 → v x = 1) ↔ ∀ (x : R), x ≠ 0 → v x = 1

Proof state:
R : Type u_5
inst✝¹ : Semiring R
S : Type u_6
inst✝ : OrderedSemiring S
v : AbsoluteValue R S
⊢ (∀ (x : R), x ≠ 0 → v x = 1) ↔ ∀ (x : R), x ≠ 0 → v x = 1

Tactic:
rfl

Result:
no goals