harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
lemma tendsto_rpow_atTop_of_base_gt_one (b : ℝ) (hb : 1 < b) :
    Tendsto (b ^ · : ℝ → ℝ) atBot (𝓝 (0 : ℝ))

Proof state:
b : ℝ
hb : 1 < b
⊢ Tendsto (fun x => rexp (log b * x)) atBot (𝓝 0)

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_pos ?_).mpr tendsto_id

Result:
b : ℝ
hb : 1 < b
⊢ 0 < log b

Proof state:
b : ℝ
hb : 1 < b
⊢ Tendsto (fun x => b ^ x) atBot (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]

Result:
b : ℝ
hb : 1 < b
⊢ Tendsto (fun x => rexp (log b * x)) atBot (𝓝 0)

Proof state:
b : ℝ
hb : 1 < b
⊢ 0 ≤ b

Tactic:
positivity

Result:
no goals

Proof state:
b : ℝ
hb : 1 < b
⊢ 0 < b

Tactic:
positivity

Result:
no goals

Proof state:
b : ℝ
hb : 1 < b
⊢ 1 < b

Tactic:
aesop

Result:
no goals

Proof state:
b : ℝ
hb : 1 < b
⊢ 0 < log b

Tactic:
exact (log_pos_iff (by positivity)).mpr <| by aesop

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_eq_of_same {a b} {d : S} :
    f.mk' a d = f.mk' b d ↔ ∃ c : S, c * a = c * b

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a b : M
d : ↥S
⊢ f.mk' a d = f.mk' b d ↔ ∃ c, ↑c * a = ↑c * b

Tactic:
rw [mk'_eq_iff_eq', map_mul, map_mul, ← eq_iff_exists f]

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a b : M
d : ↥S
⊢ f.toMap a * f.toMap ↑d = f.toMap b * f.toMap ↑d ↔ f.toMap a = f.toMap b

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a b : M
d : ↥S
⊢ f.toMap a * f.toMap ↑d = f.toMap b * f.toMap ↑d ↔ f.toMap a = f.toMap b

Tactic:
exact (map_units f d).mul_left_inj

Result:
no goals
-- Mathlib/Tactic/NormNum/Prime.lean
theorem isNat_minFac_4 : {n n' k : ℕ} →
    IsNat n n' → MinFacHelper n' k → (k * k).ble n' = false → IsNat (minFac n) n'
  | n, _, k, ⟨rfl⟩, h1, h2 => by
    refine ⟨(Nat.prime_def_minFac.mp ?_).2⟩
    rw [Nat.prime_def_le_sqrt]
    refine ⟨h1.one_lt, fun m hm hmn h2mn ↦ ?_⟩
    exact lt_irrefl m <| calc
      m ≤ sqrt n   := hmn
      _ < k        := sqrt_lt.mpr (ble_eq_false.mp h2)
      _ ≤ n.minFac := h1.2.2
      _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn

Proof state:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n

Tactic:
refine ⟨h1.one_lt, fun m hm hmn h2mn ↦ ?_⟩

Result:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
m : ℕ
hm : 2 ≤ m
hmn : m ≤ n.sqrt
h2mn : m ∣ n
⊢ False

Proof state:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ Nat.Prime n

Tactic:
rw [Nat.prime_def_le_sqrt]

Result:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n

Proof state:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
m : ℕ
hm : 2 ≤ m
hmn : m ≤ n.sqrt
h2mn : m ∣ n
⊢ False

Tactic:
exact lt_irrefl m <| calc
  m ≤ sqrt n   := hmn
  _ < k        := sqrt_lt.mpr (ble_eq_false.mp h2)
  _ ≤ n.minFac := h1.2.2
  _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn

Result:
no goals

Proof state:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ IsNat n.minFac n

Tactic:
refine ⟨(Nat.prime_def_minFac.mp ?_).2⟩

Result:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ Nat.Prime n
-- Mathlib/Data/Matroid/Map.lean
lemma comapOn_dual_eq_of_bijOn (h : BijOn f E N.E) :
    (N.comapOn E f)✶ = N✶.comapOn E f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ (N.comapOn E f)✶.IsBase B ↔ (N✶.comapOn E f).IsBase B

Tactic:
rw [comapOn_isBase_iff_of_bijOn (by simpa), dual_isBase_iff, comapOn_isBase_iff_of_bijOn h,
  dual_isBase_iff _, comapOn_ground_eq, and_iff_left diff_subset, and_iff_left (by simpa),
  h.injOn.image_diff_subset (by simpa), h.image_eq]

Result:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f)✶.E = (N✶.comapOn E f).E

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f)✶ = N✶.comapOn E f

