harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {g : M → X}
    {s : Set M} {x : M} :
    ContinuousWithinAt (g ∘ (f.extend I).symm) ((f.extend I).symm ⁻¹' s ∩ range I) (f.extend I x) ↔
      ContinuousWithinAt (g ∘ f.symm) (f.symm ⁻¹' s) (f x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
X : Type u_8
inst✝ : TopologicalSpace X
g : M → X
s : Set M
x : M
⊢ ContinuousWithinAt (g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ range ↑I) (↑(f.extend I) x) ↔
    ContinuousWithinAt ((g ∘ ↑f.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' (↑f.symm ⁻¹' s) ∩ range ↑I) (↑I (↑f x))

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
X : Type u_8
inst✝ : TopologicalSpace X
g : M → X
s : Set M
x : M
⊢ ContinuousWithinAt (g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ range ↑I) (↑(f.extend I) x) ↔
    ContinuousWithinAt (g ∘ ↑f.symm) (↑f.symm ⁻¹' s) (↑f x)

Tactic:
rw [← I.symm_continuousWithinAt_comp_right_iff]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
X : Type u_8
inst✝ : TopologicalSpace X
g : M → X
s : Set M
x : M
⊢ ContinuousWithinAt (g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ range ↑I) (↑(f.extend I) x) ↔
    ContinuousWithinAt ((g ∘ ↑f.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' (↑f.symm ⁻¹' s) ∩ range ↑I) (↑I (↑f x))
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem exists_boundary_dart {u v : V} (p : G.Walk u v) (S : Set V) (uS : u ∈ S) (vS : v ∉ S) :
    ∃ d : G.Dart, d ∈ p.darts ∧ d.fst ∈ S ∧ d.snd ∉ S

Proof state:
case pos
V : Type u
G : SimpleGraph V
u v : V
S : Set V
x y w : V
a : G.Adj x y
p' : G.Walk y w
ih : y ∈ S → w ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : x ∈ S
vS : w ∉ S
h : y ∈ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
obtain ⟨d, hd, hcd⟩ := ih h vS

Result:
case pos.intro.intro
V : Type u
G : SimpleGraph V
u v : V
S : Set V
x y w : V
a : G.Adj x y
p' : G.Walk y w
ih : y ∈ S → w ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : x ∈ S
vS : w ∉ S
h : y ∈ S
d : G.Dart
hd : d ∈ p'.darts
hcd : d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Proof state:
case neg
V : Type u
G : SimpleGraph V
u v : V
S : Set V
x y w : V
a : G.Adj x y
p' : G.Walk y w
ih : y ∈ S → w ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : x ∈ S
vS : w ∉ S
h : y ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
exact ⟨⟨(x, y), a⟩, List.Mem.head _, uS, h⟩

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u✝ : V
uS : u✝ ∈ S
vS : u✝ ∉ S
⊢ ∃ d ∈ nil.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
cases vS uS

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u✝ v✝ w✝ : V
a : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : v✝ ∈ S → w✝ ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u✝ ∈ S
vS : w✝ ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
rename_i x y w

Result:
case cons
V : Type u
G : SimpleGraph V
u v : V
S : Set V
x y w : V
a : G.Adj x y
p' : G.Walk y w
ih : y ∈ S → w ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : x ∈ S
vS : w ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Proof state:
case pos.intro.intro
V : Type u
G : SimpleGraph V
u v : V
S : Set V
x y w : V
a : G.Adj x y
p' : G.Walk y w
ih : y ∈ S → w ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : x ∈ S
vS : w ∉ S
h : y ∈ S
d : G.Dart
hd : d ∈ p'.darts
hcd : d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
exact ⟨d, List.Mem.tail _ hd, hcd⟩

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
S : Set V
x y w : V
a : G.Adj x y
p' : G.Walk y w
ih : y ∈ S → w ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : x ∈ S
vS : w ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
by_cases h : y ∈ S

Result:
case pos
V : Type u
G : SimpleGraph V
u v : V
S : Set V
x y w : V
a : G.Adj x y
p' : G.Walk y w
ih : y ∈ S → w ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : x ∈ S
vS : w ∉ S
h : y ∈ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

case neg
V : Type u
G : SimpleGraph V
u v : V
S : Set V
x y w : V
a : G.Adj x y
p' : G.Walk y w
ih : y ∈ S → w ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : x ∈ S
vS : w ∉ S
h : y ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
-- Mathlib/Logic/Basic.lean
theorem lawful_beq_subsingleton {α : Type*} (inst1 : BEq α) (inst2 : BEq α)
    [@LawfulBEq α inst1] [@LawfulBEq α inst2] :
    inst1 = inst2

Proof state:
case h
α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
x y : α
⊢ (x == y) = (x == y)

Tactic:
simp only [beq_eq_decide]

Result:
no goals

Proof state:
case h
α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
⊢ ∀ (x y : α), (x == y) = (x == y)

Tactic:
intro x y

Result:
case h
α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
x y : α
⊢ (x == y) = (x == y)

Proof state:
α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
⊢ inst1 = inst2

Tactic:
apply beq_ext

Result:
case h
α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
⊢ ∀ (x y : α), (x == y) = (x == y)
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem sup_pow_eq_top {n : ℕ} (h : I ⊔ J = ⊤) : I ⊔ J ^ n = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n : ℕ
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ n = ⊤

Tactic:
rw [← Finset.card_range n, ← Finset.prod_const]

Result:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n : ℕ
h : I ⊔ J = ⊤
⊢ I ⊔ ∏ _x ∈ Finset.range n, J = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n : ℕ
h : I ⊔ J = ⊤
⊢ I ⊔ ∏ _x ∈ Finset.range n, J = ⊤

Tactic:
exact sup_prod_eq_top fun _ _ => h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_add_C {a : R} : (p + C a).natDegree = p.natDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : (C a).natDegree < p.natDegree
⊢ (p + C a).natDegree = p.natDegree

Tactic:
exact natDegree_add_eq_left_of_natDegree_lt hpd

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : ¬p.degree ≤ 0
⊢ (p + C a).natDegree = p.natDegree

Tactic:
rw [not_le, degree_eq_natDegree hp, Nat.cast_pos, ← natDegree_C a] at hpd

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : (C a).natDegree < p.natDegree
⊢ (p + C a).natDegree = p.natDegree

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
⊢ (p + C a).natDegree = p.natDegree

Tactic:
rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]

Result:
no goals

Proof state:
case inl
R : Type u
inst✝ : Semiring R
a : R
⊢ (0 + C a).natDegree = natDegree 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
⊢ (p + C a).natDegree = p.natDegree

Tactic:
by_cases hpd : p.degree ≤ 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
⊢ (p + C a).natDegree = p.natDegree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : ¬p.degree ≤ 0
⊢ (p + C a).natDegree = p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
⊢ (p + C a).natDegree = p.natDegree

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Result:
case inl
R : Type u
inst✝ : Semiring R
a : R
⊢ (0 + C a).natDegree = natDegree 0

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
⊢ (p + C a).natDegree = p.natDegree
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma add_half_inf_sub_mem_Ioo {l u v : ℝ} (hv : v ∈ Set.Ioo l u) :
    v + ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

Proof state:
case bc
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ (v - l) ⊓ (u - v) ≤ u - v

Tactic:
exact inf_le_right

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ 0 < (v - l) ⊓ (u - v)

Tactic:
positivity

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v + ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

Tactic:
constructor

Result:
case left
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ l < v + ((v - l) ⊓ (u - v)) / 2

case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v + ((v - l) ⊓ (u - v)) / 2 < u

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
⊢ 0 < (v - l) ⊓ (u - v)

Tactic:
simp [hv.1, hv.2]

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v + (u - v) = u

Tactic:
abel

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v + ((v - l) ⊓ (u - v)) / 2 < v + (v - l) ⊓ (u - v)

Tactic:
gcongr

Result:
case bc
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ ((v - l) ⊓ (u - v)) / 2 < (v - l) ⊓ (u - v)

Proof state:
case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v + ((v - l) ⊓ (u - v)) / 2 < u

Tactic:
calc v + ((v - l) ⊓ (u - v)) / 2
_ < v + ((v - l) ⊓ (u - v)) := by gcongr; exact half_lt_self (by positivity)
_ ≤ v + (u - v) := by gcongr; exact inf_le_right
_ = u := by abel

Result:
no goals

Proof state:
case left
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ l < v + ((v - l) ⊓ (u - v)) / 2

Tactic:
calc l < v := hv.1
_ ≤ v + ((v - l) ⊓ (u - v)) / 2 := le_add_of_nonneg_right (by positivity)

Result:
no goals

Proof state:
case bc
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ ((v - l) ⊓ (u - v)) / 2 < (v - l) ⊓ (u - v)

Tactic:
exact half_lt_self (by positivity)

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
⊢ v + ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

Tactic:
have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hv.1, hv.2]

Result:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v + ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ 0 ≤ ((v - l) ⊓ (u - v)) / 2

Tactic:
positivity

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v + (v - l) ⊓ (u - v) ≤ v + (u - v)

Tactic:
gcongr

Result:
case bc
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ (v - l) ⊓ (u - v) ≤ u - v
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_def' : normSq a = a.1 ^ 2 + a.2 ^ 2 + a.3 ^ 2 + a.4 ^ 2

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2

Tactic:
simp only [normSq_def, sq, mul_neg, sub_neg_eq_add, mul_re, star_re, star_imI, star_imJ,
  star_imK]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_left_eq_arctan_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∡ p₃ p₁ p₂ = Real.arctan (dist p₃ p₂ / dist p₁ p₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
  angle_eq_arctan_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (left_ne_of_oangle_eq_pi_div_two h)]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem L1.setToFun_eq_setToL1 (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E) :
    setToFun μ T hT f = L1.setToL1 hT f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
⊢ setToFun μ T hT ↑↑f = (setToL1 hT) f

Tactic:
rw [setToFun_eq hT (L1.integrable_coeFn f), Integrable.toL1_coeFn]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
theorem adjoint_apply_of_dense (y : T†.domain) : T† y = adjointAux hT y

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : ↥T†.domain
⊢ (if hT : Dense ↑T.domain then adjointAux hT else 0) y = (adjointAux hT) y

Tactic:
simp only [hT, dif_pos, LinearMap.coe_mk]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : ↥T†.domain
⊢ ↑T† y = (adjointAux hT) y

Tactic:
classical
change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
simp only [hT, dif_pos, LinearMap.coe_mk]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : ↥T†.domain
⊢ ↑T† y = (adjointAux hT) y

Tactic:
change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : ↥T†.domain
⊢ (if hT : Dense ↑T.domain then adjointAux hT else 0) y = (adjointAux hT) y
-- Mathlib/Data/Analysis/Filter.lean
theorem ne_bot_iff {f : Filter α} (F : f.Realizer) : f ≠ ⊥ ↔ ∀ a : F.σ, (F.F a).Nonempty

Proof state:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, ¬(F.F.f x).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ≤ Realizer.bot.F.f b

Tactic:
simp only [Set.not_nonempty_iff_eq_empty]

Result:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, F.F.f x = ∅) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ≤ Realizer.bot.F.f b

