harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsTopologicalGroup.exists_antitone_basis_nhds_one [FirstCountableTopology G] :
    ∃ u : ℕ → Set G, (𝓝 1).HasAntitoneBasis u ∧ ∀ n, u (n + 1) * u (n + 1) ⊆ u n

Proof state:
case intro.mk
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
⊢ ∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n

Tactic:
obtain ⟨φ, -, hφ, φ_anti_basis⟩ := HasAntitoneBasis.subbasis_with_rel ⟨hu, u_anti⟩ event_mul

Result:
case intro.mk.intro.intro.intro
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
φ : ℕ → ℕ
hφ : ∀ ⦃m n : ℕ⦄, m < n → u (φ n) * u (φ n) ⊆ u (φ m)
φ_anti_basis : (𝓝 1).HasAntitoneBasis (u ∘ φ)
⊢ ∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n

Proof state:
case intro.intro.intro
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (j ⊔ k)
⊢ u m * u m ⊆ u n

Tactic:
rintro - ⟨a, ha, b, hb, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (j ⊔ k)
a : G
ha : a ∈ u m
b : G
hb : b ∈ u m
⊢ (fun x1 x2 => x1 * x2) a b ∈ u n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_eq_neg_one_mul : ∀ a : Int, -a = -1 * a
  | 0      => rfl
  | succ n => show _ = -[1 * n +1] by rw [Nat.one_mul]; rfl
  | -[n+1] => show _ = ofNat _ by rw [Nat.one_mul]; rfl

Proof state:
n : Nat
⊢ -↑n.succ = -[n+1]

Tactic:
rfl

Result:
no goals

Proof state:
n : Nat
⊢ - -[n+1] = ofNat n.succ

Tactic:
rfl

Result:
no goals

Proof state:
n : Nat
⊢ - -[n+1] = ofNat (succ 0 * n.succ)

Tactic:
rw [Nat.one_mul]

Result:
n : Nat
⊢ - -[n+1] = ofNat n.succ

Proof state:
n : Nat
⊢ -↑n.succ = -[1 * n+1]

Tactic:
rw [Nat.one_mul]

Result:
n : Nat
⊢ -↑n.succ = -[n+1]
-- Mathlib/Data/List/Permutation.lean
theorem get_permutations'Aux (s : List α) (x : α) (n : ℕ)
    (hn : n < length (permutations'Aux x s)) :
    (permutations'Aux x s).get ⟨n, hn⟩ = s.insertIdx n x

Proof state:
α : Type u_1
s : List α
x : α
n : ℕ
hn : n < (permutations'Aux x s).length
⊢ (permutations'Aux x s).get ⟨n, hn⟩ = insertIdx n x s

Tactic:
simp [getElem_permutations'Aux]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem mul_int (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (x * m)

Proof state:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑↑m)

Tactic:
refine h.mul_rat ?_

Result:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0

Proof state:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0

Tactic:
rwa [Int.cast_ne_zero]

Result:
no goals

Proof state:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑m)

Tactic:
rw [← cast_intCast]

Result:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑↑m)
-- Mathlib/Order/ModularLattice.lean
theorem covBy_sup_of_inf_covBy_right : a ⊓ b ⋖ b → a ⋖ a ⊔ b

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ b → a ⋖ a ⊔ b

Tactic:
rw [sup_comm, inf_comm]

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ b → a ⋖ b ⊔ a

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ b → a ⋖ b ⊔ a

Tactic:
exact covBy_sup_of_inf_covBy_left

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem sub {q r : ℚ} : padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + -r) ≤ padicNorm p q ⊔ padicNorm p (-r)

Tactic:
exact padicNorm.nonarchimedean

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q - r) ≤ padicNorm p q ⊔ padicNorm p r

Tactic:
rw [sub_eq_add_neg, ← padicNorm.neg r]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + -r) ≤ padicNorm p q ⊔ padicNorm p (-r)
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[reassoc, simp]
lemma map_comp {S S' S'' : Scheme} (f : S ⟶ S') (g : S' ⟶ S'') :
    map n (f ≫ g) = map n f ≫ map n g

Proof state:
n : Type v
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ map n (f ≫ g) = map n f ≫ map n g

Tactic:
ext1

Result:
case h₁
n : Type v
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ map n (f ≫ g) ≫ 𝔸(n; S'') ↘ S'' = (map n f ≫ map n g) ≫ 𝔸(n; S'') ↘ S''

case h₂
n : Type v
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (f ≫ g)))) (coord S'' i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n f ≫ map n g))) (coord S'' i✝)

Proof state:
case h₂
n : Type v
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (f ≫ g)))) (coord S'' i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n f ≫ map n g))) (coord S'' i✝)

