harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Perm/Basic.lean
theorem flatMap_append_perm (l : List α) (f g : α → List β) :
    l.flatMap f ++ l.flatMap g ~ l.flatMap fun x => f x ++ g x

Proof state:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x => f x ++ g x) l
⊢ flatMap f l ++ (g a ++ flatMap g l) ~ g a ++ (flatMap f l ++ flatMap g l)

Tactic:
rw [← append_assoc, ← append_assoc]

Result:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x => f x ++ g x) l
⊢ flatMap f l ++ g a ++ flatMap g l ~ g a ++ flatMap f l ++ flatMap g l

Proof state:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x => f x ++ g x) l
⊢ f a ++ (flatMap f l ++ (g a ++ flatMap g l)) ~ f a ++ (g a ++ flatMap (fun x => f x ++ g x) l)

Tactic:
refine (Perm.trans ?_ (IH.append_left _)).append_left _

Result:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x => f x ++ g x) l
⊢ flatMap f l ++ (g a ++ flatMap g l) ~ g a ++ (flatMap f l ++ flatMap g l)

Proof state:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x => f x ++ g x) l
⊢ flatMap f l ++ g a ++ flatMap g l ~ g a ++ flatMap f l ++ flatMap g l

Tactic:
exact perm_append_comm.append_right _

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x => f x ++ g x) l
⊢ flatMap f (a :: l) ++ flatMap g (a :: l) ~ flatMap (fun x => f x ++ g x) (a :: l)

Tactic:
simp only [flatMap_cons, append_assoc]

Result:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x => f x ++ g x) l
⊢ f a ++ (flatMap f l ++ (g a ++ flatMap g l)) ~ f a ++ (g a ++ flatMap (fun x => f x ++ g x) l)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
⊢ flatMap f l ++ flatMap g l ~ flatMap (fun x => f x ++ g x) l

Tactic:
induction' l with a l IH

Result:
case nil
α : Type u_1
β : Type u_2
f g : α → List β
⊢ flatMap f [] ++ flatMap g [] ~ flatMap (fun x => f x ++ g x) []

case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x => f x ++ g x) l
⊢ flatMap f (a :: l) ++ flatMap g (a :: l) ~ flatMap (fun x => f x ++ g x) (a :: l)

Proof state:
case nil
α : Type u_1
β : Type u_2
f g : α → List β
⊢ flatMap f [] ++ flatMap g [] ~ flatMap (fun x => f x ++ g x) []

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem pred_lt_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
    a.pred ha < b.pred hb ↔ a < b

Proof state:
n : Nat
a b : Fin n.succ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.pred ha < b.pred hb ↔ a < b

Tactic:
rw [← succ_lt_succ_iff, succ_pred, succ_pred]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_sup_le_lift {ι} {f : ι → Ordinal} (H : ∀ i, f i < sup.{u, v} f) :
    cof (sup.{u, v} f) ≤ Cardinal.lift.{v, u} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
