harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem at_one : legendreSym p 1 = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p 1 = 1

Tactic:
rw [legendreSym, Int.cast_one, MulChar.map_one]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Prod.lean
theorem snd_natCast (n : ℕ) : (n : α × β).snd = n

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).2 = ↑n

Tactic:
induction n <;> simp [*]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem LinearOrder.ext {A B : LinearOrder α}
    (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) : A = B

Proof state:
case a.a.a.le.h.h.a
α : Type u_2
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
exact H x y

Result:
no goals

Proof state:
α : Type u_2
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
ext x y

Result:
case a.a.a.le.h.h.a
α : Type u_2
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
-- Mathlib/Order/LiminfLimsup.lean
theorem exists_forall_mem_of_hasBasis_mem_blimsup' {l : Filter β} {b : ι → Set β}
    (hl : l.HasBasis (fun _ => True) b) {u : β → Set α} {p : β → Prop} {x : α}
    (hx : x ∈ blimsup u l p) : ∃ f : ι → β, ∀ i, x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
hl : l.HasBasis (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Tactic:
obtain ⟨f, hf⟩ := exists_forall_mem_of_hasBasis_mem_blimsup hl hx

Result:
case intro
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
hl : l.HasBasis (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
f : ↑{i | True} → β
hf : ∀ (i : ↑{i | True}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Proof state:
case intro
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
hl : l.HasBasis (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
f : ↑{i | True} → β
hf : ∀ (i : ↑{i | True}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Tactic:
exact ⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_eq_self {l : Vector α n} {p : α → Prop} {hp : ∀ (a : α), a ∈ l → p a}
    {f : (a : α) → p a → α} : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a

Proof state:
α : Type u_1
n : Nat
l : Vector α n
p : α → Prop
hp : ∀ (a : α), a ∈ l → p a
f : (a : α) → p a → α
⊢ pmap f l hp = l ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
p : α → Prop
f : (a : α) → p a → α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
hp : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } hp =
      { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    ∀ (a : α) (h : a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }), f a ⋯ = a

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Prop
f : (a : α) → p a → α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
hp : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } hp =
      { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    ∀ (a : α) (h : a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }), f a ⋯ = a

Tactic:
simp [Array.pmap_eq_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_inj {x y : BitVec w} : ~~~x = ~~~y ↔ x = y :=
  ⟨fun h => by rw [← @not_not w x, ← @not_not w y, h], congrArg _⟩

Proof state:
w : Nat
x y : BitVec w
h : ~~~x = ~~~y
⊢ x = y

Tactic:
rw [← @not_not w x, ← @not_not w y, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_eq_empty_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
    l.mapFinIdx f = #[] ↔ l = #[]

Proof state:
case mk
α : Type u_1
β : Type u_2
toList✝ : List α
f : (i : Nat) → α → i < { toList := toList✝ }.size → β
⊢ { toList := toList✝ }.mapFinIdx f = #[] ↔ { toList := toList✝ } = #[]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ l.mapFinIdx f = #[] ↔ l = #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
toList✝ : List α
f : (i : Nat) → α → i < { toList := toList✝ }.size → β
⊢ { toList := toList✝ }.mapFinIdx f = #[] ↔ { toList := toList✝ } = #[]
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem map_comap_bracket_eq {J₁ J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) :
    map f ⁅comap f J₁, comap f J₂⁆ = ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ ≤ f.idealRange

Tactic:
exact le_trans (LieSubmodule.lie_le_left _ _) inf_le_left

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ map f ⁅comap f J₁, comap f J₂⁆ = ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆

Tactic:
rw [← map_sup_ker_eq_map, ← comap_bracket_eq h, map_comap_eq h, inf_eq_right]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ ≤ f.idealRange
-- Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
@[reassoc (attr := simp)]
lemma comm (i j : ι) :
    f ψ i ≫ L.d i j = K.d (e.f i) (e.f j) ≫ f ψ j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
i j : ι
⊢ (ψ.f (e.f i) ≫ (L.extendXIso e ⋯).hom) ≫ L.d i j = K.d (e.f i) (e.f j) ≫ ψ.f (e.f j) ≫ (L.extendXIso e ⋯).hom

Tactic:
simp only [assoc, ← ψ.comm_assoc, L.extend_d_eq e rfl rfl, Iso.inv_hom_id, comp_id]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
i j : ι
⊢ f ψ i ≫ L.d i j = K.d (e.f i) (e.f j) ≫ f ψ j

Tactic:
dsimp [f]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
i j : ι
⊢ (ψ.f (e.f i) ≫ (L.extendXIso e ⋯).hom) ≫ L.d i j = K.d (e.f i) (e.f j) ≫ ψ.f (e.f j) ≫ (L.extendXIso e ⋯).hom
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem mul_le_nndist (hf : AntilipschitzWith K f) (x y : α) :
    K⁻¹ * nndist x y ≤ nndist (f x) (f y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ K⁻¹ * nndist x y ≤ nndist (f x) (f y)

Tactic:
simpa only [div_eq_inv_mul] using NNReal.div_le_of_le_mul' (hf.le_mul_nndist x y)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
    elem a as = decide (a ∈ as)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
⊢ elem a as = decide (a ∈ as)

Tactic:
rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem prime_p : Prime (p : ℤ_[p])

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (maximalIdeal ℤ_[p]).IsPrime

Tactic:
infer_instance

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0

Tactic:
exact NeZero.ne _

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Prime ↑p

Tactic:
rw [← Ideal.span_singleton_prime, ← maximalIdeal_eq_span_p]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (maximalIdeal ℤ_[p]).IsPrime

p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegrable_iff' [NoAtoms μ] :
    IntervalIntegrable f μ a b ↔ IntegrableOn f (uIcc a b) μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
inst✝ : NoAtoms μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f [[a, b]] μ

Tactic:
rw [intervalIntegrable_iff, ← Icc_min_max, uIoc, integrableOn_Icc_iff_integrableOn_Ioc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffine_of_equiv {P Q : Fin 3 → F} (h : P ≈ Q) : toAffine W P = toAffine W Q

Proof state:
case intro
F : Type u
inst✝ : Field F
W : Jacobian F
Q : Fin 3 → F
u : Fˣ
⊢ toAffine W ((fun m => m • Q) u) = toAffine W Q

Tactic:
exact toAffine_smul Q u.isUnit

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
h : P ≈ Q
⊢ toAffine W P = toAffine W Q

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
F : Type u
inst✝ : Field F
W : Jacobian F
Q : Fin 3 → F
u : Fˣ
⊢ toAffine W ((fun m => m • Q) u) = toAffine W Q
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem length_splitWrtCompositionAux (l : List α) (ns) :
    length (l.splitWrtCompositionAux ns) = ns.length

Proof state:
case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), (l.splitWrtCompositionAux tail✝).length = tail✝.length
l : List α
⊢ (l.splitWrtCompositionAux (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Tactic:
simp [*]

Result:
no goals

Proof state:
case nil
α : Type u_1
l : List α
⊢ (l.splitWrtCompositionAux []).length = [].length

Tactic:
simp [splitWrtCompositionAux, *]

Result:
no goals

Proof state:
α : Type u_1
l : List α
ns : List ℕ
⊢ (l.splitWrtCompositionAux ns).length = ns.length

Tactic:
induction ns generalizing l

Result:
case nil
α : Type u_1
l : List α
⊢ (l.splitWrtCompositionAux []).length = [].length

case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), (l.splitWrtCompositionAux tail✝).length = tail✝.length
l : List α
⊢ (l.splitWrtCompositionAux (head✝ :: tail✝)).length = (head✝ :: tail✝).length
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma max_div_min_eq_mabs (a b : α) : max a b / min a b = |b / a|ₘ

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ (a ⊔ b) / (a ⊓ b) = mabs (b / a)

Tactic:
rw [mabs_div_comm, max_div_min_eq_mabs']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
theorem map_π_preserves_coequalizer_inv_colimMap {X' Y' : D} (f' g' : X' ⟶ Y')
    [HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : G.map f ≫ q = p ≫ f')
    (wg : G.map g ≫ q = p ≫ g') :
    G.map (coequalizer.π f g) ≫
        (PreservesCoequalizer.iso G f g).inv ≫
          colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) =
      q ≫ coequalizer.π f' g'

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
⊢ G.map (coequalizer.π f g) ≫
      (PreservesCoequalizer.iso G f g).inv ≫ colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) =
    q ≫ coequalizer.π f' g'

Tactic:
rw [← Category.assoc, map_π_preserves_coequalizer_inv, ι_colimMap, parallelPairHom_app_one]

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem curry_id_eq_coev : curry (𝟙 _) = (ihom.coev A).app X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X : C
inst✝ : Closed A
⊢ curry (𝟙 (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X

Tactic:
rw [curry_eq, (ihom A).map_id (A ⊗ _)]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X : C
inst✝ : Closed A
⊢ (ihom.coev A).app ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X : C
inst✝ : Closed A
⊢ (ihom.coev A).app ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X

Tactic:
apply comp_id

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_univ : dens (univ : Finset α) = 1

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ univ.dens = 1

Tactic:
simp [dens, card_univ]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean
theorem structuralIsoOfExpr_whiskerLeft (f : C) {g h : C}
    (η : g ⟶ h) (η' : g ≅ h) (ih_η : η'.hom = η)  :
    (whiskerLeftIso f η').hom = f ◁ η

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η : g ⟶ h
η' : g ≅ h
ih_η : η'.hom = η
⊢ (whiskerLeftIso f η').hom = f ◁ η

Tactic:
simp [ih_η]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_mkArray {β} (f : α → Vector β m) : (mkVector n a).flatMap f = (mkVector n (f a)).flatten

Proof state:
case h
α : Type u_1
m n : Nat
a : α
β : Type u_2
f : α → Vector β m
i : Nat
h : i < n * m
⊢ ((mkVector n a).flatMap f)[i] = (mkVector n (f a)).flatten[i]

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
m n : Nat
a : α
β : Type u_2
f : α → Vector β m
⊢ (mkVector n a).flatMap f = (mkVector n (f a)).flatten

Tactic:
ext i h

Result:
case h
α : Type u_1
m n : Nat
a : α
β : Type u_2
f : α → Vector β m
i : Nat
h : i < n * m
⊢ ((mkVector n a).flatMap f)[i] = (mkVector n (f a)).flatten[i]
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_eq_of_add_equiv_zero {f g : PadicSeq p} (h : f + g ≈ 0) : f.norm = g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝¹ : (f + g - 0).LimZero
this✝ : f ≈ -g
this : f.norm = (-g).norm
⊢ f.norm = g.norm

Tactic:
simpa only [norm_neg] using this

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
⊢ f.norm = g.norm

Tactic:
have : LimZero (f + g - 0) := h

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : (f + g - 0).LimZero
⊢ f.norm = g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : (f + g - 0).LimZero
⊢ LimZero (f - -g)

Tactic:
simpa only [sub_zero, sub_neg_eq_add]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝ : (f + g - 0).LimZero
this : f ≈ -g
⊢ f.norm = g.norm

Tactic:
have : f.norm = (-g).norm := norm_equiv this

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝¹ : (f + g - 0).LimZero
this✝ : f ≈ -g
this : f.norm = (-g).norm
⊢ f.norm = g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : (f + g - 0).LimZero
⊢ f.norm = g.norm

Tactic:
have : f ≈ -g := show LimZero (f - -g) by simpa only [sub_zero, sub_neg_eq_add]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝ : (f + g - 0).LimZero
this : f ≈ -g
⊢ f.norm = g.norm
-- Mathlib/Probability/Independence/Basic.lean
lemma IndepFun_iff {β γ} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ]
    (f : Ω → β) (g : Ω → γ) (μ : Measure Ω) :
    IndepFun f g μ ↔ ∀ t1 t2, MeasurableSet[MeasurableSpace.comap f mβ] t1
      → MeasurableSet[MeasurableSpace.comap g mγ] t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Proof state:
Ω : Type u_1
x✝ : MeasurableSpace Ω
β : Type u_6
γ : Type u_7
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
⊢ IndepFun f g μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Tactic:
rw [IndepFun_iff_Indep, Indep_iff]

Result:
no goals
-- Mathlib/Algebra/Module/Equiv/Defs.lean
theorem symm_trans_self (f : M₁ ≃ₛₗ[σ₁₂] M₂) : f.symm.trans f = LinearEquiv.refl R₂ M₂

Proof state:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_7
M₂ : Type u_8
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
⊢ f.symm.trans f = refl R₂ M₂

Tactic:
ext x

Result:
case h
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_7
M₂ : Type u_8
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
x : M₂
⊢ (f.symm.trans f) x = (refl R₂ M₂) x

Proof state:
case h
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_7
M₂ : Type u_8
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
x : M₂
⊢ (f.symm.trans f) x = (refl R₂ M₂) x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem X_mul_divX_add (p : R[X]) : X * divX p + C (p.coeff 0) = p :=
  ext <| by rintro ⟨_ | _⟩ <;> simp [coeff_C, Nat.succ_ne_zero, coeff_mul_X]

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (X * p.divX + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
rintro ⟨_ | _⟩ <;> simp [coeff_C, Nat.succ_ne_zero, coeff_mul_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {fallback v : β} :
    getD (m.insertIfNew k v) a fallback =
      if k == a ∧ m.contains k = false then v else getD m a fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
fallback v : β
⊢ getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ m.contains k = false then v else getD m a fallback

Tactic:
simp_to_model [insertIfNew] using List.getValueD_insertEntryIfNew

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/--
Checking AB* of shape `Discrete ℕ` is enough for countable AB4*, provided that the category has
finite biproducts and finite colimits.
-/
lemma CountableAB4Star.of_hasExactLimitsOfShape_nat [HasFiniteColimits C]
    [HasCountableProducts C] [HasExactLimitsOfShape (Discrete ℕ) C] : CountableAB4Star C

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteColimits C
inst✝¹ : HasCountableProducts C
inst✝ : HasExactLimitsOfShape (Discrete ℕ) C
⊢ CountableAB4Star C

Tactic:
apply (config := { allowSynthFailures := true })
    CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite

Result:
case inst
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteColimits C
inst✝¹ : HasCountableProducts C
inst✝ : HasExactLimitsOfShape (Discrete ℕ) C
⊢ ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C

Proof state:
case inst
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteColimits C
inst✝¹ : HasCountableProducts C
inst✝ : HasExactLimitsOfShape (Discrete ℕ) C
⊢ ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C

Tactic:
exact fun _ ↦ inferInstance

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem beth_one : ℶ_ 1 = 𝔠

Proof state:
⊢ ℶ_ 1 = 𝔠

Tactic:
simpa using beth_succ 0

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_pow_self (n : ℕ) :
    count K v ((v.asIdeal : FractionalIdeal R⁰ K) ^ n) = n

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℕ
⊢ count K v (↑v.asIdeal ^ n) = ↑n

Tactic:
rw [count_pow, count_self, mul_one]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
lemma zeroLocus_smul_of_isUnit {r : R} (hr : IsUnit r) (s : Set R) :
    zeroLocus (r • s) = zeroLocus s

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
r : R
hr : IsUnit r
s : Set R
x✝ : PrimeSpectrum R
⊢ x✝ ∈ zeroLocus (r • s) ↔ x✝ ∈ zeroLocus s

Tactic:
simp [Set.subset_def, ← Set.image_smul, Ideal.unit_mul_mem_iff_mem _ hr]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
r : R
hr : IsUnit r
s : Set R
⊢ zeroLocus (r • s) = zeroLocus s

Tactic:
ext

Result:
case h
R : Type u
inst✝ : CommSemiring R
r : R
hr : IsUnit r
s : Set R
x✝ : PrimeSpectrum R
⊢ x✝ ∈ zeroLocus (r • s) ↔ x✝ ∈ zeroLocus s
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integrable_cexp_neg_sum_mul_add {ι : Type*} [Fintype ι] {b : ι → ℂ}
    (hb : ∀ i, 0 < (b i).re) (c : ι → ℂ) :
    Integrable (fun (v : ι → ℝ) ↦ cexp (- ∑ i, b i * (v i : ℂ) ^ 2 + ∑ i, c i * v i))

Proof state:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ Integrable (fun v => ∏ x : ι, cexp (-b x * ↑(v x) ^ 2 + c x * ↑(v x))) volume

Tactic:
apply Integrable.fintype_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v^2 + c i * v)) (fun i ↦ ?_)

Result:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ Integrable ((fun i v => cexp (-b i * ↑v ^ 2 + c i * ↑v)) i) volume

Proof state:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ Integrable (fun v => cexp (-∑ i : ι, b i * ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i))) volume

Tactic:
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]

Result:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ Integrable (fun v => ∏ x : ι, cexp (-b x * ↑(v x) ^ 2 + c x * ↑(v x))) volume

Proof state:
case h.e'_6.h.h.e'_1
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
x : ℝ
⊢ -b i * ↑x ^ 2 + c i * ↑x = -b i * ↑x ^ 2 + c i * ↑x + 0

Tactic:
simp only [add_zero]

Result:
no goals

Proof state:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ Integrable ((fun i v => cexp (-b i * ↑v ^ 2 + c i * ↑v)) i) volume

Tactic:
convert integrable_cexp_quadratic (hb i) (c i) 0 using 3 with x

Result:
case h.e'_6.h.h.e'_1
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
x : ℝ
⊢ -b i * ↑x ^ 2 + c i * ↑x = -b i * ↑x ^ 2 + c i * ↑x + 0
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma div_sq_cancel (a b : G₀) : a ^ 2 * b / a = a * b

Proof state:
case inr
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a ^ 2 * b / a = a * b

Tactic:
rw [sq, mul_assoc, mul_div_cancel_left₀ _ ha]

Result:
no goals

Proof state:
case inl
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
b : G₀
⊢ 0 ^ 2 * b / 0 = 0 * b

Tactic:
simp

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
⊢ a ^ 2 * b / a = a * b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
b : G₀
⊢ 0 ^ 2 * b / 0 = 0 * b

case inr
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a ^ 2 * b / a = a * b
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem transReflReparamAux_mem_I (t : I) : transReflReparamAux t ∈ I

Proof state:
t : ↑I
⊢ transReflReparamAux t ∈ I

Tactic:
unfold transReflReparamAux

Result:
t : ↑I
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) ∈ I

Proof state:
t : ↑I
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) ∈ I

Tactic:
split_ifs <;> constructor <;> linarith [unitInterval.le_one t, unitInterval.nonneg t]

Result:
no goals