harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Localization/Submodule.lean
theorem isNoetherianRing (h : IsNoetherianRing R) : IsNoetherianRing S

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
h : WellFounded fun x1 x2 => x1 > x2
⊢ WellFounded fun x1 x2 => x1 > x2

Tactic:
exact OrderEmbedding.wellFounded (IsLocalization.orderEmbedding M S).dual h

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
h : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
rw [isNoetherianRing_iff, isNoetherian_iff] at h ⊢

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
h : WellFounded fun x1 x2 => x1 > x2
⊢ WellFounded fun x1 x2 => x1 > x2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem or_comm (x y : BitVec w) :
    x ||| y = y ||| x

Proof state:
w : Nat
x y : BitVec w
⊢ x ||| y = y ||| x

Tactic:
ext i

Result:
case pred
w : Nat
x y : BitVec w
i : Nat
a✝ : i < w
⊢ (x ||| y).getLsbD i = (y ||| x).getLsbD i

Proof state:
case pred
w : Nat
x y : BitVec w
i : Nat
a✝ : i < w
⊢ (x ||| y).getLsbD i = (y ||| x).getLsbD i

Tactic:
simp [Bool.or_comm]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
@[ext (iff := false)]
lemma ext {x y : RelSeries r} (length_eq : x.length = y.length)
    (toFun_eq : x.toFun = y.toFun ∘ Fin.cast (by rw [length_eq])) : x = y

Proof state:
α : Type u_1
r : Rel α α
β : Type u_2
s : Rel β β
x y : RelSeries r
length_eq : x.length = y.length
⊢ x.length + 1 = y.length + 1

Tactic:
rw [length_eq]

Result:
no goals

Proof state:
case mk
α : Type u_1
r : Rel α α
y : RelSeries r
nx : ℕ
fx : Fin (nx + 1) → α
step✝ : ∀ (i : Fin nx), r (fx i.castSucc) (fx i.succ)
length_eq : nx = y.length
toFun_eq : fx = y.toFun ∘ Fin.cast ⋯
⊢ { length := nx, toFun := fx, step := step✝ } = y

Tactic:
subst length_eq toFun_eq

Result:
case mk
α : Type u_1
r : Rel α α
y : RelSeries r
step✝ : ∀ (i : Fin y.length), r ((y.toFun ∘ Fin.cast ⋯) i.castSucc) ((y.toFun ∘ Fin.cast ⋯) i.succ)
⊢ { length := y.length, toFun := y.toFun ∘ Fin.cast ⋯, step := step✝ } = y

Proof state:
case mk
α : Type u_1
r : Rel α α
y : RelSeries r
nx : ℕ
fx : Fin (nx + 1) → α
step✝ : ∀ (i : Fin nx), r (fx i.castSucc) (fx i.succ)
length_eq : { length := nx, toFun := fx, step := step✝ }.length = y.length
toFun_eq : { length := nx, toFun := fx, step := step✝ }.toFun = y.toFun ∘ Fin.cast ⋯
⊢ { length := nx, toFun := fx, step := step✝ } = y

Tactic:
dsimp only at length_eq toFun_eq

Result:
case mk
α : Type u_1
r : Rel α α
y : RelSeries r
nx : ℕ
fx : Fin (nx + 1) → α
step✝ : ∀ (i : Fin nx), r (fx i.castSucc) (fx i.succ)
length_eq : nx = y.length
toFun_eq : fx = y.toFun ∘ Fin.cast ⋯
⊢ { length := nx, toFun := fx, step := step✝ } = y

Proof state:
α : Type u_1
r : Rel α α
x y : RelSeries r
length_eq : x.length = y.length
toFun_eq : x.toFun = y.toFun ∘ Fin.cast ⋯
⊢ x = y

Tactic:
rcases x with ⟨nx, fx⟩