Proof state:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty

Tactic:
rw [not_iff_comm, ← le_bot_iff, F.le_iff Realizer.bot, not_forall]

Result:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, ¬(F.F.f x).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ≤ Realizer.bot.F.f b

Proof state:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, F.F.f x = ∅) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ≤ Realizer.bot.F.f b

Tactic:
exact ⟨fun ⟨x, e⟩ _ ↦ ⟨x, le_of_eq e⟩, fun h ↦
  let ⟨x, h⟩ := h ()
  ⟨x, le_bot_iff.1 h⟩⟩

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem Associates.finprod_ne_zero (I : Ideal R) :
    Associates.mk (∏ᶠ v : HeightOneSpectrum R, v.maxPowDividing I) ≠ 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0

Tactic:
rw [Associates.mk_ne_zero, finprod_def]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
⊢ (if h : (mulSupport fun v => v.maxPowDividing I).Finite then ∏ i ∈ h.toFinset, i.maxPowDividing I else 1) ≠ 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
⊢ (if h : (mulSupport fun v => v.maxPowDividing I).Finite then ∏ i ∈ h.toFinset, i.maxPowDividing I else 1) ≠ 0

Tactic:
split_ifs

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : (mulSupport fun v => v.maxPowDividing I).Finite
⊢ ∏ v ∈ h✝.toFinset, v.maxPowDividing I ≠ 0

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : ¬(mulSupport fun v => v.maxPowDividing I).Finite
⊢ 1 ≠ 0

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : (mulSupport fun v => v.maxPowDividing I).Finite
v : HeightOneSpectrum R
a✝ : v ∈ h✝.toFinset
⊢ v.maxPowDividing I ≠ 0