H : sup f = lsub f
⊢ (lsub f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
exact cof_lsub_le_lift f

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < sup f
⊢ (sup f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [← sup_eq_lsub_iff_lt_sup.{u, v}] at H

Result:
ι : Type u
f : ι → Ordinal.{max u v}
H : sup f = lsub f
⊢ (sup f).cof ≤ Cardinal.lift.{v, u} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
H : sup f = lsub f
⊢ (sup f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [H]

Result:
ι : Type u
f : ι → Ordinal.{max u v}
H : sup f = lsub f
⊢ (lsub f).cof ≤ Cardinal.lift.{v, u} #ι
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = ↑m - ↑n

Proof state:
case hn
m n✝ i n : Nat
⊢ -↑i + -↑1 = ↑n + -↑n + -↑i + -↑1

Tactic:
rw [← @Int.sub_eq_add_neg n, ← ofNat_sub, Nat.sub_self, ofNat_zero, Int.zero_add]

Result:
case hn
m n✝ i n : Nat
⊢ n ≤ n

Proof state:
case hn
m n✝ i n : Nat
⊢ n ≤ n

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
case hn
m n✝ i n : Nat
⊢ -[i+1] = ↑n - ↑(n + i + 1)

Tactic:
simp only [negSucc_coe, ofNat_add, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]

Result:
case hn
m n✝ i n : Nat
⊢ -↑i + -↑1 = ↑n + -↑n + -↑i + -↑1

Proof state:
case hp
m n : Nat
⊢ ∀ (i n : Nat), ↑i = ↑(n + i) - ↑n

Tactic:
intros i n

Result:
case hp
m n✝ i n : Nat
⊢ ↑i = ↑(n + i) - ↑n

Proof state:
case hn
m n : Nat
⊢ ∀ (i m : Nat), -[i+1] = ↑m - ↑(m + i + 1)

Tactic:
intros i n

Result:
case hn
m n✝ i n : Nat
⊢ -[i+1] = ↑n - ↑(n + i + 1)

Proof state:
case hp
m n✝ i n : Nat
⊢ ↑i = ↑(n + i) - ↑n

Tactic:
rw [Int.ofNat_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm,
  Int.add_right_neg, Int.add_zero]

Result:
no goals

Proof state:
m n : Nat
⊢ subNatNat m n = ↑m - ↑n

Tactic:
apply subNatNat_elim m n fun m n i => i = m - n

Result:
case hp
m n : Nat
⊢ ∀ (i n : Nat), ↑i = ↑(n + i) - ↑n

case hn
m n : Nat
⊢ ∀ (i m : Nat), -[i+1] = ↑m - ↑(m + i + 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_eq' {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ x, x ∈ xs ∧ p x)

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.any p = false
⊢ false = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simp only [any_eq_false'] at h

Result:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ∀ (x : α), x ∈ xs → ¬p x = true
⊢ false = decide (∃ x, x ∈ xs ∧ p x = true)

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.any p = false
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simp only [h]

Result:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.any p = false
⊢ false = decide (∃ x, x ∈ xs ∧ p x = true)

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
by_cases h : xs.any p

Result:
case pos
α : Type u_1
xs : Array α
p : α → Bool
h : xs.any p = true
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ¬xs.any p = true
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Proof state:
case pos
α : Type u_1
xs : Array α
p : α → Bool
h : xs.any p = true
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simp_all [any_eq_true', -any_eq_true]

Result:
no goals

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ∀ (x : α), x ∈ xs → ¬p x = true
⊢ false = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simpa using h

Result:
no goals

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ¬xs.any p = true
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simp only [Bool.not_eq_true] at h

Result:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.any p = false
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_smul_right_of_tower (a : S) (x y : M) : polar Q x (a • y) = a • polar Q x y

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
a : S
x y : M
⊢ polar (⇑Q) x (a • y) = a • polar (⇑Q) x y

Tactic:
rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, algebraMap_smul]

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem UpperSemicontinuousAt.add' {f g : α → γ} (hf : UpperSemicontinuousAt f x)
    (hg : UpperSemicontinuousAt g x)
    (hcont : ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
    UpperSemicontinuousAt (fun z => f z + g z) x

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
hf : UpperSemicontinuousWithinAt f univ x
hg : UpperSemicontinuousWithinAt g univ x
⊢ UpperSemicontinuousWithinAt (fun z => f z + g z) univ x

Tactic:
exact hf.add' hg hcont

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : UpperSemicontinuousAt f x
hg : UpperSemicontinuousAt g x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
⊢ UpperSemicontinuousAt (fun z => f z + g z) x

Tactic:
simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
hf : UpperSemicontinuousWithinAt f univ x
hg : UpperSemicontinuousWithinAt g univ x
⊢ UpperSemicontinuousWithinAt (fun z => f z + g z) univ x
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem wordProd_reverse (ω : List B) : π (reverse ω) = (π ω)⁻¹

Proof state:
case nil
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.wordProd [].reverse = (cs.wordProd [])⁻¹

Tactic:
simp

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.wordProd ω.reverse = (cs.wordProd ω)⁻¹

Tactic:
induction' ω with x ω' ih

Result:
case nil
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.wordProd [].reverse = (cs.wordProd [])⁻¹

case cons
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
x : B
ω' : List B
ih : cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹
⊢ cs.wordProd (x :: ω').reverse = (cs.wordProd (x :: ω'))⁻¹

Proof state:
case cons
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
x : B
ω' : List B
ih : cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹
⊢ cs.wordProd (x :: ω').reverse = (cs.wordProd (x :: ω'))⁻¹

Tactic:
simpa [wordProd_cons, wordProd_append] using ih

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
lemma isPullback_map {S T : Scheme.{max u v}} (f : S ⟶ T) :
    IsPullback (map n f) (𝔸(n; S) ↘ S) (𝔸(n; T) ↘ T) f

Proof state:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n]))) (𝔸(n; S) ↘ S)
    (terminal.from (Spec ℤ[n])) (f ≫ terminal.from T)

