harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp [Finite V]
    {c : G.ConnectedComponent} (h : G.IsCycles) (hv : v ∈ c.supp)
    (hn : (G.neighborSet v).Nonempty) :
    ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
⊢ ∃ p, p.IsCycle ∧ p.toSubgraph.verts = c.supp

Tactic:
obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
  ⟨hw, h.reachable_deleteEdges hw⟩

Result:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
⊢ ∃ p, p.IsCycle ∧ p.toSubgraph.verts = c.supp

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
⊢ (p.rotate hvp).toSubgraph.verts = p.toSubgraph.verts

Tactic:
simp_all

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ p.toSubgraph.Adj v w

Tactic:
refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj

Result:
V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ ↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v)

Proof state:
V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ Nonempty (↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v))

Tactic:
rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
  h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem disjoint_nil_right (l : List α) : Disjoint l []

Proof state:
α : Type u_1
l : List α
⊢ l.Disjoint []

Tactic:
rw [disjoint_comm]

Result:
α : Type u_1
l : List α
⊢ [].Disjoint l

Proof state:
α : Type u_1
l : List α
⊢ [].Disjoint l

Tactic:
exact disjoint_nil_left _

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem list_get?₁ : ∀ l : List α, Primrec l.get?
  | [] => dom_denumerable.2 zero
  | a :: l =>
    dom_denumerable.2 <|
      (casesOn1 (encode a).succ <| dom_denumerable.1 <| list_get?₁ l).of_eq fun n => by
        cases n <;> simp

Proof state:
α : Type u_1
inst✝ : Primcodable α
a : α
l : List α
n : ℕ
⊢ (Nat.casesOn n (encode a).succ fun n => encode (l.get? (ofNat ℕ n))) = encode ((a :: l).get? (ofNat ℕ n))

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) :
    l[i] = l.reverse[l.length - 1 - i]'(by simpa using Nat.sub_one_sub_lt_of_lt h)

Proof state:
α : Type ?u.5176
l : List α
i : Nat
h : i < l.length
⊢ l.length - 1 - i < l.reverse.length

Tactic:
simpa using Nat.sub_one_sub_lt_of_lt h

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ l[i] = l.reverse[l.length - 1 - i]

Tactic:
rw [getElem_reverse]

Result:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ l[i] = l[l.length - 1 - (l.length - 1 - i)]

Proof state:
case e_i
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ i = l.length - 1 - (l.length - 1 - i)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ l[i] = l[l.length - 1 - (l.length - 1 - i)]

Tactic:
congr

Result:
case e_i
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ i = l.length - 1 - (l.length - 1 - i)
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc]
lemma liftCycles_leftHomologyπ_eq_zero_of_boundary (x : A ⟶ S.X₁) (hx : k = x ≫ S.f) :
    S.liftCycles k (by rw [hx, assoc, S.zero, comp_zero]) ≫ S.leftHomologyπ = 0 :=
  LeftHomologyData.liftK_π_eq_zero_of_boundary _ k x hx

Proof state:
C : Type u_1
inst✝² : Category.{?u.207993, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ k ≫ S.g = 0

Tactic:
rw [hx, assoc, S.zero, comp_zero]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_lt_ncard (h : s ⊂ t) (ht : t.Finite

Proof state:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : autoParam t.Finite _auto✝
⊢ s.encard < t.encard

Tactic:
exact ht.encard_lt_encard h

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : autoParam t.Finite _auto✝
⊢ s.ncard < t.ncard

Tactic:
rw [← Nat.cast_lt (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h.subset).cast_ncard_eq]

Result:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : autoParam t.Finite _auto✝
⊢ s.encard < t.encard
-- Mathlib/Probability/Process/Adapted.lean
theorem adapted (h : ProgMeasurable f u) : Adapted f u

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
i : ι
this : u i = (fun p => u (↑p.1) p.2) ∘ fun x => (⟨i, ⋯⟩, x)
⊢ StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun x => (⟨i, ⋯⟩, x))

Tactic:
exact (h i).comp_measurable measurable_prod_mk_left

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
i : ι
this : u i = (fun p => u (↑p.1) p.2) ∘ fun x => (⟨i, ⋯⟩, x)
⊢ StronglyMeasurable (u i)

Tactic:
rw [this]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
i : ι
this : u i = (fun p => u (↑p.1) p.2) ∘ fun x => (⟨i, ⋯⟩, x)
⊢ StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun x => (⟨i, ⋯⟩, x))

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
⊢ Adapted f u

Tactic:
intro i

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
i : ι
⊢ StronglyMeasurable (u i)

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
i : ι
⊢ StronglyMeasurable (u i)