Tactic:
apply pow_ne_zero _ v.ne_bot

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : (mulSupport fun v => v.maxPowDividing I).Finite
⊢ ∏ v ∈ h✝.toFinset, v.maxPowDividing I ≠ 0

Tactic:
rw [Finset.prod_ne_zero_iff]

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : (mulSupport fun v => v.maxPowDividing I).Finite
⊢ ∀ a ∈ h✝.toFinset, a.maxPowDividing I ≠ 0

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : (mulSupport fun v => v.maxPowDividing I).Finite
⊢ ∀ a ∈ h✝.toFinset, a.maxPowDividing I ≠ 0

Tactic:
intro v _

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : (mulSupport fun v => v.maxPowDividing I).Finite
v : HeightOneSpectrum R
a✝ : v ∈ h✝.toFinset
⊢ v.maxPowDividing I ≠ 0

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : ¬(mulSupport fun v => v.maxPowDividing I).Finite
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals
-- Mathlib/Data/Bool/Count.lean
theorem count_not_eq_count (hl : Chain' (· ≠ ·) l) (h2 : Even (length l)) (b : Bool) :
    count (!b) l = count b l

Proof state:
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : l.length % 2 = 1
⊢ count (!x) (x :: l) = count x (x :: l)

Tactic:
rw [count_cons_of_ne x.not_ne_self, hl.count_not, h2, count_cons_self]

Result:
no goals

Proof state:
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : l.length % 2 = 1
this : count (!x) (x :: l) = count x (x :: l)
⊢ count (!b) (x :: l) = count b (x :: l)

Tactic:
cases b <;> cases x <;>
revert this <;> simp only [Bool.not_false, Bool.not_true] <;> intro this <;>
(try exact this) <;> exact this.symm

Result:
no goals

Proof state:
case nil
b : Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) []
h2 : Even [].length
⊢ count (!b) [] = count b []