Tactic:
simp only [terminal.comp_from, ]

Result:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n]))) (𝔸(n; S) ↘ S)
    (terminal.from (Spec ℤ[n])) (terminal.from S)

Proof state:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n]))) (𝔸(n; S) ↘ S)
    (terminal.from (Spec ℤ[n])) (terminal.from S)

Tactic:
convert (IsPullback.of_hasPullback _ _).flip

Result:
case h.e'_7.h
n : Type v
S T : Scheme
f : S ⟶ T
e_3✝ : 𝔸(n; S) = pullback (terminal.from S) (terminal.from (Spec ℤ[n]))
⊢ map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])) =
    pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))

Proof state:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f) (𝔸(n; S) ↘ S) (𝔸(n; T) ↘ T) f

Tactic:
refine (IsPullback.paste_horiz_iff (.flip <| .of_hasPullback _ _) (map_over f)).mp ?_

Result:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n]))) (𝔸(n; S) ↘ S)
    (terminal.from (Spec ℤ[n])) (f ≫ terminal.from T)

Proof state:
case h.e'_7.h
n : Type v
S T : Scheme
f : S ⟶ T
e_3✝ : 𝔸(n; S) = pullback (terminal.from S) (terminal.from (Spec ℤ[n]))
⊢ map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])) =
    pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))

Tactic:
rw [← toSpecMvPoly, ← toSpecMvPoly, map_toSpecMvPoly]

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Even.mul_odd [HasDistribNeg R] (hf : f.Even) (hg : g.Odd) : (f * g).Odd

Proof state:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Even f
hg : Function.Odd g
a : α
⊢ (f * g) (-a) = -(f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a, mul_neg]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Even f
hg : Function.Odd g
⊢ Function.Odd (f * g)

Tactic:
intro a

Result:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Even f
hg : Function.Odd g
a : α
⊢ (f * g) (-a) = -(f * g) a
-- Mathlib/Topology/Algebra/Module/LinearPMap.lean
theorem closure_def {f : E →ₗ.[R] F} (hf : f.IsClosable) : f.closure = hf.choose

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.closure = Exists.choose hf

Tactic:
simp [closure, hf]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
theorem pullbackIsoPullback_inv_snd :
    (pullbackIsoPullback f g).inv ≫ pullback.snd _ _ = fun p => (p.1 : X × Y).snd

Proof state:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.snd f g = fun p => (↑p).2

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem mem_getLast?_eq_getLast : ∀ {l : List α} {x : α}, x ∈ l.getLast? → ∃ h, x = getLast l h
  | [], x, hx => False.elim <| by simp at hx
  | [a], x, hx =>
    have : a = x

Proof state:
case intro
α : Type u
a b : α
l : List α
x : α
hx : x ∈ (b :: l).getLast?
w✝ : b :: l ≠ []
h₂ : x = (b :: l).getLast w✝
⊢ ∃ h, x = (a :: b :: l).getLast h

Tactic:
use cons_ne_nil _ _

Result:
case h
α : Type u
a b : α
l : List α
x : α
hx : x ∈ (b :: l).getLast?
w✝ : b :: l ≠ []
h₂ : x = (b :: l).getLast w✝
⊢ x = (a :: b :: l).getLast ⋯

Proof state:
α : Type u
a b : α
l : List α
x : α
hx : x ∈ (b :: l).getLast?
⊢ ∃ h, x = (a :: b :: l).getLast h

Tactic:
rcases mem_getLast?_eq_getLast hx with ⟨_, h₂⟩

Result:
case intro
α : Type u
a b : α
l : List α
x : α
hx : x ∈ (b :: l).getLast?
w✝ : b :: l ≠ []
h₂ : x = (b :: l).getLast w✝
⊢ ∃ h, x = (a :: b :: l).getLast h

Proof state:
α : Type u
a b : α
l : List α
x : α
hx : x ∈ (a :: b :: l).getLast?
⊢ ∃ h, x = (a :: b :: l).getLast h

Tactic:
rw [getLast?_cons_cons] at hx