Tactic:
have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) :=
  rfl

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : TopologicalSpace β
inst✝¹ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝ : MeasurableSpace ι
h : ProgMeasurable f u
i : ι
this : u i = (fun p => u (↑p.1) p.2) ∘ fun x => (⟨i, ⋯⟩, x)
⊢ StronglyMeasurable (u i)
-- Mathlib/RingTheory/WittVector/Teichmuller.lean
theorem teichmuller_mul_aux₂ {R : Type*} (x y : MvPolynomial R ℤ) :
    teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℤ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Tactic:
refine map_injective (MvPolynomial.map (Int.castRingHom ℚ))
  (MvPolynomial.map_injective _ Int.cast_injective) ?_

Result:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℤ
⊢ (map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p (x * y)) =
    (map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p x * teichmullerFun p y)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℤ
⊢ (map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p (x * y)) =
    (map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p x * teichmullerFun p y)

Tactic:
simp only [teichmuller_mul_aux₁, map_teichmullerFun, RingHom.map_mul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem le_mex_of_forall {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal}
    (H : ∀ b < a, ∃ i, f i = b) : a ≤ mex.{_, v} f

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
a : Ordinal.{max u v}
H : ∀ b < a, ∃ i, f i = b
⊢ a ≤ mex f

Tactic:
by_contra! h

Result:
ι : Type u
f : ι → Ordinal.{max u v}
a : Ordinal.{max u v}
H : ∀ b < a, ∃ i, f i = b
h : mex f < a
⊢ False

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
a : Ordinal.{max u v}
H : ∀ b < a, ∃ i, f i = b
h : mex f < a
⊢ False

Tactic:
exact mex_not_mem_range f (H _ h)

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma ge_of_forall_gt_iff_ge : (∀ z : α, z < x → z ≤ y) ↔ x ≤ y

Proof state:
α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y

Tactic:
cases x <;> cases y <;> simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Result:
no goals
-- Mathlib/Order/Disjoint.lean
lemma Codisjoint.ne_bot_of_ne_top (h : Codisjoint a b) (ha : a ≠ ⊤) : b ≠ ⊥

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
a : α
ha : a ≠ ⊤
h : Codisjoint a ⊥
⊢ False

Tactic:
exact ha <| by simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
a : α
ha : a ≠ ⊤
h : Codisjoint a ⊥
⊢ a = ⊤

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
a b : α
h : Codisjoint a b
ha : a ≠ ⊤
⊢ b ≠ ⊥

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
a : α
ha : a ≠ ⊤
h : Codisjoint a ⊥
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forM_map [Monad m] [LawfulMonad m] (l : Vector α n) (g : α → β) (f : β → m PUnit) :
    forM (l.map g) f = forM l (fun a => f (g a))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_4
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
g : α → β
f : β → m PUnit
⊢ forM (map g l) f = forM l fun a => f (g a)

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_4
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
f : β → m PUnit
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ forM (map g { toArray := toArray✝, size_toArray := size_toArray✝ }) f =
    forM { toArray := toArray✝, size_toArray := size_toArray✝ } fun a => f (g a)

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_4
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
f : β → m PUnit
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ forM (map g { toArray := toArray✝, size_toArray := size_toArray✝ }) f =
    forM { toArray := toArray✝, size_toArray := size_toArray✝ } fun a => f (g a)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
lemma _root_.Function.HasTemperateGrowth.const (c : F) :
    Function.HasTemperateGrowth (fun _ : E ↦ c) :=
  .of_fderiv (by simpa using .zero) (differentiable_const c) (k := 0) (C := ‖c‖) (fun x ↦ by simp)

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
⊢ Function.HasTemperateGrowth (fderiv ℝ fun x => c)

Tactic:
simpa using .zero

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
x : E
⊢ ‖c‖ ≤ ‖c‖ * (1 + ‖x‖) ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
lemma arctan_add_arctan_lt_pi_div_two {x y : ℝ} (h : x * y < 1) : arctan x + arctan y < π / 2

Proof state:
case inr
x y : ℝ
h : x * y < 1
hy : 0 < y
⊢ arctan x + arctan y < π / 2

Tactic:
rw [← lt_div_iff₀ hy, ← inv_eq_one_div] at h

Result:
case inr
x y : ℝ
h : x < y⁻¹
hy : 0 < y
⊢ arctan x + arctan y < π / 2

Proof state:
case inr
x y : ℝ
h : x < y⁻¹
hy : 0 < y
⊢ arctan x + arctan y < π / 2

Tactic:
replace h : arctan x < arctan y⁻¹ := tanOrderIso.symm.strictMono h

Result:
case inr
x y : ℝ
hy : 0 < y
h : arctan x < arctan y⁻¹
⊢ arctan x + arctan y < π / 2

Proof state:
case inl
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2 + arctan 0

Tactic:
exact add_lt_add_of_lt_of_le (arctan_lt_pi_div_two _) (tanOrderIso.symm.monotone hy)

Result:
no goals

Proof state:
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Tactic:
rcases le_or_lt y 0 with hy | hy

Result:
case inl
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2

case inr
x y : ℝ
h : x * y < 1
hy : 0 < y
⊢ arctan x + arctan y < π / 2

Proof state:
case inr
x y : ℝ
hy : 0 < y
h : arctan x < arctan y⁻¹
⊢ arctan x + arctan y < π / 2

Tactic:
rwa [arctan_inv_of_pos hy, lt_tsub_iff_right] at h

Result:
no goals

Proof state:
case inl
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2

Tactic:
rw [← add_zero (π / 2), ← arctan_zero]

Result:
case inl
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2 + arctan 0
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
theorem IsInitial.epi_to {X Y : C} (t : IsInitial X) (f : Y ⟶ X) : Epi f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f : Y ⟶ X
⊢ Epi f

Tactic:
haveI := t.isSplitEpi_to f

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f : Y ⟶ X
this : IsSplitEpi f
⊢ Epi f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f : Y ⟶ X
this : IsSplitEpi f
⊢ Epi f

Tactic:
infer_instance

Result:
no goals
-- Mathlib/RingTheory/Localization/Ideal.lean
lemma mk'_mem_map_algebraMap_iff (I : Ideal R) (x : R) (s : M) :
    IsLocalization.mk' S x s ∈ I.map (algebraMap R S) ↔ ∃ s ∈ M, s * x ∈ I

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
I : Ideal R
x : R
s : ↥M
⊢ (∃ x_1 c, ↑(c * x_1.2) * x = ↑c * ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I

Tactic:
exact ⟨fun ⟨⟨y, t⟩, c, h⟩ ↦ ⟨_, (c * t).2, h ▸ I.mul_mem_left c.1 y.2⟩, fun ⟨s, hs, h⟩ ↦
  ⟨⟨⟨_, h⟩, ⟨s, hs⟩⟩, 1, by simp⟩⟩

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
I : Ideal R
x : R
s✝ : ↥M
x✝ : ∃ s ∈ M, s * x ∈ I
s : R
hs : s ∈ M
h : s * x ∈ I
⊢ ↑(1 * (⟨s * x, h⟩, ⟨s, hs⟩).2) * x = ↑1 * ↑(⟨s * x, h⟩, ⟨s, hs⟩).1

Tactic:
simp

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
I : Ideal R
x : R
s : ↥M
⊢ mk' S x s ∈ Ideal.map (algebraMap R S) I ↔ ∃ s ∈ M, s * x ∈ I

Tactic:
rw [← Ideal.unit_mul_mem_iff_mem _ (IsLocalization.map_units S s), IsLocalization.mk'_spec',
  IsLocalization.mem_map_algebraMap_iff M]

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
I : Ideal R
x : R
s : ↥M
⊢ (∃ x_1, (algebraMap R S) x * (algebraMap R S) ↑x_1.2 = (algebraMap R S) ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I

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
I : Ideal R
x : R
s : ↥M
⊢ (∃ x_1, (algebraMap R S) x * (algebraMap R S) ↑x_1.2 = (algebraMap R S) ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I

Tactic:
simp_rw [← map_mul, IsLocalization.eq_iff_exists M, mul_comm x, ← mul_assoc, ← Submonoid.coe_mul]

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
I : Ideal R
x : R
s : ↥M
⊢ (∃ x_1 c, ↑(c * x_1.2) * x = ↑c * ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.map_vadd_zmultiples [AddCommGroup α] (hf : Periodic f c)
    (a : AddSubgroup.zmultiples c) (x : α) : f (a +ᵥ x) = f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
hf : Periodic f c
a : ↥(AddSubgroup.zmultiples c)
x : α
⊢ f (a +ᵥ x) = f x

Tactic:
rcases a with ⟨_, m, rfl⟩

Result:
case mk.intro
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
hf : Periodic f c
x : α
m : ℤ
⊢ f (⟨(fun x => x • c) m, ⋯⟩ +ᵥ x) = f x

Proof state:
case mk.intro
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
hf : Periodic f c
x : α
m : ℤ
⊢ f (⟨(fun x => x • c) m, ⋯⟩ +ᵥ x) = f x

Tactic:
simp [AddSubgroup.vadd_def, add_comm _ x, hf.zsmul m x]

Result:
no goals
-- Mathlib/Order/Cofinal.lean
theorem isCofinal_setOf_imp_lt (r : α → α → Prop) [h : IsWellFounded α r] :
    IsCofinal { a | ∀ b, r b a → b < a }

Proof state:
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
⊢ IsCofinal {a | ∀ (b : α), r b a → b < a}

Tactic:
intro a

Result:
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a : α
⊢ ∃ y ∈ {a | ∀ (b : α), r b a → b < a}, a ≤ y

Proof state:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Set.Ici a
hb' : ∀ x ∈ Set.Ici a, ¬r x b
c : α
hc : r c b
⊢ c < b

Tactic:
by_contra! hc'

Result:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Set.Ici a
hb' : ∀ x ∈ Set.Ici a, ¬r x b
c : α
hc : r c b
hc' : b ≤ c
⊢ False

Proof state:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Set.Ici a
hb' : ∀ x ∈ Set.Ici a, ¬r x b
c : α
hc : r c b
hc' : b ≤ c
⊢ False

Tactic:
exact hb' c (hb.trans hc') hc

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Set.Ici a
hb' : ∀ x ∈ Set.Ici a, ¬r x b
⊢ ∃ y ∈ {a | ∀ (b : α), r b a → b < a}, a ≤ y

Tactic:
refine ⟨b, fun c hc ↦ ?_, hb⟩

Result:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Set.Ici a
hb' : ∀ x ∈ Set.Ici a, ¬r x b
c : α
hc : r c b
⊢ c < b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a : α
⊢ ∃ y ∈ {a | ∀ (b : α), r b a → b < a}, a ≤ y

Tactic:
obtain ⟨b, hb, hb'⟩ := h.wf.has_min (Set.Ici a) Set.nonempty_Ici

Result:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Set.Ici a
hb' : ∀ x ∈ Set.Ici a, ¬r x b
⊢ ∃ y ∈ {a | ∀ (b : α), r b a → b < a}, a ≤ y
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_pos [PosMulStrictMono G₀] (ha : 0 < a) (hb : 0 < b) : 0 < a / b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹

Tactic:
exact mul_pos ha (inv_pos.2 hb)

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a / b

Tactic:
rw [div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_fderiv {f : G → E} {x : G} :
    fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ fderivWithin 𝕜 (⇑iso ∘ f) univ x = (↑iso).comp (fderivWithin 𝕜 f univ x)

Tactic:
exact iso.comp_fderivWithin uniqueDiffWithinAt_univ

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ fderiv 𝕜 (⇑iso ∘ f) x = (↑iso).comp (fderiv 𝕜 f x)

Tactic:
rw [← fderivWithin_univ, ← fderivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ fderivWithin 𝕜 (⇑iso ∘ f) univ x = (↑iso).comp (fderivWithin 𝕜 f univ x)
-- Mathlib/LinearAlgebra/Span/Defs.lean
lemma exists_add_eq_of_codisjoint (h : Codisjoint p p') (x : M) :
    ∃ y ∈ p, ∃ z ∈ p', y + z = x

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : Codisjoint p p'
x : M
⊢ x ∈ p ⊔ p'

Tactic:
simpa only [h.eq_top] using Submodule.mem_top

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : Codisjoint p p'
x : M
this : x ∈ p ⊔ p'
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
exact Submodule.mem_sup.mp this

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : Codisjoint p p'
x : M
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
suffices x ∈ p ⊔ p' by exact Submodule.mem_sup.mp this

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : Codisjoint p p'
x : M
⊢ x ∈ p ⊔ p'
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem projectRightAssign_property :
    (projectRightAssign assign) x hx = (assign <| .inr ⟨x, hx⟩)

Proof state:
aig✝ : AIG Nat
assign : aig✝.CNFVar → Bool
x : Nat
hx : x < aig✝.decls.size
⊢ projectRightAssign assign x hx = assign (Sum.inr ⟨x, hx⟩)

Tactic:
simp [projectRightAssign]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma hasUnifEigenvalue_iff_mem_spectrum [FiniteDimensional K V] {f : End K V} {μ : K} :
    f.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker (f - μ • 1) = ⊥ ↔ LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥

Tactic:
simp [Submodule.ext_iff, LinearMap.mem_ker]

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ f.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f

Tactic:
rw [spectrum.mem_iff, IsUnit.sub_iff, LinearMap.isUnit_iff_ker_eq_bot,
  HasUnifEigenvalue, genEigenspace_one, ne_eq, not_iff_not]

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker (f - μ • 1) = ⊥ ↔ LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_eq_zero : dens s = 0 ↔ s = ∅

Proof state:
α : Type u_2
inst✝ : Fintype α
s : Finset α
⊢ s.dens = 0 ↔ s = ∅

Tactic:
simp +contextual [dens, Fintype.card_eq_zero_iff, eq_empty_of_isEmpty]

Result:
no goals