Tactic:
rfl

Result:
no goals

Proof state:
case true.true
l : List Bool
h2 : l.length % 2 = 1
hl : Chain' (fun x1 x2 => x1 ≠ x2) (true :: l)
this : count false (true :: l) = count true (true :: l)
⊢ count false (true :: l) = count true (true :: l)

Tactic:
try exact this

Result:
no goals

Proof state:
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : l.length % 2 = 1
⊢ count (!b) (x :: l) = count b (x :: l)

Tactic:
suffices count (!x) (x :: l) = count x (x :: l) by
  cases b <;> cases x <;>
  revert this <;> simp only [Bool.not_false, Bool.not_true] <;> intro this <;>
  (try exact this) <;> exact this.symm

Result:
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : l.length % 2 = 1
⊢ count (!x) (x :: l) = count x (x :: l)

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ count (!b) l = count b l

Tactic:
rcases l with - | ⟨x, l⟩

Result:
case nil
b : Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) []
h2 : Even [].length
⊢ count (!b) [] = count b []

case cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : Even (x :: l).length
⊢ count (!b) (x :: l) = count b (x :: l)

Proof state:
case true.true
l : List Bool
h2 : l.length % 2 = 1
hl : Chain' (fun x1 x2 => x1 ≠ x2) (true :: l)
this : count false (true :: l) = count true (true :: l)
⊢ count false (true :: l) = count true (true :: l)

Tactic:
exact this

Result:
no goals

Proof state:
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : Even (x :: l).length
⊢ count (!b) (x :: l) = count b (x :: l)

Tactic:
rw [length_cons, Nat.even_add_one, Nat.not_even_iff] at h2

Result:
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : l.length % 2 = 1
⊢ count (!b) (x :: l) = count b (x :: l)
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ico_intCast :
    Pairwise (Disjoint on fun n : ℤ => Ico (n : α) (n + 1))

Proof state:
α : Type u_1
inst✝ : OrderedRing α
⊢ Pairwise (Disjoint on fun n => Ico (↑n) (↑n + 1))

Tactic:
simpa only [zero_add] using pairwise_disjoint_Ico_add_intCast (0 : α)

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_ncard_insert (a : α) (s : Set α) : s.ncard ≤ (insert a s).ncard

Proof state:
α : Type u_1
a : α
s : Set α
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
classical
refine
  s.finite_or_infinite.elim (fun h ↦ ?_) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
rw [ncard_insert_eq_ite h]; split_ifs <;> simp

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
(rw [h.ncard]; exact Nat.zero_le _)

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Set α
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
refine
  s.finite_or_infinite.elim (fun h ↦ ?_) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))

Result:
α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ (insert a s).ncard

Proof state:
α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
rw [h.ncard]

Result:
α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ 0 ≤ (insert a s).ncard

Proof state:
α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
rw [ncard_insert_eq_ite h]

Result:
α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1

Proof state:
α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ 0 ≤ (insert a s).ncard

Tactic:
exact Nat.zero_le _

Result:
no goals