Result:
α : Type u
a b : α
l : List α
x : α
hx : x ∈ (b :: l).getLast?
⊢ ∃ h, x = (a :: b :: l).getLast h

Proof state:
α : Type u
a x : α
hx : x ∈ [a].getLast?
⊢ a = x

Tactic:
simpa using hx

Result:
no goals

Proof state:
case h
α : Type u
a b : α
l : List α
x : α
hx : x ∈ (b :: l).getLast?
w✝ : b :: l ≠ []
h₂ : x = (b :: l).getLast w✝
⊢ x = (a :: b :: l).getLast ⋯

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u
x : α
hx : x ∈ [].getLast?
⊢ False

Tactic:
simp at hx

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_sup : comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂

Proof state:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂

Tactic:
rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
@[simp]
lemma valuation_inv (x : ℚ_[p]) : x⁻¹.valuation = -x.valuation

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0⁻¹.valuation = -valuation 0

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x⁻¹.valuation = -x.valuation

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0⁻¹.valuation = -valuation 0

case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ x⁻¹.valuation = -x.valuation

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ x⁻¹.valuation = -x.valuation

Tactic:
have h_norm : ‖x⁻¹‖ = ‖x‖⁻¹ := norm_inv x

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
⊢ x⁻¹.valuation = -x.valuation

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : ↑p ≠ 1
⊢ x⁻¹.valuation = -x.valuation

Tactic:
have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ x⁻¹.valuation = -x.valuation

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ x⁻¹.valuation = -x.valuation

Tactic:
rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation <| inv_ne_zero hx,
  ← zpow_neg, zpow_right_inj₀ hp_pos hp_ne_one, neg_inj] at h_norm

Result:
no goals

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
⊢ x⁻¹.valuation = -x.valuation

Tactic:
have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : ↑p ≠ 1
⊢ x⁻¹.valuation = -x.valuation
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.eq_prime_pow_mul_coprime [DecidableEq (Ideal T)] {I : Ideal T} (hI : I ≠ ⊥)
    (P : Ideal T) [hpm : P.IsMaximal] :
    ∃ Q : Ideal T, P ⊔ Q = ⊤ ∧ I = P ^ (Multiset.count P (normalizedFactors I)) * Q

Proof state:
case h.left
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
inst✝ : DecidableEq (Ideal T)
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ P ⊔ (filter (fun x => ¬P = x) (normalizedFactors I)).prod = ⊤

Tactic:
refine P.sup_multiset_prod_eq_top (fun p hpi ↦ ?_)

Result:
case h.left
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
inst✝ : DecidableEq (Ideal T)
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
p : Ideal T
hpi : p ∈ filter (fun x => ¬P = x) (normalizedFactors I)
⊢ P ⊔ p = ⊤

Proof state:
case h
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
inst✝ : DecidableEq (Ideal T)
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ P ⊔ (filter (fun x => ¬P = x) (normalizedFactors I)).prod = ⊤ ∧
    I = P ^ count P (normalizedFactors I) * (filter (fun x => ¬P = x) (normalizedFactors I)).prod

Tactic:
constructor

Result:
case h.left
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
inst✝ : DecidableEq (Ideal T)
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ P ⊔ (filter (fun x => ¬P = x) (normalizedFactors I)).prod = ⊤

case h.right
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
inst✝ : DecidableEq (Ideal T)
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ I = P ^ count P (normalizedFactors I) * (filter (fun x => ¬P = x) (normalizedFactors I)).prod

Proof state:
case h.left
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
inst✝ : DecidableEq (Ideal T)
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
p : Ideal T
hpi : p ∈ filter (fun x => ¬P = x) (normalizedFactors I)
⊢ P ⊔ p = ⊤

Tactic:
have hp : Prime p := prime_of_normalized_factor p (filter_subset _ (normalizedFactors I) hpi)

Result:
case h.left
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
inst✝ : DecidableEq (Ideal T)
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
p : Ideal T
hpi : p ∈ filter (fun x => ¬P = x) (normalizedFactors I)
hp : Prime p
⊢ P ⊔ p = ⊤

Proof state:
case h.right
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
inst✝ : DecidableEq (Ideal T)
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ (filter (fun x => P = x) (normalizedFactors I) + filter (fun a => ¬P = a) (normalizedFactors I)).prod =
    P ^ count P (normalizedFactors I) * (filter (fun x => ¬P = x) (normalizedFactors I)).prod