Tactic:
simp

Result:
no goals

Proof state:
case h₁
n : Type v
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ map n (f ≫ g) ≫ 𝔸(n; S'') ↘ S'' = (map n f ≫ map n g) ≫ 𝔸(n; S'') ↘ S''

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma div_ne_zero_iff : a / b ≠ 0 ↔ b ≠ 0 ∧ b ≤ a

Proof state:
a b : ℕ
⊢ a / b ≠ 0 ↔ b ≠ 0 ∧ b ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_add_opow_of_principal_add {a} (ha : Principal (· + ·) a) (b : Ordinal) :
    Principal (· + ·) (a ^ b)

Proof state:
case inl.inl
ha : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) 1

Tactic:
exact principal_add_one

Result:
no goals

Proof state:
case inr.intro
b c : Ordinal.{u_1}
ha : Principal (fun x1 x2 => x1 + x2) ((fun x => ω ^ x) c)
⊢ Principal (fun x1 x2 => x1 + x2) (ω ^ (c * b))

Tactic:
exact principal_add_omega0_opow _

Result:
no goals

Proof state:
case inl.inl
ha : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) (0 ^ 0)

Tactic:
rw [opow_zero]

Result:
case inl.inl
ha : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) 1

Proof state:
case inl.inr
b : Ordinal.{u_1}
ha : Principal (fun x1 x2 => x1 + x2) 0
hb : b ≠ 0
⊢ Principal (fun x1 x2 => x1 + x2) (0 ^ b)

Tactic:
rwa [zero_opow hb]

Result:
no goals

Proof state:
a : Ordinal.{u_1}
ha : Principal (fun x1 x2 => x1 + x2) a
b : Ordinal.{u_1}
⊢ Principal (fun x1 x2 => x1 + x2) (a ^ b)

Tactic:
rcases principal_add_iff_zero_or_omega0_opow.1 ha with (rfl | ⟨c, rfl⟩)

Result:
case inl
b : Ordinal.{u_1}
ha : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) (0 ^ b)

case inr.intro
b c : Ordinal.{u_1}
ha : Principal (fun x1 x2 => x1 + x2) ((fun x => ω ^ x) c)
⊢ Principal (fun x1 x2 => x1 + x2) ((fun x => ω ^ x) c ^ b)

Proof state:
case inl
b : Ordinal.{u_1}
ha : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) (0 ^ b)

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Result:
case inl.inl
ha : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) (0 ^ 0)

case inl.inr
b : Ordinal.{u_1}
ha : Principal (fun x1 x2 => x1 + x2) 0
hb : b ≠ 0
⊢ Principal (fun x1 x2 => x1 + x2) (0 ^ b)

Proof state:
case inr.intro
b c : Ordinal.{u_1}
ha : Principal (fun x1 x2 => x1 + x2) ((fun x => ω ^ x) c)
⊢ Principal (fun x1 x2 => x1 + x2) ((fun x => ω ^ x) c ^ b)

Tactic:
rw [← opow_mul]

