harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.bisim' {α : TypeVec n} {β : Type*} (Q : β → Prop) (u v : β → Cofix F α)
    (h : ∀ x, Q x → ∃ a f' f₀ f₁,
      Cofix.dest (u x) = q.abs ⟨a, q.P.appendContents f' f₀⟩ ∧
        Cofix.dest (v x) = q.abs ⟨a, q.P.appendContents f' f₁⟩ ∧
          ∀ i, ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x') :
    ∀ x, Q x → u x = v x := fun x Qx =>
  let R := fun w z : Cofix F α => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
  Cofix.bisim R
    (fun x y ⟨x', Qx', xeq, yeq⟩ => by
      rcases h x' Qx' with ⟨a, f', f₀, f₁, ux'eq, vx'eq, h'⟩
      rw [liftR_iff]
      refine
        ⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq,
          yeq.symm ▸ vx'eq, ?_⟩
      intro i; cases i
      · apply h'
      · intro j
        apply Eq.refl)
    _ _ ⟨x, Qx, rfl, rfl⟩

Proof state:
case intro.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∃ a f₀ f₁,
    x.dest = MvQPF.abs ⟨a, f₀⟩ ∧
      y.dest = MvQPF.abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast R (f₀ i j) (f₁ i j)

Tactic:
refine
  ⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq,
    yeq.symm ▸ vx'eq, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast R ((P F).appendContents f' f₀ i j) ((P F).appendContents f' f₁ i j)
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_le_one_iff : a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
simp [hb, hb.not_lt, hb.ne, div_le_one_of_neg]

Result:
no goals

Proof state:
case inr.inl
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a / 0 ≤ 1 ↔ 0 < 0 ∧ a ≤ 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 ≤ a

Tactic:
simp [zero_le_one]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

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

Result:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

case inr.inl
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a / 0 ≤ 1 ↔ 0 < 0 ∧ a ≤ 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 ≤ a

case inr.inr
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Proof state:
case inr.inr
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
simp [hb, hb.not_lt, div_le_one, hb.ne.symm]

Result:
no goals
-- Mathlib/Algebra/Star/Free.lean
theorem star_ι (x : X) : star (ι R x) = ι R x

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : X
⊢ star (ι R x) = ι R x

Tactic:
simp [star, Star.star]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
/-- Formulation of reflection formula tailored to functional equations of L-functions of even
Dirichlet characters (including Riemann zeta). -/
lemma inv_Gammaℝ_one_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) :
    (Gammaℝ (1 - s))⁻¹ = Gammaℂ s * cos (π * s / 2) * (Gammaℝ s)⁻¹

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
n : ℕ
h : s = -(2 * ↑n + 1)
⊢ False

Tactic:
specialize hs (2 * n + 1)

Result:
s : ℂ
h1 : s.Gammaℝ ≠ 0
n : ℕ
h : s = -(2 * ↑n + 1)
hs : s ≠ -↑(2 * n + 1)
⊢ False

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
⊢ ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)

Tactic:
intro n h

Result:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
n : ℕ
h : s = -(2 * ↑n + 1)
⊢ False

Proof state:
s : ℂ
h1 : s.Gammaℝ ≠ 0
n : ℕ
h : s = -(2 * ↑n + 1)
hs : s ≠ -↑(2 * n + 1)
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹

Tactic:
rw [← Gammaℝ_div_Gammaℝ_one_sub h2, ← div_eq_mul_inv, div_right_comm, div_self h1, one_div]

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
n : ℕ
h : s = -(2 * ↑n)
⊢ False

Tactic:
specialize hs (2 * n)

Result:
s : ℂ
n : ℕ
h : s = -(2 * ↑n)
hs : s ≠ -↑(2 * n)
⊢ False

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ s.Gammaℝ ≠ 0

Tactic:
rw [Ne, Gammaℝ_eq_zero_iff, not_exists]

Result:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ ∀ (x : ℕ), ¬s = -(2 * ↑x)

Proof state:
s : ℂ
n : ℕ
h : s = -(2 * ↑n)
hs : s ≠ -↑(2 * n)
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹

Tactic:
have h1 : Gammaℝ s ≠ 0 := by
  rw [Ne, Gammaℝ_eq_zero_iff, not_exists]
  intro n h
  specialize hs (2 * n)
  simp_all

Result:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ ∀ (x : ℕ), ¬s = -(2 * ↑x)

Tactic:
intro n h

Result:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
n : ℕ
h : s = -(2 * ↑n)
⊢ False

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹

Tactic:
have h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1) := by
  intro n h
  specialize hs (2 * n + 1)
  simp_all

Result:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioc_sub_one_left_eq_Icc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioc (a - 1) b = Icc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc_of_not_isMin ha b

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_diff_right : Iic a \ {a} = Iio a :=
  ext fun x => by simp [lt_iff_le_and_ne]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a x : α
⊢ x ∈ Iic a \ {a} ↔ x ∈ Iio a