Tactic:
rw [prod_add, pow_count]

Result:
no goals

Proof state:
case h.left
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
inst✝ : DecidableEq (Ideal T)
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
p : Ideal T
hpi : p ∈ filter (fun x => ¬P = x) (normalizedFactors I)
hp : Prime p
⊢ P ⊔ p = ⊤

Tactic:
exact hpm.coprime_of_ne ((isPrime_of_prime hp).isMaximal hp.ne_zero) (of_mem_filter hpi)

Result:
no goals
-- Mathlib/Algebra/Order/CompleteField.lean
theorem cutMap_self (a : α) : cutMap α a = Iio a ∩ range (Rat.cast : ℚ → α)

Proof state:
case h
α : Type u_2
inst✝ : LinearOrderedField α
a x✝ : α
⊢ x✝ ∈ cutMap α a ↔ x✝ ∈ Iio a ∩ range Rat.cast

Tactic:
constructor

Result:
case h.mp
α : Type u_2
inst✝ : LinearOrderedField α
a x✝ : α
⊢ x✝ ∈ cutMap α a → x✝ ∈ Iio a ∩ range Rat.cast

case h.mpr
α : Type u_2
inst✝ : LinearOrderedField α
a x✝ : α
⊢ x✝ ∈ Iio a ∩ range Rat.cast → x✝ ∈ cutMap α a

Proof state:
case h.mp.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a : α
q : ℚ
h : q ∈ {t | ↑t < a}
⊢ ↑q ∈ Iio a ∩ range Rat.cast

Tactic:
exact ⟨h, q, rfl⟩

Result:
no goals

Proof state:
case h.mpr.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a : α
q : ℚ
h : ↑q ∈ Iio a
⊢ ↑q ∈ cutMap α a

Tactic:
exact ⟨q, h, rfl⟩

Result:
no goals

Proof state:
case h.mp
α : Type u_2
inst✝ : LinearOrderedField α
a x✝ : α
⊢ x✝ ∈ cutMap α a → x✝ ∈ Iio a ∩ range Rat.cast

Tactic:
rintro ⟨q, h, rfl⟩

Result:
case h.mp.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a : α
q : ℚ
h : q ∈ {t | ↑t < a}
⊢ ↑q ∈ Iio a ∩ range Rat.cast

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ cutMap α a = Iio a ∩ range Rat.cast

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : LinearOrderedField α
a x✝ : α
⊢ x✝ ∈ cutMap α a ↔ x✝ ∈ Iio a ∩ range Rat.cast

Proof state:
case h.mpr
α : Type u_2
inst✝ : LinearOrderedField α
a x✝ : α
⊢ x✝ ∈ Iio a ∩ range Rat.cast → x✝ ∈ cutMap α a

Tactic:
rintro ⟨h, q, rfl⟩

Result:
case h.mpr.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a : α
q : ℚ
h : ↑q ∈ Iio a
⊢ ↑q ∈ cutMap α a
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem Affine.Simplex.span_eq_top [FiniteDimensional k V] {n : ℕ} (T : Affine.Simplex k V n)
    (hrank : finrank k V = n) : affineSpan k (Set.range T.points) = ⊤

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : FiniteDimensional k V
n : ℕ
T : Simplex k V n
hrank : finrank k V = n
⊢ affineSpan k (Set.range T.points) = ⊤

Tactic:
rw [AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one T.independent,
  Fintype.card_fin, hrank]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Comap.lean
@[simp]
lemma comap_id (μ : Measure β) : comap (fun x ↦ x) μ = μ

Proof state:
case h.hf
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet ((fun x => x) '' s)

case h.hs
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
all_goals simp [*]

Result:
no goals

Proof state:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
⊢ comap (fun x => x) μ = μ

Tactic:
ext s hs

Result:
case h
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ (comap (fun x => x) μ) s = μ s

Proof state:
case h.hs
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
simp [*]

Result:
no goals

Proof state:
case h.hfi
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Injective fun x => x

Tactic:
exact injective_id

Result:
no goals

Proof state:
case h
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ (comap (fun x => x) μ) s = μ s

Tactic:
rw [comap_apply, image_id']

Result:
case h.hfi
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Injective fun x => x

case h.hf
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet ((fun x => x) '' s)

case h.hs
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s