Tactic:
refine ext_isBase (by simp) (fun B hB ↦ ?_)

Result:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ (N.comapOn E f)✶.IsBase B ↔ (N✶.comapOn E f).IsBase B

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ B ⊆ E

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ BijOn f E N✶.E

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E

Tactic:
exact (h.mapsTo.mono_left (show B ⊆ E by simpa)).image_subset

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem map_add_atTop_eq_nat (k : ℕ) : map (fun a => a + k) atTop = atTop :=
  map_atTop_eq_of_gc (· - k) k (fun _ _ h => Nat.add_le_add_right h k)
    (fun _ _ h => (Nat.le_sub_iff_add_le h).symm) fun a h => by rw [Nat.sub_add_cancel h]

Proof state:
k a : ℕ
h : a ≥ k
⊢ a ≤ (fun x => x - k) a + k

Tactic:
rw [Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem dvd_zero (a : α) : a ∣ 0 :=
  Dvd.intro 0 (by simp)

Proof state:
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
⊢ a * 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
@[simp] lemma removeNth_update (p : Fin (n + 1)) (x) (f : ∀ j, α j) :
    removeNth p (update f p x) = removeNth p f

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
i : Fin n
⊢ p.removeNth (update f p x) i = p.removeNth f i

Tactic:
simp [removeNth, succAbove_ne]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
⊢ p.removeNth (update f p x) = p.removeNth f

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
i : Fin n
⊢ p.removeNth (update f p x) i = p.removeNth f i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_zero : ∀ a : Int, a / 0 = 0
  | ofNat _ => show ofNat _ = _ by simp
  | -[_+1] => rfl

Proof state:
a✝ : Nat
⊢ ofNat (a✝ / 0) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle y (y - x) = Real.arcsin (‖x‖ / ‖y - x‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ o.oangle y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

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

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ o.oangle y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma isOfFinOrder_of_finite (x : G) : IsOfFinOrder x

Proof state:
G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x : G
⊢ IsOfFinOrder x

Tactic:
by_contra h

Result:
G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x : G
h : ¬IsOfFinOrder x
⊢ False

Proof state:
G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x : G
h : ¬IsOfFinOrder x
⊢ False

Tactic:
exact infinite_not_isOfFinOrder h <| Set.toFinite _

Result:
no goals
-- Mathlib/RingTheory/RingHom/Locally.lean
/-- Equivalence variant of `locally_of_exists`. This is sometimes easier to use, if the
`IsLocalization.Away` instance can't be automatically inferred. -/
lemma locally_iff_exists (hP : RespectsIso P) (f : R →+* S) :
    Locally P f ↔ ∃ (ι : Type u) (s : ι → S) (_ : Ideal.span (Set.range s) = ⊤) (Sₜ : ι → Type u)
      (_ : (i : ι) → CommRing (Sₜ i)) (_ : (i : ι) → Algebra S (Sₜ i))
      (_ : (i : ι) → IsLocalization.Away (s i : S) (Sₜ i)),
      ∀ i, P ((algebraMap S (Sₜ i)).comp f) :=
  ⟨fun ⟨s, hsone, hs⟩ ↦ ⟨s, fun t : s ↦ (t : S), by simpa, fun t ↦ Localization.Away (t : S),
      inferInstance, inferInstance, inferInstance, fun t ↦ hs t.val t.property⟩,
    fun ⟨ι, s, hsone, Sₜ, _, _, hislocal, hs⟩ ↦ locally_of_exists hP f s hsone Sₜ hs⟩

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
⊢ Ideal.span (Set.range fun t => ↑t) = ⊤

Tactic:
simpa

Result:
no goals
-- Mathlib/Deprecated/Logic.lean
theorem decide_False' (h : Decidable False) : decide False = false

Proof state:
h : Decidable False
⊢ decide False = false

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem map_objs_eq (hφ : Function.Injective φ.obj) : (map φ hφ S).objs = φ.obj '' S.objs

Proof state:
case h
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
x : D
⊢ x ∈ (map φ hφ S).objs ↔ x ∈ φ.obj '' S.objs

Tactic:
convert mem_map_objs_iff S φ hφ x

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
⊢ (map φ hφ S).objs = φ.obj '' S.objs

Tactic:
ext x

Result:
case h
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
x : D
⊢ x ∈ (map φ hφ S).objs ↔ x ∈ φ.obj '' S.objs
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_empty [Monad m] (f : β → α → m β) (init : β) :
    foldlM f init #[] start stop = return init

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
start stop : Nat
inst✝ : Monad m
f : β → α → m β
init : β
⊢ foldlM f init #[] start stop = pure init

Tactic:
simp [foldlM]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ↔ ReflBEq α

Proof state:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Array α)
a : α
⊢ (a == a) = true

Tactic:
apply beq_of_beq_singleton

Result:
case mp.refl.a
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Array α)
a : α
⊢ (#[a] == #[a]) = true

Proof state:
case mpr.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ∀ {a : Array α}, (a == a) = true

Tactic:
apply Array.isEqv_self_beq

Result:
no goals

Proof state:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Array α)
⊢ ∀ {a : α}, (a == a) = true

