harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma induce_connected_of_patches {s : Set V} (u : V) (hu : u ∈ s)
    (patches : ∀ {v}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
                  (G.induce s').Reachable ⟨u, hu'⟩ ⟨v, hv'⟩) : (G.induce s).Connected

Proof state:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ ∃ v, ∀ (w : ↑s), (induce s G).Reachable v w

Tactic:
refine ⟨⟨u, hu⟩, ?_⟩

Result:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ ∀ (w : ↑s), (induce s G).Reachable ⟨u, hu⟩ w

Proof state:
case mk.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
v : V
hv : v ∈ s
sv : Set V
svs : sv ⊆ s
hu' : u ∈ sv
hv' : v ∈ sv
uv : (induce sv G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ (induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
exact uv.map (induceHomOfLE _ svs).toHom

Result:
no goals

Proof state:
case mk
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
v : V
hv : v ∈ s
⊢ (induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
obtain ⟨sv, svs, hu', hv', uv⟩ := patches hv

Result:
case mk.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
v : V
hv : v ∈ s
sv : Set V
svs : sv ⊆ s
hu' : u ∈ sv
hv' : v ∈ sv
uv : (induce sv G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ (induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩

Proof state:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ (induce s G).Connected

Tactic:
rw [connected_iff_exists_forall_reachable]

Result:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ ∃ v, ∀ (w : ↑s), (induce s G).Reachable v w

Proof state:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ ∀ (w : ↑s), (induce s G).Reachable ⟨u, hu⟩ w

Tactic:
rintro ⟨v, hv⟩

Result:
case mk
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
v : V
hv : v ∈ s
⊢ (induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩
-- Mathlib/Data/Rel.lean
theorem graph_comp {f : β → γ} {g : α → β} : graph (f ∘ g) = Rel.comp (graph g) (graph f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
⊢ graph (f ∘ g) = (graph g).comp (graph f)

Tactic:
ext x y

Result:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : α
y : γ
⊢ graph (f ∘ g) x y ↔ (graph g).comp (graph f) x y

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : α
y : γ
⊢ graph (f ∘ g) x y ↔ (graph g).comp (graph f) x y

Tactic:
simp [Rel.comp]

Result:
no goals
-- Mathlib/Computability/RegularExpressions.lean
theorem map_id : ∀ P : RegularExpression α, P.map id = P
  | 0 => rfl
  | 1 => rfl
  | char _ => rfl
  | R + S => by simp_rw [map, map_id]
  | R * S => by simp_rw [map, map_id]
  | star R => by simp_rw [map, map_id]

Proof state:
α : Type u_1
R S : RegularExpression α
⊢ map id (R * S) = R * S

Tactic:
simp_rw [map, map_id]

Result:
no goals

Proof state:
α : Type u_1
R : RegularExpression α
⊢ map id R.star = R.star

Tactic:
simp_rw [map, map_id]

Result:
no goals

Proof state:
α : Type u_1
R S : RegularExpression α
⊢ map id (R + S) = R + S

Tactic:
simp_rw [map, map_id]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem toNat_apply_of_lt_aleph0 {c : Cardinal.{u}} (h : c < ℵ₀) :
    toNat c = Classical.choose (lt_aleph0.1 h) :=
  Nat.cast_injective (R := Cardinal.{u}) <| by
    rw [cast_toNat_of_lt_aleph0 h, ← Classical.choose_spec (lt_aleph0.1 h)]

Proof state:
c : Cardinal.{u}
h : c < ℵ₀
⊢ ↑(toNat c) = ↑(Classical.choose ⋯)

Tactic:
rw [cast_toNat_of_lt_aleph0 h, ← Classical.choose_spec (lt_aleph0.1 h)]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem ghostFun_one : ghostFun (1 : 𝕎 R) = 1

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ WittVector.ghostFun 1 = 1

Tactic:
ghost_fun_tac 1, ![]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pred_min_pred : ∀ (x y), min (pred x) (pred y) = pred (min x y)
  | 0, _ => by simp only [Nat.pred_zero, Nat.zero_min]
  | _, 0 => by simp only [Nat.pred_zero, Nat.min_zero]
  | _+1, _+1 => by simp only [Nat.pred_succ, Nat.succ_min_succ]

Proof state:
x✝ : Nat
⊢ min (pred 0) x✝.pred = (min 0 x✝).pred

Tactic:
simp only [Nat.pred_zero, Nat.zero_min]

Result:
no goals

Proof state:
x✝ : Nat
⊢ min x✝.pred (pred 0) = (min x✝ 0).pred

Tactic:
simp only [Nat.pred_zero, Nat.min_zero]

Result:
no goals

Proof state:
n✝¹ n✝ : Nat
⊢ min (n✝¹ + 1).pred (n✝ + 1).pred = (min (n✝¹ + 1) (n✝ + 1)).pred

Tactic:
simp only [Nat.pred_succ, Nat.succ_min_succ]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem limitObjIsoLimitCompEvaluation_hom_π [HasLimitsOfShape J C] (F : J ⥤ K ⥤ C) (j : J)
    (k : K) :
    (limitObjIsoLimitCompEvaluation F k).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j =
      (limit.π F j).app k

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (preservesLimitIso ((evaluation K C).obj k) F).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j = (limit.π F j).app k

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (limitObjIsoLimitCompEvaluation F k).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j = (limit.π F j).app k

Tactic:
dsimp [limitObjIsoLimitCompEvaluation]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (preservesLimitIso ((evaluation K C).obj k) F).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j = (limit.π F j).app k
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_dif {p : Prop} [Decidable p] (f : p → M) :
    ∏ᶠ i, f i = if h : p then f h else 1

Proof state:
case neg
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
⊢ ∏ᶠ (i : p), f i = 1

Tactic:
haveI : IsEmpty p := ⟨h⟩

Result:
case neg
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
this : IsEmpty p
⊢ ∏ᶠ (i : p), f i = 1

Proof state:
case neg
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
this : IsEmpty p
⊢ ∏ᶠ (i : p), f i = 1

Tactic:
exact finprod_of_isEmpty f

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
⊢ ∏ᶠ (i : p), f i = if h : p then f h else 1

Tactic:
split_ifs with h

Result:
case pos
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : p
⊢ ∏ᶠ (i : p), f i = f h

case neg
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
⊢ ∏ᶠ (i : p), f i = 1

Proof state:
case pos
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : p
this : Unique p
⊢ ∏ᶠ (i : p), f i = f h

Tactic:
exact finprod_unique f

Result:
no goals

Proof state:
case pos
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : p
⊢ ∏ᶠ (i : p), f i = f h

Tactic:
haveI : Unique p := ⟨⟨h⟩, fun _ => rfl⟩

Result:
case pos
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : p
this : Unique p
⊢ ∏ᶠ (i : p), f i = f h
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma d_pOpcycles [K.HasHomology j] : K.d i j ≫ K.pOpcycles j = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.d i j ≫ K.pOpcycles j = 0

Tactic:
by_cases hij : c.Rel i j

Result:
case pos
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
hij : c.Rel i j
⊢ K.d i j ≫ K.pOpcycles j = 0

case neg
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
hij : ¬c.Rel i j
⊢ K.d i j ≫ K.pOpcycles j = 0

Proof state:
case neg
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
hij : ¬c.Rel i j
⊢ K.d i j ≫ K.pOpcycles j = 0

Tactic:
rw [K.shape _ _ hij, zero_comp]

Result:
no goals

Proof state:
case pos
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
hij : c.Rel i j
⊢ K.d i j ≫ K.pOpcycles j = 0

Tactic:
obtain rfl := c.prev_eq' hij

Result:
case pos
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
j : ι
inst✝¹ : K.HasHomology j
inst✝ : K.HasHomology (c.prev j)
hij : c.Rel (c.prev j) j
⊢ K.d (c.prev j) j ≫ K.pOpcycles j = 0

Proof state:
case pos
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
j : ι
inst✝¹ : K.HasHomology j
inst✝ : K.HasHomology (c.prev j)
hij : c.Rel (c.prev j) j
⊢ K.d (c.prev j) j ≫ K.pOpcycles j = 0

Tactic:
exact (K.sc j).f_pOpcycles

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem preVal_add (x y : ModP O p) :
    preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)

Proof state:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Tactic:
rw [hx0, zero_add]

Result:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x = 0
⊢ preVal K v O p y ≤ preVal K v O p 0 ⊔ preVal K v O p y

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Tactic:
by_cases hx0 : x = 0

Result:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Proof state:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : ¬y = 0
hxy0 : x + y = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Tactic:
rw [hxy0, preVal_zero]

Result:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : ¬y = 0
hxy0 : x + y = 0
⊢ 0 ≤ preVal K v O p x ⊔ preVal K v O p y
-- Mathlib/Data/Set/Card.lean
theorem encard_pair {x y : α} (hne : x ≠ y) : ({x, y} : Set α).encard = 2

Proof state:
α : Type u_1
x y : α
hne : x ≠ y
⊢ {x, y}.encard = 2

Tactic:
rw [encard_insert_of_not_mem (by simpa), ← one_add_one_eq_two,
  WithTop.add_right_inj WithTop.one_ne_top, encard_singleton]

Result:
no goals

Proof state:
α : Type u_1
x y : α
hne : x ≠ y
⊢ x ∉ {y}

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.erase_aux [DecidableRel (α := α) (· ≤ ·)] (x : α) {t a₁ a₂} (h : Valid' a₁ t a₂) :
    Valid' a₁ (erase x t) a₂ ∧ Raised (erase x t).size t.size

Proof state:
case node.intro.intro.gt.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Raised (erase x t_r).size t_r.size ∧ BalancedSz t_l.size t_r.size

Tactic:
exact And.intro t_r_size h.bal.1

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem rfindOpt {n} {f : List.Vector ℕ (n + 1) → ℕ} (hf : @Partrec' (n + 1) f) :
    @Partrec' n fun v => Nat.rfindOpt fun a => ofNat (Option ℕ) (f (a ::ᵥ v)) :=
  ((rfind <|
        (of_prim (Primrec.nat_sub.comp (_root_.Primrec.const 1) Primrec.vector_head)).comp₁
          (fun n => Part.some (1 - n)) hf).bind
    ((prim Nat.Primrec'.pred).comp₁ Nat.pred hf)).of_eq
    fun v =>
    Part.ext fun b => by
      simp only [Nat.rfindOpt, exists_prop, Nat.sub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff,
        Part.mem_some_iff, Option.mem_def, Part.mem_coe]
      refine
        exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)
      · congr
        funext n
        cases f (n ::ᵥ v) <;> simp [Nat.succ_le_succ] <;> rfl
      · have := Nat.rfind_spec h
        simp only [Part.coe_some, Part.mem_some_iff] at this
        revert this; rcases f (a ::ᵥ v) with - | c <;> intro this
        · cases this
        rw [← Option.some_inj, eq_comm]
        rfl

Proof state:
case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
have := Nat.rfind_spec h

Result:
case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
this : true ∈ ↑(some (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome)
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma absolutelyContinuous_of_compProd [SFinite μ] [IsSFiniteKernel κ] [h_zero : ∀ a, NeZero (κ a)]
    (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
    μ ≪ ν

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a => (κ a) univ) =ᶠ[ae (μ.restrict s)] 0
⊢ μ s = 0

Tactic:
by_contra hμs

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a => (κ a) univ) =ᶠ[ae (μ.restrict s)] 0
hμs : ¬μ s = 0
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_add (θ₁ θ₂ : Real.Angle) : sin (θ₁ + θ₂) = sin θ₁ * cos θ₂ + cos θ₁ * sin θ₂

Proof state:
case h
θ₂ : Angle
x✝ : ℝ
⊢ (↑x✝ + θ₂).sin = (↑x✝).sin * θ₂.cos + (↑x✝).cos * θ₂.sin

Tactic:
induction θ₂ using Real.Angle.induction_on

Result:
case h.h
x✝¹ x✝ : ℝ
⊢ (↑x✝¹ + ↑x✝).sin = (↑x✝¹).sin * (↑x✝).cos + (↑x✝¹).cos * (↑x✝).sin

Proof state:
case h.h
x✝¹ x✝ : ℝ
⊢ (↑x✝¹ + ↑x✝).sin = (↑x✝¹).sin * (↑x✝).cos + (↑x✝¹).cos * (↑x✝).sin

Tactic:
exact Real.sin_add _ _

Result:
no goals

Proof state:
θ₁ θ₂ : Angle
⊢ (θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin

Tactic:
induction θ₁ using Real.Angle.induction_on

Result:
case h
θ₂ : Angle
x✝ : ℝ
⊢ (↑x✝ + θ₂).sin = (↑x✝).sin * θ₂.cos + (↑x✝).cos * θ₂.sin
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
theorem toReal_lintegral_coe_eq_integral [OpensMeasurableSpace X] (f : X →ᵇ ℝ≥0) (μ : Measure X) :
    (∫⁻ x, (f x : ℝ≥0∞) ∂μ).toReal = ∫ x, (f x : ℝ) ∂μ

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ 0 ≤ᶠ[ae μ] fun x => ↑(f x)

Tactic:
exact Eventually.of_forall (by simp only [Pi.zero_apply, NNReal.zero_le_coe, imp_true_iff])

Result:
no goals

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = (∫⁻ (a : X), ENNReal.ofReal ↑(f a) ∂μ).toReal

Tactic:
simp only [ENNReal.ofReal_coe_nnreal]

Result:
no goals

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = ∫ (x : X), ↑(f x) ∂μ

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae _ (by simpa [Function.comp_apply] using
      (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable)]

Result:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = (∫⁻ (a : X), ENNReal.ofReal ↑(f a) ∂μ).toReal

X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ 0 ≤ᶠ[ae μ] fun x => ↑(f x)

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ AEStronglyMeasurable (fun x => ↑(f x)) μ

Tactic:
simpa [Function.comp_apply] using
(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable

Result:
no goals

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ ∀ (x : X), 0 x ≤ (fun x => ↑(f x)) x

Tactic:
simp only [Pi.zero_apply, NNReal.zero_le_coe, imp_true_iff]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
/-- The interior of `M × N` is the product of the interiors of `M` and `N`. -/
lemma interior_prod :
    (I.prod J).interior (M × N) = (I.interior M) ×ˢ (J.interior N)

Proof state:
case h.mp
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : p ∈ ModelWithCorners.interior (M × N)
⊢ p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N

Tactic:
replace hp : (I.prod J).IsInteriorPoint p := hp

Result:
case h.mp
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : (I.prod J).IsInteriorPoint p
⊢ p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N

Proof state:
case h.mpr
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N
h : p.1 ∈ {x | I.IsInteriorPoint x} ∧ p.2 ∈ ModelWithCorners.interior N
⊢ (↑(extChartAt (I.prod J) p) p).1 ∈ interior (range ↑I) ∧ (↑(extChartAt (I.prod J) p) p).2 ∈ interior (range ↑J)

Tactic:
exact h

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem degree_of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.toPoly.degree ≤ 1

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ P.toPoly.degree ≤ 1

Tactic:
simpa only [of_b_eq_zero ha hb] using degree_linear_le

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem mem_supported : p ∈ supported R s ↔ ↑p.vars ⊆ s

Proof state:
case mpr
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ ↑p.vars ⊆ s → ∃ x, (rename Subtype.val) x = p

Tactic:
intro hs

Result:
case mpr
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
hs : ↑p.vars ⊆ s
⊢ ∃ x, (rename Subtype.val) x = p

Proof state:
case mp
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ (∃ x, (rename Subtype.val) x = p) → ↑p.vars ⊆ s

Tactic:
rintro ⟨p, rfl⟩

Result:
case mp.intro
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑((rename Subtype.val) p).vars ⊆ s

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
hs : ↑p.vars ⊆ s
⊢ ↑p.vars ⊆ Set.range Subtype.val

Tactic:
simpa

Result:
no goals

Proof state:
case mp.intro
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(Finset.image Subtype.val p.vars) ⊆ s

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ p ∈ supported R s ↔ ↑p.vars ⊆ s

Tactic:
rw [supported_eq_range_rename, AlgHom.mem_range]

Result:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ (∃ x, (rename Subtype.val) x = p) ↔ ↑p.vars ⊆ s

Proof state:
case mp.intro
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑((rename Subtype.val) p).vars ⊆ s

Tactic:
refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_

Result:
case mp.intro
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(Finset.image Subtype.val p.vars) ⊆ s

Proof state:
case mpr
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
hs : ↑p.vars ⊆ s
⊢ ∃ x, (rename Subtype.val) x = p

Tactic:
exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)

Result:
no goals

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ (∃ x, (rename Subtype.val) x = p) ↔ ↑p.vars ⊆ s

Tactic:
constructor

Result:
case mp
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ (∃ x, (rename Subtype.val) x = p) → ↑p.vars ⊆ s

case mpr
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ ↑p.vars ⊆ s → ∃ x, (rename Subtype.val) x = p