harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem map_lt [LT α] [LT β]
    {l₁ l₂ : Array α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) :
    map f l₁ < map f l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
w : ∀ (x y : α), x < y → f x < f y
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } < { toList := toList✝ }
⊢ map f { toList := toList✝¹ } < map f { toList := toList✝ }

Tactic:
simpa using List.map_lt w h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₁ l₂ : Array α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ < l₂
⊢ map f l₁ < map f l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₂ : Array α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
toList✝ : List α
h : { toList := toList✝ } < l₂
⊢ map f { toList := toList✝ } < map f l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
l₂ : Array α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
toList✝ : List α
h : { toList := toList✝ } < l₂
⊢ map f { toList := toList✝ } < map f l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
w : ∀ (x y : α), x < y → f x < f y
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } < { toList := toList✝ }
⊢ map f { toList := toList✝¹ } < map f { toList := toList✝ }
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem range_sin_infinite : (range Real.sin).Infinite

Proof state:
⊢ (range sin).Infinite

Tactic:
rw [Real.range_sin]

Result:
⊢ (Icc (-1) 1).Infinite

Proof state:
⊢ -1 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ (Icc (-1) 1).Infinite

Tactic:
exact Icc_infinite (by norm_num)

Result:
no goals
-- Mathlib/Algebra/Algebra/Rat.lean
/-- `nnqsmul` is equal to any other module structure via a cast. -/
lemma cast_smul_eq_qsmul [Module R S] (q : ℚ) (a : S) : (q : R) • a = q • a

Proof state:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionRing R
inst✝³ : CharZero R
inst✝² : Ring S
inst✝¹ : Module ℚ S
inst✝ : Module R S
q : ℚ
a : S
⊢ (fun x => ↑q.den • x) (↑q • a) = (fun x => ↑q.den • x) (q • a)

Tactic:
dsimp

Result:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionRing R
inst✝³ : CharZero R
inst✝² : Ring S
inst✝¹ : Module ℚ S
inst✝ : Module R S
q : ℚ
a : S
⊢ ↑q.den • ↑q • a = ↑q.den • q • a

Proof state:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionRing R
inst✝³ : CharZero R
inst✝² : Ring S
inst✝¹ : Module ℚ S
inst✝ : Module R S
q : ℚ
a : S
⊢ ↑q.den • ↑q • a = ↑q.den • q • a

Tactic:
rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Int.cast_smul_eq_zsmul, ← smul_assoc,
  nsmul_eq_mul q.den, ← cast_natCast, ← cast_mul, den_mul_eq_num, cast_intCast,
  Int.cast_smul_eq_zsmul]

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionRing R
inst✝³ : CharZero R
inst✝² : Ring S
inst✝¹ : Module ℚ S
inst✝ : Module R S
q : ℚ
a : S
⊢ ↑q • a = q • a

Tactic:
refine MulAction.injective₀ (G₀ := ℚ) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_

Result:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionRing R
inst✝³ : CharZero R
inst✝² : Ring S
inst✝¹ : Module ℚ S
inst✝ : Module R S
q : ℚ
a : S
⊢ (fun x => ↑q.den • x) (↑q • a) = (fun x => ↑q.den • x) (q • a)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffineLift_neg (P : W.Point) : (-P).toAffineLift = -P.toAffineLift

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : W.Point
⊢ (-P).toAffineLift = -P.toAffineLift

Tactic:
rcases P with @⟨⟨_⟩, hP⟩

Result:
case mk.mk
F : Type u
inst✝ : Field F
W : Jacobian F
point✝ : PointClass F
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ (-mk hP).toAffineLift = -(mk hP).toAffineLift

Proof state:
case mk.mk
F : Type u
inst✝ : Field F
W : Jacobian F
point✝ : PointClass F
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ (-mk hP).toAffineLift = -(mk hP).toAffineLift

Tactic:
exact toAffine_neg hP

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
/-- The p-adic valuation of `n` is less than or equal to its logarithm w.r.t `p`. -/
lemma padicValNat_le_nat_log (n : ℕ) : padicValNat p n ≤ Nat.log p n