Tactic:
intro a

Result:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Array α)
a : α
⊢ (a == a) = true

Proof state:
case mp
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Array α)
⊢ ReflBEq α

Tactic:
constructor

Result:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Array α)
⊢ ∀ {a : α}, (a == a) = true

Proof state:
case mp.refl.a
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Array α)
a : α
⊢ (#[a] == #[a]) = true

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq (Array α) → ReflBEq α

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : BEq α
h : ReflBEq (Array α)
⊢ ReflBEq α

Proof state:
case mpr
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq α → ReflBEq (Array α)

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ReflBEq (Array α)

Proof state:
case mpr
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ReflBEq (Array α)

Tactic:
constructor

Result:
case mpr.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ∀ {a : Array α}, (a == a) = true

Proof state:
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq (Array α) ↔ ReflBEq α

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq (Array α) → ReflBEq α

case mpr
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq α → ReflBEq (Array α)
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem add (hf : IsBoundedLinearMap 𝕜 f) (hg : IsBoundedLinearMap 𝕜 g) :
    IsBoundedLinearMap 𝕜 fun e => f e + g e :=
  let ⟨hlf, Mf, _, hMf⟩ := hf
  let ⟨hlg, Mg, _, hMg⟩ := hg
  (hlf.mk' _ + hlg.mk' _).isLinear.with_bound (Mf + Mg) fun x =>
    calc
      ‖f x + g x‖ ≤ Mf * ‖x‖ + Mg * ‖x‖ := norm_add_le_of_le (hMf x) (hMg x)
      _ ≤ (Mf + Mg) * ‖x‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left✝¹ : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left✝ : 0 < Mg
hMg : ∀ (x : E), ‖g x‖ ≤ Mg * ‖x‖
x : E
⊢ Mf * ‖x‖ + Mg * ‖x‖ ≤ (Mf + Mg) * ‖x‖

Tactic:
rw [add_mul]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem add_assoc : a + b + c = a + (b + c) :=
  numDenCasesOn' a fun n₁ d₁ h₁ ↦ numDenCasesOn' b fun n₂ d₂ h₂ ↦ numDenCasesOn' c fun n₃ d₃ h₃ ↦ by
    simp only [ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂, divInt_add_divInt,
      Int.mul_eq_zero, or_self, h₃]
    rw [Int.mul_assoc, Int.add_mul, Int.add_mul, Int.mul_assoc, Int.add_assoc]
    congr 2
    ac_rfl

Proof state:
case e_a.e_a
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₂ * ↑d₁ * ↑d₃ + n₃ * (↑d₁ * ↑d₂) = n₂ * ↑d₃ * ↑d₁ + n₃ * ↑d₂ * ↑d₁

Tactic:
ac_rfl

Result:
no goals

Proof state:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₁ * ↑d₃ + n₃ * (↑d₁ * ↑d₂))) /. (↑d₁ * (↑d₂ * ↑d₃)) =
    (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ * ↑d₁ + n₃ * ↑d₂ * ↑d₁)) /. (↑d₁ * (↑d₂ * ↑d₃))

Tactic:
congr 2

Result:
case e_a.e_a
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₂ * ↑d₁ * ↑d₃ + n₃ * (↑d₁ * ↑d₂) = n₂ * ↑d₃ * ↑d₁ + n₃ * ↑d₂ * ↑d₁