Result:
case mk
α : Type u_1
r : Rel α α
y : RelSeries r
nx : ℕ
fx : Fin (nx + 1) → α
step✝ : ∀ (i : Fin nx), r (fx i.castSucc) (fx i.succ)
length_eq : { length := nx, toFun := fx, step := step✝ }.length = y.length
toFun_eq : { length := nx, toFun := fx, step := step✝ }.toFun = y.toFun ∘ Fin.cast ⋯
⊢ { length := nx, toFun := fx, step := step✝ } = y

Proof state:
case mk
α : Type u_1
r : Rel α α
y : RelSeries r
step✝ : ∀ (i : Fin y.length), r ((y.toFun ∘ Fin.cast ⋯) i.castSucc) ((y.toFun ∘ Fin.cast ⋯) i.succ)
⊢ { length := y.length, toFun := y.toFun ∘ Fin.cast ⋯, step := step✝ } = y

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem fdiv_eq_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → a.fdiv b = a / b
  | _, b, ⟨c, rfl⟩ => by
    by_cases bz : b = 0
    · simp [bz]
    · rw [mul_fdiv_cancel_left _ bz, mul_ediv_cancel_left _ bz]

Proof state:
case pos
b c : Int
bz : b = 0
⊢ (b * c).fdiv b = b * c / b

Tactic:
simp [bz]

Result:
no goals

Proof state:
case neg
b c : Int
bz : ¬b = 0
⊢ (b * c).fdiv b = b * c / b

Tactic:
rw [mul_fdiv_cancel_left _ bz, mul_ediv_cancel_left _ bz]

Result:
no goals

Proof state:
b c : Int
⊢ (b * c).fdiv b = b * c / b

Tactic:
by_cases bz : b = 0

Result:
case pos
b c : Int
bz : b = 0
⊢ (b * c).fdiv b = b * c / b

case neg
b c : Int
bz : ¬b = 0
⊢ (b * c).fdiv b = b * c / b
-- Mathlib/Geometry/Manifold/VectorField.lean
@[simp] lemma mpullbackWithin_univ : mpullbackWithin I I' f V univ = mpullback I I' f V

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
⊢ mpullbackWithin I I' f V univ = mpullback I I' f V

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
x : M
⊢ mpullbackWithin I I' f V univ x = mpullback I I' f V x

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
x : M
⊢ mpullbackWithin I I' f V univ x = mpullback I I' f V x