Proof state:
case zero
p : ℕ
⊢ padicValNat p 0 ≤ log p 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.succ.zero
n : ℕ
⊢ padicValNat (0 + 1) (n + 1) ≤ log (0 + 1) (n + 1)

Tactic:
simp

Result:
no goals

Proof state:
case succ
p n : ℕ
⊢ padicValNat p (n + 1) ≤ log p (n + 1)

Tactic:
rcases p with _ | _ | p

Result:
case succ.zero
n : ℕ
⊢ padicValNat 0 (n + 1) ≤ log 0 (n + 1)

case succ.succ.zero
n : ℕ
⊢ padicValNat (0 + 1) (n + 1) ≤ log (0 + 1) (n + 1)

case succ.succ.succ
n p : ℕ
⊢ padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)

Proof state:
case succ.succ.succ
n p : ℕ
⊢ padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)

Tactic:
exact Nat.le_log_of_pow_le p.one_lt_succ_succ (le_of_dvd n.succ_pos pow_padicValNat_dvd)

Result:
no goals

Proof state:
case succ.zero
n : ℕ
⊢ padicValNat 0 (n + 1) ≤ log 0 (n + 1)

Tactic:
simp

Result:
no goals

Proof state:
p n : ℕ
⊢ padicValNat p n ≤ log p n

Tactic:
rcases n with _ | n

Result:
case zero
p : ℕ
⊢ padicValNat p 0 ≤ log p 0

case succ
p n : ℕ
⊢ padicValNat p (n + 1) ≤ log p (n + 1)
-- Mathlib/Data/Set/Prod.lean
theorem pi_eq_empty (hs : i ∈ s) (ht : t i = ∅) : s.pi t = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ f i ∉ t i

Tactic:
simp [ht]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
⊢ s.pi t = ∅

Tactic:
ext f

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ f ∈ s.pi t ↔ f ∈ ∅

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ ∃ x, ∃ (_ : x ∈ s), f x ∉ t x

Tactic:
exact ⟨i, hs, by simp [ht]⟩

Result:
no goals

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ f ∈ s.pi t ↔ f ∈ ∅

Tactic:
simp only [mem_empty_iff_false, not_forall, iff_false, mem_pi, Classical.not_imp]

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ ∃ x, ∃ (_ : x ∈ s), f x ∉ t x
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem isOpen_iff_dist (s : Set (∀ n, E n)) :
    IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Tactic:
constructor

Result:
case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ IsOpen s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ (∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s) → IsOpen s
-- Mathlib/Topology/Separation/Basic.lean
theorem T0Space.of_cover (h : ∀ x y, Inseparable x y → ∃ s : Set X, x ∈ s ∧ y ∈ s ∧ T0Space s) :
    T0Space X

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
⊢ T0Space X

Tactic:
refine ⟨fun x y hxy => ?_⟩

Result:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : X
hxy : Inseparable x y
⊢ x = y

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set X
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable x y
⊢ ↑x = ↑y

Tactic:
exact congr_arg Subtype.val hxy.eq

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : X
hxy : Inseparable x y
⊢ x = y

Tactic:
rcases h x y hxy with ⟨s, hxs, hys, hs⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : X
hxy : Inseparable x y
s : Set X
hxs : x ∈ s
hys : y ∈ s
hs : T0Space ↑s
⊢ x = y

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : X
hxy : Inseparable x y
s : Set X
hxs : x ∈ s
hys : y ∈ s
hs : T0Space ↑s
⊢ x = y