Proof state:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₁ /. ↑d₁ + n₂ /. ↑d₂ + n₃ /. ↑d₃ = n₁ /. ↑d₁ + (n₂ /. ↑d₂ + n₃ /. ↑d₃)

Tactic:
simp only [ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂, divInt_add_divInt,
  Int.mul_eq_zero, or_self, h₃]

Result:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ ((n₁ * ↑d₂ + n₂ * ↑d₁) * ↑d₃ + n₃ * (↑d₁ * ↑d₂)) /. (↑d₁ * ↑d₂ * ↑d₃) =
    (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ + n₃ * ↑d₂) * ↑d₁) /. (↑d₁ * (↑d₂ * ↑d₃))

Proof state:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ ((n₁ * ↑d₂ + n₂ * ↑d₁) * ↑d₃ + n₃ * (↑d₁ * ↑d₂)) /. (↑d₁ * ↑d₂ * ↑d₃) =
    (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ + n₃ * ↑d₂) * ↑d₁) /. (↑d₁ * (↑d₂ * ↑d₃))

Tactic:
rw [Int.mul_assoc, Int.add_mul, Int.add_mul, Int.mul_assoc, Int.add_assoc]

Result:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₁ * ↑d₃ + n₃ * (↑d₁ * ↑d₂))) /. (↑d₁ * (↑d₂ * ↑d₃)) =
    (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ * ↑d₁ + n₃ * ↑d₂ * ↑d₁)) /. (↑d₁ * (↑d₂ * ↑d₃))
-- Mathlib/Algebra/LinearRecurrence.lean
theorem is_sol_mkSol (init : Fin E.order → α) : E.IsSolution (E.mkSol init)

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ E.mkSol init (n + E.order) = ∑ i : Fin E.order, E.coeffs i * E.mkSol init (n + ↑i)

Tactic:
rw [mkSol]

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ (if h : n + E.order < E.order then init ⟨n + E.order, h⟩
    else
      ∑ k : Fin E.order,
        let_fun x := ⋯;
        E.coeffs k * E.mkSol init (n + E.order - E.order + ↑k)) =
    ∑ i : Fin E.order, E.coeffs i * E.mkSol init (n + ↑i)

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ (if h : n + E.order < E.order then init ⟨n + E.order, h⟩
    else
      ∑ k : Fin E.order,
        let_fun x := ⋯;
        E.coeffs k * E.mkSol init (n + E.order - E.order + ↑k)) =
    ∑ i : Fin E.order, E.coeffs i * E.mkSol init (n + ↑i)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
⊢ E.IsSolution (E.mkSol init)

Tactic:
intro n

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ E.mkSol init (n + E.order) = ∑ i : Fin E.order, E.coeffs i * E.mkSol init (n + ↑i)
-- Mathlib/Analysis/RCLike/Basic.lean
lemma pos_iff_exists_ofReal : 0 < z ↔ ∃ x > (0 : ℝ), x = z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < re z ∧ im z = 0 ↔ ∃ x > 0, re ↑x = re z ∧ im ↑x = im z

Tactic:
aesop

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ ∃ x > 0, ↑x = z

Tactic:
simp_rw [pos_iff (K := K), ext_iff (K := K)]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < re z ∧ im z = 0 ↔ ∃ x > 0, re ↑x = re z ∧ im ↑x = im z
-- Mathlib/NumberTheory/AbelSummation.lean
theorem sumlocc {m : ℕ} (n : ℕ) :
    ∀ᵐ t, t ∈ Set.Icc (n : ℝ) (n + 1) → ∑ k ∈ Icc m ⌊t⌋₊, c k = ∑ k ∈ Icc m n, c k

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
⊢ ∀ᵐ (t : ℝ), t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc m ⌊t⌋₊, c k = ∑ k ∈ Icc m n, c k

Tactic:
filter_upwards [Ico_ae_eq_Icc] with t h ht

Result:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
t : ℝ
h : Set.Ico ?m.1131 ?m.1132 t = Set.Icc ?m.1131 ?m.1132 t
ht : t ∈ Set.Icc (↑n) (↑n + 1)
⊢ ∑ k ∈ Icc m ⌊t⌋₊, c k = ∑ k ∈ Icc m n, c k

Proof state:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
t : ℝ
h : Set.Ico ?m.1131 ?m.1132 t = Set.Icc ?m.1131 ?m.1132 t
ht : t ∈ Set.Icc (↑n) (↑n + 1)
⊢ ∑ k ∈ Icc m ⌊t⌋₊, c k = ∑ k ∈ Icc m n, c k