Tactic:
simp [lt_iff_le_and_ne]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem frequently_lt_of_lt_limsup {α β} [ConditionallyCompleteLinearOrder β] {f : Filter α}
    {u : α → β} {b : β}
    (hu : f.IsCoboundedUnder (· ≤ ·) u

Proof state:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h : b < limsup u f
⊢ ∃ᶠ (x : α) in f, b < u x

Tactic:
contrapose! h

Result:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ limsup u f ≤ b

Proof state:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ limsup u f ≤ b

Tactic:
apply limsSup_le_of_le hu

Result:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ ∀ᶠ (n : β) in map u f, n ≤ b

Proof state:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ ∀ᶠ (n : β) in map u f, n ≤ b

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys.size

Proof state:
case mk.mk
α : Type u_1
inst✝ : BEq α
toList✝¹ toList✝ : List α
h : ({ toList := toList✝¹ } == { toList := toList✝ }) = true
⊢ { toList := toList✝¹ }.size = { toList := toList✝ }.size

Tactic:
simp [List.length_eq_of_beq (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
toList✝¹ toList✝ : List α
h : ({ toList := toList✝¹ } == { toList := toList✝ }) = true
⊢ (?m.144526 == ?m.144527) = true

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
ys : Array α
toList✝ : List α
h : ({ toList := toList✝ } == ys) = true
⊢ { toList := toList✝ }.size = ys.size

Tactic:
cases ys

Result:
case mk.mk
α : Type u_1
inst✝ : BEq α
toList✝¹ toList✝ : List α
h : ({ toList := toList✝¹ } == { toList := toList✝ }) = true
⊢ { toList := toList✝¹ }.size = { toList := toList✝ }.size

Proof state:
α : Type u_1
inst✝ : BEq α
xs ys : Array α
h : (xs == ys) = true
⊢ xs.size = ys.size

Tactic:
cases xs

Result:
case mk
α : Type u_1
inst✝ : BEq α
ys : Array α
toList✝ : List α
h : ({ toList := toList✝ } == ys) = true
⊢ { toList := toList✝ }.size = ys.size
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_range_le_of_locally_holder_on [SecondCountableTopology X] {r : ℝ≥0} {f : X → Y}
    (hr : 0 < r) (hf : ∀ x : X, ∃ C : ℝ≥0, ∃ s ∈ 𝓝 x, HolderOnWith C r f s) :
    dimH (range f) ≤ dimH (univ : Set X) / r

Proof state:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
⊢ dimH (f '' univ) ≤ dimH univ / ↑r

Tactic:
refine dimH_image_le_of_locally_holder_on hr fun x _ => ?_

Result:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝[univ] x, HolderOnWith C r f t

Proof state:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝[univ] x, HolderOnWith C r f t

Tactic:
simpa only [exists_prop, nhdsWithin_univ] using hf x

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
⊢ dimH (range f) ≤ dimH univ / ↑r

Tactic:
rw [← image_univ]

Result:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
⊢ dimH (f '' univ) ≤ dimH univ / ↑r
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_cos_pow_three :
    ∫ x in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3

Tactic:
exact this

Result:
no goals

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3

Tactic:
have := @integral_sin_pow_mul_cos_pow_odd a b 0 1

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 0 * cos x ^ (2 * 1 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 0 * (1 - u ^ 2) ^ 1
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 0 * cos x ^ (2 * 1 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 0 * (1 - u ^ 2) ^ 1
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3

Tactic:
norm_num at this

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_alterKey [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β → Option β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) :
    getKey k' (alterKey k f l) hc =
      if heq : k == k' then
        k
      else
        haveI h' : containsKey k' l

Proof state:
case isTrue
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l
h✝ : (k == k') = true
⊢ getKey k' (alterKey k f l) hc = k

Tactic:
next heq =>
apply Option.some_inj.mp
simp_all

Result:
no goals
-- Mathlib/Analysis/Complex/Isometry.lean
theorem rotation_ne_conjLIE (a : Circle) : rotation a ≠ conjLIE

Proof state:
a : Circle
⊢ rotation a ≠ conjLIE

Tactic:
intro h

Result:
a : Circle
h : rotation a = conjLIE
⊢ False

Proof state:
a : Circle
h : rotation a = conjLIE
⊢ False

Tactic:
have h1 : rotation a 1 = conj 1 := LinearIsometryEquiv.congr_fun h 1

Result:
a : Circle
h : rotation a = conjLIE
h1 : (rotation a) 1 = (starRingEnd ℂ) 1
⊢ False

Proof state:
a : Circle
h : rotation a = conjLIE
h1 : (rotation a) 1 = (starRingEnd ℂ) 1
⊢ False

Tactic:
have hI : rotation a I = conj I := LinearIsometryEquiv.congr_fun h I

Result:
a : Circle
h : rotation a = conjLIE
h1 : (rotation a) 1 = (starRingEnd ℂ) 1
hI : (rotation a) I = (starRingEnd ℂ) I
⊢ False

Proof state:
a : Circle
h : rotation a = conjLIE
h1 : (rotation a) 1 = (starRingEnd ℂ) 1
hI : (rotation a) I = (starRingEnd ℂ) I
⊢ False

Tactic:
rw [rotation_apply, RingHom.map_one, mul_one] at h1

Result:
a : Circle
h : rotation a = conjLIE
h1 : ↑a = 1
hI : (rotation a) I = (starRingEnd ℂ) I
⊢ False

Proof state:
a : Circle
h : rotation a = conjLIE
h1 : ↑a = 1
hI : 1 = 0
⊢ False

Tactic:
exact one_ne_zero hI

Result:
no goals

Proof state:
a : Circle
h : rotation a = conjLIE
h1 : ↑a = 1
hI : (rotation a) I = (starRingEnd ℂ) I
⊢ False

Tactic:
rw [rotation_apply, conj_I, ← neg_one_mul, mul_left_inj' I_ne_zero, h1, eq_neg_self_iff] at hI

Result:
a : Circle
h : rotation a = conjLIE
h1 : ↑a = 1
hI : 1 = 0
⊢ False
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_one : ⌊(1 : α)⌋ = 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ⌊1⌋ = 1

Tactic:
rw [← cast_one, floor_intCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.filterMap [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {f : (a : α) → β a → Option (γ a)} :
    DistinctKeys l → DistinctKeys (l.filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩))

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
f : (a : α) → β a → Option (γ a)
⊢ DistinctKeys l → DistinctKeys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)

Tactic:
apply distinctKeys_of_sublist_keys

Result:
case h
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
f : (a : α) → β a → Option (γ a)
⊢ (keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)).Sublist (keys l)

Proof state:
case h
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
f : (a : α) → β a → Option (γ a)
⊢ (List.map (fun x => x.fst) (List.filter (fun p => (f p.fst p.snd).isSome) l)).Sublist (List.map (fun x => x.fst) l)

Tactic:
apply Sublist.map

Result:
case h.s
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
f : (a : α) → β a → Option (γ a)
⊢ (List.filter (fun p => (f p.fst p.snd).isSome) l).Sublist l

Proof state:
case h
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
f : (a : α) → β a → Option (γ a)
⊢ (keys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)).Sublist (keys l)

Tactic:
rw [keys_filterMap, keys_eq_map, keys_eq_map]

Result:
case h
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
f : (a : α) → β a → Option (γ a)
⊢ (List.map (fun x => x.fst) (List.filter (fun p => (f p.fst p.snd).isSome) l)).Sublist (List.map (fun x => x.fst) l)

Proof state:
case h.s
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
f : (a : α) → β a → Option (γ a)
⊢ (List.filter (fun p => (f p.fst p.snd).isSome) l).Sublist l

Tactic:
exact filter_sublist l

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
s : Set α
t : Set β
⊢ (μ.prod ν) (s ×ˢ t) = μ s * ν t

Tactic:
simp [coeFn_def]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem integrable_prod_iff ⦃f : α × β → E⦄ (h1f : AEStronglyMeasurable f (μ.prod ν)) :
    Integrable f (μ.prod ν) ↔
      (∀ᵐ x ∂μ, Integrable (fun y => f (x, y)) ν) ∧ Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂ν) μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y => f (x, y)) ν) ∧ Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
simp [Integrable, h1f, hasFiniteIntegral_prod_iff', h1f.norm.integral_prod_right',
  h1f.prod_mk_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).getKey! k = if k ∈ m then k else default

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey! k = if m.contains k = true then k else default

Tactic:
simp_to_raw using Raw₀.getKey!_modify_self

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey! k = if k ∈ m then k else default

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey! k = if m.contains k = true then k else default
-- Mathlib/GroupTheory/GroupAction/Iwasawa.lean
theorem commutator_le (IwaS : IwasawaStructure M α) [IsQuasiPreprimitive M α]
    (N : Subgroup M) [nN : N.Normal] (hNX : MulAction.fixedPoints N α ≠ .univ) :
    commutator M ≤ N

Proof state:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a x : α
⊢ IwaS.T x ≤ N ⊔ IwaS.T a

Tactic:
obtain ⟨g, rfl⟩ := MulAction.exists_smul_eq N a x

Result:
case intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a
-- Mathlib/Analysis/Calculus/ContDiff/RCLike.lean
/-- If `f` is `C^1`, it is locally Lipschitz. -/
lemma ContDiff.locallyLipschitz {f : E' → F'} (hf : ContDiff 𝕂 1 f) : LocallyLipschitz f

Proof state:
case intro.intro.intro
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf✝ : ContDiff 𝕂 1 f
x : E'
K : ℝ≥0
t : Set E'
ht : t ∈ 𝓝 ?m.65930
hf : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Tactic:
use K, t

Result:
no goals

Proof state:
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : ContDiff 𝕂 1 f
x : E'
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Tactic:
rcases hf.contDiffAt.exists_lipschitzOnWith with ⟨K, t, ht, hf⟩

Result:
case intro.intro.intro
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf✝ : ContDiff 𝕂 1 f
x : E'
K : ℝ≥0
t : Set E'
ht : t ∈ 𝓝 ?m.65930
hf : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Proof state:
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : ContDiff 𝕂 1 f
⊢ LocallyLipschitz f

Tactic:
intro x

Result:
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : ContDiff 𝕂 1 f
x : E'
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t