Tactic:
lift x to s using hxs

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
y : X
s : Set X
hys : y ∈ s
hs : T0Space ↑s
x : { x // x ∈ s }
hxy : Inseparable (↑x) y
⊢ ↑x = y

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set X
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable ↑x ↑y
⊢ ↑x = ↑y

Tactic:
rw [← subtype_inseparable_iff] at hxy

Result:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set X
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable x y
⊢ ↑x = ↑y

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
y : X
s : Set X
hys : y ∈ s
hs : T0Space ↑s
x : { x // x ∈ s }
hxy : Inseparable (↑x) y
⊢ ↑x = y

Tactic:
lift y to s using hys

Result:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set X
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable ↑x ↑y
⊢ ↑x = ↑y
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem integrable_iff_integrableAtFilter_atBot_atTop [LinearOrder X] [CompactIccSpace X] :
    Integrable f μ ↔
    (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ

Proof state:
case mpr
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩

Result:
case mpr
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ

Proof state:
case mpr
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ

Tactic:
exact (IntegrableAtFilter.sup_iff.mpr h.1).filter_mono cocompact_le_atBot_atTop

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ Integrable f μ ↔ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ

Tactic:
constructor

Result:
case mp
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ Integrable f μ → (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ

case mpr
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ

Proof state:
case mp
X : Type u_1
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ Integrable f μ → (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ

Tactic:
exact fun hf ↦ ⟨⟨hf.integrableAtFilter _, hf.integrableAtFilter _⟩, hf.locallyIntegrable⟩

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
theorem withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [SigmaFinite μ]
    (h : s ≪ᵥ μ.toENNRealVectorMeasure) : μ.withDensityᵥ (s.rnDeriv μ) = s

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.withDensityᵥ (s.rnDeriv μ)) i = ↑s i

Tactic:
rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub,
  setIntegral_toReal_rnDeriv h.1 i, setIntegral_toReal_rnDeriv h.2 i]

Result:
case h
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ (s.toJordanDecomposition.posPart i).toReal - (s.toJordanDecomposition.negPart i).toReal = ↑s i

case h.hf
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x => (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) (μ.restrict i)

case h.hg
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x => (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) (μ.restrict i)

Proof state:
case h.hg.refine_2
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in Set.univ, s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ⊤

Tactic:
rw [setLIntegral_univ]

Result:
case h.hg.refine_2
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ⊤
-- Mathlib/NumberTheory/Modular.lean
theorem smul_eq_lcRow0_add {p : Fin 2 → ℤ} (hp : IsCoprime (p 0) (p 1)) (hg : g 1 = p) :
    ↑(g • z) =
      (lcRow0 p ↑(g : SL(2, ℝ)) : ℂ) / ((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) +
        ((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1))

Proof state:
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ (↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))) =
    ((↑(p 0) * ↑(↑g 0 0) + ↑(p 1) * ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1))) +
        (↑(p 1) * ↑z - ↑(p 0)) * (↑(p 0) ^ 2 + ↑(p 1) ^ 2)) *
      denom (↑g) z

Tactic:
rw [(by simp :
  (p 1 : ℂ) * z - p 0 = (p 1 * z - p 0) * ↑(Matrix.det (↑g : Matrix (Fin 2) (Fin 2) ℤ)))]

Result:
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ (↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))) =
    ((↑(p 0) * ↑(↑g 0 0) + ↑(p 1) * ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1))) +
        (↑(p 1) * ↑z - ↑(p 0)) * ↑(↑g).det * (↑(p 0) ^ 2 + ↑(p 1) ^ 2)) *
      denom (↑g) z

Proof state:
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ ↑(p 1) * ↑z - ↑(p 0) = (↑(p 1) * ↑z - ↑(p 0)) * ↑(↑g).det

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem getLast?_filter (p : α → Bool) (l : List α) : (l.filter p).getLast? = l.reverse.find? p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p l).reverse.head? = find? p l.reverse

Tactic:
simp [← filter_reverse]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p l).getLast? = find? p l.reverse

Tactic:
rw [getLast?_eq_head?_reverse]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p l).reverse.head? = find? p l.reverse
-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem diagramNatTrans_id (X : C) (P : Cᵒᵖ ⥤ D) :
    J.diagramNatTrans (𝟙 P) X = 𝟙 (J.diagram P X)

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
⊢ (J.diagramNatTrans (𝟙 P) X).app x✝ = (𝟙 (J.diagram P X)).app x✝

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun i => ?_)

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans (𝟙 P) X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i =
    (𝟙 (J.diagram P X)).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans (𝟙 P) X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i =
    (𝟙 (J.diagram P X)).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