Tactic:
rw [Nat.floor_eq_on_Ico _ _ (h.mpr ht)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem transpose_circulant [AddGroup n] (v : n → α) :
    (circulant v)ᵀ = circulant fun i => v (-i)

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝ : AddGroup n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᵀ i✝ j✝ = circulant (fun i => v (-i)) i✝ j✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Type u_3
inst✝ : AddGroup n
v : n → α
⊢ (circulant v)ᵀ = circulant fun i => v (-i)

Tactic:
ext

Result:
case a
α : Type u_1
n : Type u_3
inst✝ : AddGroup n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᵀ i✝ j✝ = circulant (fun i => v (-i)) i✝ j✝
-- Mathlib/Data/Finset/Basic.lean
lemma disjoint_erase_insert (ha : a ∉ s) : Disjoint (insert a s) (t.erase a) ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ Disjoint (insert a s) (t.erase a) ↔ Disjoint s t

Tactic:
rw [← disjoint_erase_comm, erase_insert ha]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordProj_of_not_prime (n p : ℕ) (hp : ¬p.Prime) : ordProj[p] n = 1

Proof state:
n p : ℕ
hp : ¬Prime p
⊢ p ^ n.factorization p = 1

Tactic:
simp [factorization_eq_zero_of_non_prime n hp]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_int_lt (x : α) : ∃ n : ℤ, (n : α) < x :=
  let ⟨n, h⟩ := exists_int_gt (-x)
  ⟨-n, by rw [Int.cast_neg]; exact neg_lt.1 h⟩

Proof state:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ ↑(-n) < x

Tactic:
rw [Int.cast_neg]

Result:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ -↑n < x

Proof state:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ -↑n < x

Tactic:
exact neg_lt.1 h

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
@[simp] lemma egauge_zero_left_eq_top : egauge 𝕜 0 x = ∞ ↔ x ≠ 0

Proof state:
𝕜 : Type u_1
inst✝³ : NNNorm 𝕜
inst✝² : Nonempty 𝕜
E : Type u_2
inst✝¹ : Zero E
inst✝ : SMulZeroClass 𝕜 E
x : E
⊢ egauge 𝕜 0 x = ⊤ ↔ x ≠ 0

Tactic:
simp [egauge_eq_top]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Free.lean
theorem basisAux_tmul (a : A) (m : M) :
    basisAux A b (a ⊗ₜ m) = a • Finsupp.mapRange (algebraMap R A) (map_zero _) (b.repr m)

Proof state:
case h
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
m : M
a✝ : ι
⊢ ((basisAux A b) (a ⊗ₜ[R] m)) a✝ = (a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)) a✝

Tactic:
simp [basisAux, ← Algebra.commutes, Algebra.smul_def]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
m : M
⊢ (basisAux A b) (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
m : M
a✝ : ι
⊢ ((basisAux A b) (a ⊗ₜ[R] m)) a✝ = (a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)) a✝
-- Mathlib/Data/Int/Init.lean
lemma ediv_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : 0 < b) : ediv a b = -((-a - 1) / b + 1) :=
  match a, b, eq_negSucc_of_lt_zero Ha, eq_succ_of_zero_lt Hb with
  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by
    rw [show (- -[m+1] : ℤ) = (m + 1 : ℤ) by rfl]; rw [Int.add_sub_cancel]; rfl

Proof state:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n.succ
⊢ - -[m+1] = ↑m + 1

Tactic:
rfl

Result:
no goals

Proof state:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n.succ
⊢ -[m+1].ediv ↑n.succ = -((↑m + 1 - 1) / ↑n.succ + 1)

Tactic:
rw [Int.add_sub_cancel]

Result:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n.succ
⊢ -[m+1].ediv ↑n.succ = -(↑m / ↑n.succ + 1)

Proof state:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n.succ
⊢ -[m+1].ediv ↑n.succ = -(↑m / ↑n.succ + 1)

Tactic:
rfl

Result:
no goals

Proof state:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n.succ
⊢ -[m+1].ediv ↑n.succ = -((- -[m+1] - 1) / ↑n.succ + 1)

Tactic:
rw [show (- -[m+1] : ℤ) = (m + 1 : ℤ) by rfl]

Result:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n.succ
⊢ -[m+1].ediv ↑n.succ = -((↑m + 1 - 1) / ↑n.succ + 1)