Tactic:
simp [mpullback_apply, mpullbackWithin_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
protected lemma map_add {K : Type v} [Field K] (f : F →+* K) {P Q : Fin 3 → F}
    (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
    (W.map f).toProjective.add (f ∘ P) (f ∘ Q) = f ∘ W.add P Q

Proof state:
case pos
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (map W f).toProjective.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]

Result:
no goals

Proof state:
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ (map W f).toProjective.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
by_cases h : P ≈ Q

Result:
case pos
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (map W f).toProjective.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

case neg
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (map W f).toProjective.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Proof state:
case neg
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (map W f).toProjective.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem mem_properDivisors {m : ℕ} : n ∈ properDivisors m ↔ n ∣ m ∧ n < m

Proof state:
n m : ℕ
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Result:
case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0

case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Proof state:
case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0

Tactic:
simp [properDivisors]

Result:
no goals

Proof state:
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Tactic:
simp only [and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma iSup_inf_eq (f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Proof state:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
rw [iSup, sSup_inf_eq, iSup_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_le_findIdx {l : Array α} {p q : α → Bool} (h : ∀ x ∈ l, p x → q x) : l.findIdx q ≤ l.findIdx p

Proof state:
α : Type u_1
l : Array α
p q : α → Bool
h : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ findIdx q l ≤ findIdx p l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p q : α → Bool
l : List α
h : ∀ (x : α), x ∈ { toList := l } → p x = true → q x = true
⊢ findIdx q { toList := l } ≤ findIdx p { toList := l }

Proof state:
case mk
α : Type u_1
p q : α → Bool
l : List α
h : ∀ (x : α), x ∈ { toList := l } → p x = true → q x = true
⊢ findIdx q { toList := l } ≤ findIdx p { toList := l }

Tactic:
simp_all [List.findIdx_le_findIdx]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem mul_eq_zero_iff_right (hb : b ≠ 0) : a * b = 0 ↔ a = 0

Proof state:
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
hb : b ≠ 0
⊢ a * b = 0 ↔ a = 0

Tactic:
simp [hb]

Result:
no goals
-- Mathlib/MeasureTheory/Function/Floor.lean
theorem Int.measurable_ceil [OpensMeasurableSpace R] : Measurable (Int.ceil : R → ℤ) :=
  measurable_to_countable fun x => by
    simpa only [Int.preimage_ceil_singleton] using measurableSet_Ioc

Proof state:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
x : R
⊢ MeasurableSet (ceil ⁻¹' {⌈x⌉})

Tactic:
simpa only [Int.preimage_ceil_singleton] using measurableSet_Ioc

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma mem_stabilizer_finset_iff_smul_finset_subset {s : Finset α} :
    a ∈ stabilizer G s ↔ a • s ⊆ s

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a ∈ stabilizer G s ↔ a • s ⊆ s

Tactic:
rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).ge]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@[simp] lemma eLpNorm_of_isEmpty [IsEmpty α] (f : α → E) (p : ℝ≥0∞) : eLpNorm f p μ = 0

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsEmpty α
f : α → E
p : ℝ≥0∞
⊢ eLpNorm f p μ = 0

Tactic:
simp [Subsingleton.elim f 0]

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem transpose_eq_diagonal [DecidableEq n] [Zero α] {M : Matrix n n α} {v : n → α} :
    Mᵀ = diagonal v ↔ M = diagonal v :=
  (Function.Involutive.eq_iff transpose_transpose).trans <|
    by rw [diagonal_transpose]

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
M : Matrix n n α
v : n → α
⊢ M = (diagonal v)ᵀ ↔ M = diagonal v

Tactic:
rw [diagonal_transpose]

Result:
no goals
-- Mathlib/GroupTheory/NoncommPiCoprod.lean
theorem noncommPiCoprod_range
    {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y} :
    (noncommPiCoprod hcomm).range = ⨆ i : ι, H i

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
⊢ (noncommPiCoprod hcomm).range = ⨆ i, H i

Tactic:
simp [noncommPiCoprod, MonoidHom.noncommPiCoprod_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
theorem unsat_of_bitblast (expr : BVLogicalExpr) : expr.bitblast.Unsat → expr.Unsat :=  by
  intro h assign
  rw [← denote_bitblast]
  apply h

Proof state:
expr : BVLogicalExpr
⊢ expr.bitblast.Unsat → expr.Unsat

Tactic:
intro h assign

Result:
expr : BVLogicalExpr
h : expr.bitblast.Unsat
assign : BVExpr.Assignment
⊢ eval assign expr = false

Proof state:
expr : BVLogicalExpr
h : expr.bitblast.Unsat
assign : BVExpr.Assignment
⊢ eval assign expr = false

Tactic:
rw [← denote_bitblast]

Result:
expr : BVLogicalExpr
h : expr.bitblast.Unsat
assign : BVExpr.Assignment
⊢ ⟦assign.toAIGAssignment, expr.bitblast⟧ = false

Proof state:
expr : BVLogicalExpr
h : expr.bitblast.Unsat
assign : BVExpr.Assignment
⊢ ⟦assign.toAIGAssignment, expr.bitblast⟧ = false

Tactic:
apply h

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem mem_and_mem_iff {x y : α} {z : Sym2 α} (hne : x ≠ y) : x ∈ z ∧ y ∈ z ↔ z = s(x, y)

Proof state:
case mpr
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ z = s(x, y) → x ∈ z ∧ y ∈ z

Tactic:
rintro rfl

Result:
case mpr
α : Type u_1
x y : α
hne : x ≠ y
⊢ x ∈ s(x, y) ∧ y ∈ s(x, y)

Proof state:
case mpr
α : Type u_1
x y : α
hne : x ≠ y
⊢ x ∈ s(x, y) ∧ y ∈ s(x, y)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z ↔ z = s(x, y)

Tactic:
constructor

Result:
case mp
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z → z = s(x, y)

case mpr
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ z = s(x, y) → x ∈ z ∧ y ∈ z

Proof state:
case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x' y' : α
⊢ x ∈ s(x', y') ∧ y ∈ s(x', y') → s(x', y') = s(x, y)

Tactic:
rw [mem_iff, mem_iff]

Result:
case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x' y' : α
⊢ (x = x' ∨ x = y') ∧ (y = x' ∨ y = y') → s(x', y') = s(x, y)

Proof state:
case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x' y' : α
⊢ (x = x' ∨ x = y') ∧ (y = x' ∨ y = y') → s(x', y') = s(x, y)

Tactic:
aesop

Result:
no goals

Proof state:
case mp
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z → z = s(x, y)

Tactic:
induction' z with x' y'

Result:
case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x' y' : α
⊢ x ∈ s(x', y') ∧ y ∈ s(x', y') → s(x', y') = s(x, y)
-- Mathlib/Topology/PartitionOfUnity.lean
theorem coe_finsupport (x₀ : X) :
    (ρ.finsupport x₀ : Set ι) = support fun i ↦ ρ i x₀

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ↑(ρ.finsupport x₀) = support fun i => (ρ i) x₀

Tactic:
ext

Result:
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
x✝ : ι
⊢ x✝ ∈ ↑(ρ.finsupport x₀) ↔ x✝ ∈ support fun i => (ρ i) x₀

Proof state:
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
x✝ : ι
⊢ x✝ ∈ ↑(ρ.finsupport x₀) ↔ x✝ ∈ support fun i => (ρ i) x₀

Tactic:
rw [Finset.mem_coe, mem_finsupport]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_coord_change_source_mem_nhdsWithin {x : E}
    (hx : x ∈ ((f.extend I).symm ≫ f'.extend I).source) :
    ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] x

Proof state:
case intro.intro
𝕜 : 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 f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : H
hx : x ∈ (f.symm ≫ₕ f').source
⊢ (f.symm ≫ₕ f').source ∈ 𝓝 x

Tactic:
exact (PartialHomeomorph.open_source _).mem_nhds hx

Result:
no goals

Proof state:
case intro.intro
𝕜 : 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 f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : H
hx : x ∈ (f.symm ≫ₕ f').source
⊢ ↑I '' (f.symm ≫ₕ f').source ∈ 𝓝[range ↑I] ↑I x

Tactic:
refine I.image_mem_nhdsWithin ?_

Result:
case intro.intro
𝕜 : 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 f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : H
hx : x ∈ (f.symm ≫ₕ f').source
⊢ (f.symm ≫ₕ f').source ∈ 𝓝 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 f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : E
hx : x ∈ ↑I '' (f.symm ≫ₕ f').source
⊢ ↑I '' (f.symm ≫ₕ f').source ∈ 𝓝[range ↑I] x

Tactic:
obtain ⟨x, hx, rfl⟩ := hx

Result:
case intro.intro
𝕜 : 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 f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : H
hx : x ∈ (f.symm ≫ₕ f').source
⊢ ↑I '' (f.symm ≫ₕ f').source ∈ 𝓝[range ↑I] ↑I 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 f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : E
hx : x ∈ ((f.extend I).symm ≫ f'.extend I).source
⊢ ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range ↑I] x

Tactic:
rw [f.extend_coord_change_source] at hx ⊢

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 f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : E
hx : x ∈ ↑I '' (f.symm ≫ₕ f').source
⊢ ↑I '' (f.symm ≫ₕ f').source ∈ 𝓝[range ↑I] x
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma indepFun_zero_right {β γ} [MeasurableSpace β] [MeasurableSpace γ]
    {f : Ω → β} {g : Ω → γ} : IndepFun f g κ 0

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
β : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
⊢ IndepFun f g κ 0

Tactic:
simp [IndepFun]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem insertP_cons_neg (p : α → Bool) (a b l) (h : ¬ p b) :
    insertP p a (b :: l) = b :: insertP p a l

Proof state:
α : Type u_1
p : α → Bool
a b : α
l : List α
h : ¬p b = true
⊢ insertP.loop p a l [b] = b :: insertP.loop p a l []

Tactic:
exact insertP_loop ..

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a b : α
l : List α
h : ¬p b = true
⊢ insertP p a (b :: l) = b :: insertP p a l

Tactic:
simp only [insertP, insertP.loop, cond, h]

Result:
α : Type u_1
p : α → Bool
a b : α
l : List α
h : ¬p b = true
⊢ insertP.loop p a l [b] = b :: insertP.loop p a l []
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_div' (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
    num (algebraMap _ _ p / algebraMap _ _ q) =
      Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Proof state:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num =
    C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Tactic:
rw [num, numDenom_div _ hq]

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccOrder.lean
lemma Iic.coe_succ_of_not_isMax
    [SuccOrder J] {j : J} {i : Set.Iic j} (hi : ¬ IsMax i) :
    (Order.succ i).1 = Order.succ i.1

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ ↑i ∈ Iic j

Tactic:
apply Order.succ_le_of_lt

Result:
case a
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑i < j

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑(Order.succ i) = Order.succ ↑i

Tactic:
rw [coe_succ_of_mem]

Result:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ ↑i ∈ Iic j

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ i ≠ ⊤

Tactic:
simpa using hi

Result:
no goals

Proof state:
case a
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑i < j

Tactic:
exact lt_of_le_of_ne (α := Set.Iic j) le_top (by simpa using hi)

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem inf_sdiff_eq_bot_iff (hz : z ≤ y) (hx : x ≤ y) : z ⊓ y \ x = ⊥ ↔ z ≤ x

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ Disjoint z (y \ x) ↔ z ≤ x

Tactic:
exact disjoint_sdiff_iff_le hz hx

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ z ⊓ y \ x = ⊥ ↔ z ≤ x

Tactic:
rw [← disjoint_iff]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ Disjoint z (y \ x) ↔ z ≤ x
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem ext_elem (h : IsAdjoinRootMonic S f) ⦃x y : S⦄
    (hxy : ∀ i < natDegree f, h.coeff x i = h.coeff y i) : x = y :=
  EquivLike.injective h.basis.equivFun <|
    funext fun i => by
      rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
        hxy i i.prop]

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i
i : Fin f.natDegree
⊢ h.basis.equivFun x i = h.basis.equivFun y i

Tactic:
rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
  hxy i i.prop]

Result:
no goals
-- Mathlib/Data/List/Dedup.lean
theorem replicate_dedup {x : α} : ∀ {k}, k ≠ 0 → (replicate k x).dedup = [x]
  | 0, h => (h rfl).elim
  | 1, _ => rfl
  | n + 2, _ => by
    rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
      replicate_dedup n.succ_ne_zero]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (replicate (n + 2) x).dedup = [x]

Tactic:
rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
  replicate_dedup n.succ_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_C_mul_X (a : R) : derivative (C a * X) = C a

Proof state:
R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a * X) = C a

Tactic:
simp [C_mul_X_eq_monomial, derivative_monomial, Nat.cast_one, mul_one]

Result:
no goals
-- Mathlib/Algebra/Regular/Basic.lean
theorem not_isRightRegular_zero_iff : ¬IsRightRegular (0 : R) ↔ Nontrivial R

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsRightRegular 0 ↔ Nontrivial R

Tactic:
rw [nontrivial_iff, not_iff_comm, isRightRegular_zero_iff_subsingleton, subsingleton_iff]

Result:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y

Tactic:
push_neg

Result:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y

Tactic:
exact Iff.rfl

Result:
no goals