⊢ J.diagramNatTrans (𝟙 P) X = 𝟙 (J.diagram P X)

Tactic:
ext : 2

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
⊢ (J.diagramNatTrans (𝟙 P) X).app x✝ = (𝟙 (J.diagram P X)).app x✝
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem le_perfectClosure (L : IntermediateField F E) [h : IsPurelyInseparable F L] :
    L ≤ perfectClosure F E

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : IsPurelyInseparable F ↥L
⊢ L ≤ perfectClosure F E

Tactic:
rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)] at h

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
⊢ L ≤ perfectClosure F E

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
x : E
hx : x ∈ L
⊢ x ∈ perfectClosure F E

Tactic:
obtain ⟨n, y, hy⟩ := h ⟨x, hx⟩

Result:
case intro.intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
x : E
hx : x ∈ L
n : ℕ
y : F
hy : (algebraMap F ↥L) y = ⟨x, hx⟩ ^ ringExpChar F ^ n
⊢ x ∈ perfectClosure F E

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
⊢ L ≤ perfectClosure F E

Tactic:
intro x hx

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
x : E
hx : x ∈ L
⊢ x ∈ perfectClosure F E

Proof state:
case intro.intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
x : E
hx : x ∈ L
n : ℕ
y : F
hy : (algebraMap F ↥L) y = ⟨x, hx⟩ ^ ringExpChar F ^ n
⊢ x ∈ perfectClosure F E

Tactic:
exact ⟨n, y, congr_arg (algebraMap L E) hy⟩

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_add [AddZeroClass α] (d₁ d₂ : n → α) :
    diagonal d₁ + diagonal d₂ = diagonal fun i => d₁ i + d₂ i

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
⊢ diagonal d₁ + diagonal d₂ = diagonal fun i => d₁ i + d₂ i

Tactic:
ext i j

Result:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i => d₁ i + d₂ i) i j

Proof state:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i => d₁ i + d₂ i) i j

Tactic:
by_cases h : i = j <;>
simp [h]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem invOf_eq_inv (x : tsze R M) [Invertible x] : ⅟x = x⁻¹

Proof state:
R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ ⅟x = x⁻¹

Tactic:
ext <;> simp [fst_invOf, snd_invOf]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
⊢ ⅟x = x⁻¹

Tactic:
letI := invertibleFstOfInvertible x

Result:
R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ ⅟x = x⁻¹
-- Mathlib/Data/Set/Function.lean
theorem exists_injOn_iff_injective [Nonempty β] :
    (∃ f : α → β, InjOn f s) ↔ ∃ f : s → β, Injective f :=
  ⟨fun ⟨_, hf⟩ => ⟨_, hf.injective⟩,
   fun ⟨f, hf⟩ => by
    lift f to α → β using trivial
    exact ⟨f, injOn_iff_injective.2 hf⟩⟩

Proof state:
case intro
α : Type u_1
β : Type u_2
s : Set α
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : α → β
hf : Injective fun i => f ↑i
⊢ ∃ f, InjOn f s

Tactic:
exact ⟨f, injOn_iff_injective.2 hf⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : ↑s → β
hf : Injective f
⊢ ∃ f, InjOn f s

Tactic:
lift f to α → β using trivial

Result:
case intro
α : Type u_1
β : Type u_2
s : Set α
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : α → β
hf : Injective fun i => f ↑i
⊢ ∃ f, InjOn f s
-- Mathlib/Algebra/Order/Module/OrderedSMul.lean
lemma inf_eq_half_smul_add_sub_abs_sub (x y : β) : x ⊓ y = (⅟2 : α) • (x + y - |y - x|)

Proof state:
α : Type u_6
β : Type u_7
inst✝⁵ : Semiring α
inst✝⁴ : Invertible 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : AddLeftMono β
x y : β
⊢ x ⊓ y = ⅟2 • (x + y - |y - x|)

Tactic:
rw [← two_nsmul_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul α,
  smul_smul, invOf_mul_self, one_smul]

Result:
no goals