Result:
case inr.intro
b c : Ordinal.{u_1}
ha : Principal (fun x1 x2 => x1 + x2) ((fun x => ω ^ x) c)
⊢ Principal (fun x1 x2 => x1 + x2) (ω ^ (c * b))
-- Mathlib/Data/Set/Image.lean
theorem subset_image_iff {t : Set β} :
    t ⊆ f '' s ↔ ∃ u, u ⊆ s ∧ f '' u = t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ f '' (f ⁻¹' t ∩ s) = t

Tactic:
rwa [image_preimage_inter, inter_eq_left]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ t ⊆ f '' s ↔ ∃ u ⊆ s, f '' u = t

Tactic:
refine ⟨fun h ↦ ⟨f ⁻¹' t ∩ s, inter_subset_right, ?_⟩,
  fun ⟨u, hu, hu'⟩ ↦ hu'.symm ▸ image_mono hu⟩

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ f '' (f ⁻¹' t ∩ s) = t
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem Intersecting.is_max_iff_card_eq (hs : (s : Set α).Intersecting) :
    (∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α

Proof state:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∪ compl ⁻¹' ↑s

Tactic:
simp_rw [mem_union, mem_preimage]

Result:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∨ aᶜ ∈ ↑s

Proof state:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ ↑s ∧ aᶜ ∉ ↑s
⊢ (↑(insert a s)).Intersecting

Tactic:
rw [coe_insert]

Result:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ ↑s ∧ aᶜ ∉ ↑s
⊢ (insert a ↑s).Intersecting

Proof state:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ (∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α

Tactic:
classical
  refine ⟨fun h ↦ ?_, fun h t ht hst ↦ Finset.eq_of_subset_of_card_le hst <|
    Nat.le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) Nat.two_pos⟩
  suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
    rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]
  rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
    image_eq_preimage_of_inverse compl_compl compl_compl]
  refine eq_univ_of_forall fun a => ?_
  simp_rw [mem_union, mem_preimage]
  by_contra! ha
  refine s.ne_insert_of_not_mem _ ha.1 (h _ ?_ <| s.subset_insert _)
  rw [coe_insert]
  refine hs.insert ?_ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
  rintro rfl
  have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
  rw [compl_bot] at ha
  rw [coe_eq_empty.1 ((hs.isUpperSet' h).not_top_mem.1 ha.2)] at this
  exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma nonempty_embedding_iff : Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

Proof state:
n m : ℕ
⊢ Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨castLEEmb h⟩⟩

Result:
n m : ℕ
h : Nonempty (Fin n ↪ Fin m)
⊢ n ≤ m

Proof state:
case succ.intro
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m
⊢ n + 1 ≤ m

Tactic:
rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
  with ⟨m, rfl⟩

Result:
case succ.intro.intro
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ n + 1 ≤ m.succ

Proof state:
case succ.intro.intro
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
i j : Fin n
h : (fun i => ((e.setValue 0 0) i.succ).pred ⋯) i = (fun i => ((e.setValue 0 0) i.succ).pred ⋯) j
⊢ i = j

Tactic:
simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h

Result:
no goals

Proof state:
case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
h : Nonempty (Fin (n + 1) ↪ Fin m)
⊢ n + 1 ≤ m

Tactic:
obtain ⟨e⟩ := h

Result:
case succ.intro
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m
⊢ n + 1 ≤ m

Proof state:
case zero
m : ℕ
h : Nonempty (Fin 0 ↪ Fin m)
⊢ 0 ≤ m

Tactic:
exact m.zero_le

Result:
no goals

Proof state:
case succ.intro.intro
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ Fin n ↪ Fin m

Tactic:
refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
  fun i j h ↦ ?_⟩

Result:
case succ.intro.intro
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
i j : Fin n
h : (fun i => ((e.setValue 0 0) i.succ).pred ⋯) i = (fun i => ((e.setValue 0 0) i.succ).pred ⋯) j
⊢ i = j

Proof state:
case succ.intro.intro
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ n + 1 ≤ m.succ

Tactic:
refine Nat.succ_le_succ <| ihn ⟨?_⟩

Result:
case succ.intro.intro
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ Fin n ↪ Fin m

Proof state:
n m : ℕ
h : Nonempty (Fin n ↪ Fin m)
⊢ n ≤ m

Tactic:
induction n generalizing m with
| zero => exact m.zero_le
| succ n ihn =>
  obtain ⟨e⟩ := h
  rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
    with ⟨m, rfl⟩
  refine Nat.succ_le_succ <| ihn ⟨?_⟩
  refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
    fun i j h ↦ ?_⟩
  simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h

Result:
no goals
-- Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean
@[simp]
lemma Ideal.algebraMap_residueField_eq_zero {x} :
    algebraMap R I.ResidueField x = 0 ↔ x ∈ I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
x : R
⊢ (algebraMap R (Localization.AtPrime I)) x ∈ IsLocalRing.maximalIdeal (Localization.AtPrime I) ↔ x ∈ I

Tactic:
exact IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
x : R
⊢ (algebraMap R I.ResidueField) x = 0 ↔ x ∈ I

Tactic:
rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I),
  IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
x : R
⊢ (algebraMap R (Localization.AtPrime I)) x ∈ IsLocalRing.maximalIdeal (Localization.AtPrime I) ↔ x ∈ I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i

Proof state:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
ypos : y > 0
lsb_diff : x % 2 = y % 2
p : ¬x / 2 = y / 2
i : Nat
ieq : (x / 2).testBit i ≠ (y / 2).testBit i
⊢ ∃ i, x.testBit i ≠ y.testBit i

Tactic:
apply Exists.intro (i+1)

Result:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
ypos : y > 0
lsb_diff : x % 2 = y % 2
p : ¬x / 2 = y / 2
i : Nat
ieq : (x / 2).testBit i ≠ (y / 2).testBit i
⊢ x.testBit (i + 1) ≠ y.testBit (i + 1)

Proof state:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
ypos : y > 0
lsb_diff : x % 2 = y % 2
p : ¬x / 2 = y / 2
⊢ ∃ i, x.testBit i ≠ y.testBit i

Tactic:
have ⟨i, ieq⟩  := hyp ypos p

Result:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
ypos : y > 0
lsb_diff : x % 2 = y % 2
p : ¬x / 2 = y / 2
i : Nat
ieq : (x / 2).testBit i ≠ (y / 2).testBit i
⊢ ∃ i, x.testBit i ≠ y.testBit i

Proof state:
case inr
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p✝ : x ≠ y
ypos : y > 0
p : x % 2 = 1
⊢ ¬x % 2 = y % 2 → decide (x % 2 = 1) ≠ decide (y % 2 = 1)

Tactic:
cases mod_two_eq_zero_or_one y with | _ q =>
  simp [p,q]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem prepartition_isHenstock (B : Box ι) :
    (prepartition n B).IsHenstock

Proof state:
case intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ (prepartition n B).tag (box n ν) ∈ Box.Icc (box n ν)

Tactic:
rw [prepartition_tag n hν]

Result:
case intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ tag n ν ∈ Box.Icc (box n ν)

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B J✝ : Box ι
hI : J✝ ∈ prepartition n B
⊢ (prepartition n B).tag J✝ ∈ Box.Icc J✝

Tactic:
obtain ⟨ν, hν, rfl⟩ := mem_prepartition_iff.mp hI

Result:
case intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ (prepartition n B).tag (box n ν) ∈ Box.Icc (box n ν)

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
⊢ (prepartition n B).IsHenstock

Tactic:
intro _ hI

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B J✝ : Box ι
hI : J✝ ∈ prepartition n B
⊢ (prepartition n B).tag J✝ ∈ Box.Icc J✝

Proof state:
case intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ tag n ν ∈ Box.Icc (box n ν)

Tactic:
exact Box.coe_subset_Icc (tag_mem _ _)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem dist_div_tan_oangle_right_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : dist p₁ p₂ / Real.Angle.tan (∡ p₂ 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)
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = 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
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = 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
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  dist_div_tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]

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₁).sign = 1

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

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_sub (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b - c

Proof state:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
⊢ a ∣ b - c

Tactic:
simpa only [← sub_eq_add_neg] using h₁.add h₂.neg_right

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem logEmbeddingQuot_injective :
    Function.Injective (logEmbeddingQuot K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  (QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K)))
      ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₁✝)) =
    (QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K)))
      ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₂✝))
⊢ a₁✝ = a₂✝

Tactic:
exact (EmbeddingLike.apply_eq_iff_eq _).mp <| (QuotientGroup.kerLift_injective _).eq_iff.mp h

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  (MonoidHom.toAdditive'
        ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K))).comp
          (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))
      a₁✝ =
    (MonoidHom.toAdditive'
        ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K))).comp
          (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))
      a₂✝
⊢ a₁✝ = a₂✝

Tactic:
simp_rw [MonoidHom.toAdditive'_apply_apply, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom,
  Function.comp_apply, EmbeddingLike.apply_eq_iff_eq] at h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  (QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K)))
      ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₁✝)) =
    (QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K)))
      ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₂✝))
⊢ a₁✝ = a₂✝

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective ⇑(logEmbeddingQuot K)

Tactic:
unfold logEmbeddingQuot

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective
    ⇑(MonoidHom.toAdditive'
        ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K))).comp
          (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective
    ⇑(MonoidHom.toAdditive'
        ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K))).comp
          (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))

Tactic:
intro _ _ h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  (MonoidHom.toAdditive'
        ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K))).comp
          (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))
      a₁✝ =
    (MonoidHom.toAdditive'
        ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K))).comp
          (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))
      a₂✝
⊢ a₁✝ = a₂✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_flip_push_eq_append (l l' : Array α) :
    l.foldr (fun x y => push y x) l' = l' ++ l.reverse

Proof state:
case mk
α : Type u_1
l' : Array α
toList✝ : List α
⊢ foldr (fun x y => y.push x) l' { toList := toList✝ } = l' ++ { toList := toList✝ }.reverse

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ foldr (fun x y => y.push x) { toList := toList✝ } { toList := toList✝¹ } =
    { toList := toList✝ } ++ { toList := toList✝¹ }.reverse

Proof state:
α : Type u_1
l l' : Array α
⊢ foldr (fun x y => y.push x) l' l = l' ++ l.reverse

Tactic:
cases l

Result:
case mk
α : Type u_1
l' : Array α
toList✝ : List α
⊢ foldr (fun x y => y.push x) l' { toList := toList✝ } = l' ++ { toList := toList✝ }.reverse

Proof state:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ foldr (fun x y => y.push x) { toList := toList✝ } { toList := toList✝¹ } =
    { toList := toList✝ } ++ { toList := toList✝¹ }.reverse

Tactic:
simp

Result:
no goals