harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma XIsoOfEq_hom_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
    (h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂) :
    (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq (h₁₂.trans h₃₂.symm)).hom

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom

Tactic:
dsimp [XIsoOfEq]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [eqToHom_trans]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem tendsto_div_nhds_one_iff {α : Type*} {l : Filter α} {x : G} {u : α → G} :
    Tendsto (u · / x) l (𝓝 1) ↔ Tendsto u l (𝓝 x) :=
  haveI A : Tendsto (fun _ : α => x) l (𝓝 x) := tendsto_const_nhds
  ⟨fun h => by simpa using h.mul A, fun h => by simpa using h.div' A⟩

Proof state:
G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 => x) l (𝓝 x)
h : Tendsto u l (𝓝 x)
⊢ Tendsto (fun x_1 => u x_1 / x) l (𝓝 1)

Tactic:
simpa using h.div' A

Result:
no goals

Proof state:
G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 => x) l (𝓝 x)
h : Tendsto (fun x_1 => u x_1 / x) l (𝓝 1)
⊢ Tendsto u l (𝓝 x)

Tactic:
simpa using h.mul A

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem support_X_pow [Nontrivial R] (s : σ) (n : ℕ) :
    (X s ^ n : MvPolynomial σ R).support = {Finsupp.single s n}

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ (X s ^ n).support = {Finsupp.single s n}

Tactic:
classical
  rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ (X s ^ n).support = {Finsupp.single s n}

Tactic:
rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem brange_const {o : Ordinal} (ho : o ≠ 0) {c : α} : (brange o fun _ _ => c) = {c}

Proof state:
α : Type u_1
o : Ordinal.{u_4}
ho : o ≠ 0
c : α
⊢ (o.brange fun x x => c) = {c}

Tactic:
rw [← range_familyOfBFamily]

Result:
α : Type u_1
o : Ordinal.{u_4}
ho : o ≠ 0
c : α
⊢ range (o.familyOfBFamily fun x x => c) = {c}

Proof state:
α : Type u_1
o : Ordinal.{u_4}
ho : o ≠ 0
c : α
⊢ range (o.familyOfBFamily fun x x => c) = {c}

Tactic:
exact @Set.range_const _ o.toType (toType_nonempty_iff_ne_zero.2 ho) c

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem self_le_power (a : Cardinal) {b : Cardinal} (hb : 1 ≤ b) : a ≤ a ^ b

Proof state:
a b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ a ≤ a ^ b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b

case inr
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b

Proof state:
case h.e'_3
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a = a ^ 1

Tactic:
exact (power_one a).symm

Result:
no goals

Proof state:
case inr
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b

Tactic:
convert power_le_power_left ha hb

Result:
case h.e'_3
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a = a ^ 1

Proof state:
case inl
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b

Tactic:
exact zero_le _

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma leftHomologyMap'_neg :
    leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂

Tactic:
simp only [γ.leftHomologyMap'_eq, γ.neg.leftHomologyMap'_eq, LeftHomologyMapData.neg_φH]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
@[simp]
lemma ediam_top [Nontrivial α] : (⊤ : SimpleGraph α).ediam = 1

Proof state:
α : Type u_1
inst✝ : Nontrivial α
p : α × α
⊢ ⊤.edist p.1 p.2 ≤ 1

Tactic:
by_cases h : (⊤ : SimpleGraph α).Adj p.1 p.2

Result:
case pos
α : Type u_1
inst✝ : Nontrivial α
p : α × α
h : ⊤.Adj p.1 p.2
⊢ ⊤.edist p.1 p.2 ≤ 1

case neg
α : Type u_1
inst✝ : Nontrivial α
p : α × α
h : ¬⊤.Adj p.1 p.2
⊢ ⊤.edist p.1 p.2 ≤ 1

Proof state:
α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.ediam = 1

Tactic:
apply le_antisymm ?_ <| Order.one_le_iff_pos.mpr <| pos_iff_ne_zero.mpr ediam_ne_zero

Result:
α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.ediam ≤ 1

Proof state:
case pos
α : Type u_1
inst✝ : Nontrivial α
p : α × α
h : ⊤.Adj p.1 p.2
⊢ ⊤.edist p.1 p.2 ≤ 1

Tactic:
apply le_of_eq <| edist_eq_one_iff_adj.mpr h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Nontrivial α
⊢ ∀ (i : α × α), ⊤.edist i.1 i.2 ≤ 1

Tactic:
intro p

Result:
α : Type u_1
inst✝ : Nontrivial α
p : α × α
⊢ ⊤.edist p.1 p.2 ≤ 1

Proof state:
α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.ediam ≤ 1

Tactic:
apply ediam_def ▸ iSup_le_iff.mpr

Result:
α : Type u_1
inst✝ : Nontrivial α
⊢ ∀ (i : α × α), ⊤.edist i.1 i.2 ≤ 1

Proof state:
case neg
α : Type u_1
inst✝ : Nontrivial α
p : α × α
h : ¬⊤.Adj p.1 p.2
⊢ ⊤.edist p.1 p.2 ≤ 1

Tactic:
simp_all

Result:
no goals
-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem step2 (K : Subgroup G) [K.Normal] (hK : K ≤ N) : K = ⊥ ∨ K = N

Proof state:
case intro.refine_2
G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
H : Subgroup (G ⧸ K)
hH : N ≤ K
hH' : comap (QuotientGroup.mk' K) H = comap (QuotientGroup.mk' K) ⊤
⊢ False

Tactic:
exact h4.2 (le_antisymm hK hH)

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists_perm_sublists' (l : List α) : sublists l ~ sublists' l

Proof state:
α : Type u
l : List α
⊢ (finRange l.length).sublists.Nodup

Tactic:
exact nodup_sublists.mpr (nodup_finRange _)

Result:
no goals

Proof state:
case p
α : Type u
l : List α
⊢ (finRange l.length).sublists ~ (finRange l.length).sublists'

Tactic:
apply (perm_ext_iff_of_nodup _ _).mpr

Result:
case p
α : Type u
l : List α
⊢ ∀ (a : List (Fin l.length)), a ∈ (finRange l.length).sublists ↔ a ∈ (finRange l.length).sublists'

α : Type u
l : List α
⊢ (finRange l.length).sublists.Nodup

α : Type u
l : List α
⊢ (finRange l.length).sublists'.Nodup

Proof state:
case p
α : Type u
l : List α
⊢ ∀ (a : List (Fin l.length)), a ∈ (finRange l.length).sublists ↔ a ∈ (finRange l.length).sublists'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ (finRange l.length).sublists'.Nodup

Tactic:
exact (nodup_sublists'.mpr (nodup_finRange _))

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ map (map l.get) (finRange l.length).sublists ~ map (map l.get) (finRange l.length).sublists'

Tactic:
apply Perm.map

Result:
case p
α : Type u
l : List α
⊢ (finRange l.length).sublists ~ (finRange l.length).sublists'

Proof state:
α : Type u
l : List α
⊢ l.sublists ~ l.sublists'

Tactic:
rw [← finRange_map_get l, sublists_map, sublists'_map]

Result:
α : Type u
l : List α
⊢ map (map l.get) (finRange l.length).sublists ~ map (map l.get) (finRange l.length).sublists'
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_sum_subset [DecidableEq σ] :
    (∑ i ∈ t, φ i).vars ⊆ Finset.biUnion t fun i => (φ i).vars

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars ⊆ s✝.biUnion fun i => (φ i).vars
⊢ (∑ i ∈ insert a✝ s✝, φ i).vars ⊆ (insert a✝ s✝).biUnion fun i => (φ i).vars

Tactic:
rw [Finset.biUnion_insert, Finset.sum_insert has]

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars ⊆ s✝.biUnion fun i => (φ i).vars
⊢ (φ a✝ + ∑ x ∈ s✝, φ x).vars ⊆ (φ a✝).vars ∪ s✝.biUnion fun i => (φ i).vars

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars ⊆ s✝.biUnion fun i => (φ i).vars
⊢ (∑ x ∈ s✝, φ x).vars ⊆ s✝.biUnion fun i => (φ i).vars

Tactic:
assumption

Result:
no goals

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars ⊆ s✝.biUnion fun i => (φ i).vars
⊢ (φ a✝ + ∑ x ∈ s✝, φ x).vars ⊆ (φ a✝).vars ∪ s✝.biUnion fun i => (φ i).vars

Tactic:
refine Finset.Subset.trans
  (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars ⊆ s✝.biUnion fun i => (φ i).vars
⊢ (∑ x ∈ s✝, φ x).vars ⊆ s✝.biUnion fun i => (φ i).vars

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (∑ i ∈ t, φ i).vars ⊆ t.biUnion fun i => (φ i).vars

Tactic:
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has]
  refine Finset.Subset.trans
    (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
  assumption

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (∑ i ∈ t, φ i).vars ⊆ t.biUnion fun i => (φ i).vars

Tactic:
classical
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has]
  refine Finset.Subset.trans
    (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
  assumption

Result:
no goals

Proof state:
case empty
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (∑ i ∈ ∅, φ i).vars ⊆ ∅.biUnion fun i => (φ i).vars

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem sup_eq_left {a b : CauSeq α abs} (h : b ≤ a) : a ⊔ b ≈ a

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≤ a
⊢ a ⊔ b ≈ a

Tactic:
simpa only [CauSeq.sup_comm] using CauSeq.sup_eq_right h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem reverse_attach (xs : Array α) :
    xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩

Proof state:
α : Type u_1
xs : Array α
⊢ xs.attach.reverse =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.reverse.attach

Tactic:
cases xs

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach.reverse =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toList := toList✝ }.reverse.attach

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach.reverse =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toList := toList✝ }.reverse.attach

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.134317
xs : Array α
x✝ : { x // x ∈ xs.reverse }
x : α
h : x ∈ xs.reverse
⊢ x ∈ xs

Tactic:
simpa using h

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_X_pow_self (n : ℕ) : coeff R n ((X : R⟦X⟧) ^ n) = 1

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (coeff R n) (X ^ n) = 1

Tactic:
rw [coeff_X_pow, if_pos rfl]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma basicOpen_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ f ⁻¹ᵁ V)
    (s : Γ(Y, V)) : X.basicOpen (f.appLE V U e s) = U ⊓ f ⁻¹ᵁ (Y.basicOpen s)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : ↑Γ(Y, V)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appLE f V U e)) s) = U ⊓ f ⁻¹ᵁ Y.basicOpen s

Tactic:
simp only [preimage_basicOpen, Hom.appLE, CommRingCat.comp_apply, RingHom.coe_comp,
  Function.comp_apply]

Result:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : ↑Γ(Y, V)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE e).op)) ((ConcreteCategory.hom (Hom.app f V)) s)) =
    U ⊓ X.basicOpen ((ConcreteCategory.hom (Hom.app f V)) s)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : ↑Γ(Y, V)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE e).op)) ((ConcreteCategory.hom (Hom.app f V)) s)) =
    U ⊓ X.basicOpen ((ConcreteCategory.hom (Hom.app f V)) s)

Tactic:
rw [basicOpen_res]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem leadingCoeff_map_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) :
    leadingCoeff (p.map f) = f (leadingCoeff p)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ (map f p).coeff (map f p).natDegree = f (p.coeff p.natDegree)

Tactic:
rw [coeff_map, natDegree_map_of_leadingCoeff_ne_zero f hf]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ (map f p).leadingCoeff = f p.leadingCoeff

Tactic:
unfold leadingCoeff

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ (map f p).coeff (map f p).natDegree = f (p.coeff p.natDegree)
-- Mathlib/Data/Fintype/Quotient.lean
@[simp]
lemma finLiftOn_empty [e : IsEmpty ι] (q : ∀ i, Quotient (S i)) :
    finLiftOn (β := β) q = fun f _ ↦ f e.elim

Proof state:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ finLiftOn q f h = f fun a => e.elim a

Tactic:
dsimp [finLiftOn]

Result:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ (finChoice q).liftOn f h = f fun a => e.elim a

Proof state:
case h.h.a
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
a✝ : (i : ι) → α i
⊢ ⟦a✝⟧.liftOn f h = f fun a => e.elim a

Tactic:
exact h _ _ e.elim

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
⊢ finLiftOn q = fun f x => f fun a => e.elim a

Tactic:
ext f h

Result:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ finLiftOn q f h = f fun a => e.elim a

Proof state:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ (finChoice q).liftOn f h = f fun a => e.elim a

Tactic:
induction finChoice q using Quotient.ind

Result:
case h.h.a
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
a✝ : (i : ι) → α i
⊢ ⟦a✝⟧.liftOn f h = f fun a => e.elim a
-- Mathlib/NumberTheory/JacobiSum/Basic.lean
/-- The Jacobi sum is compatible with ring homomorphisms. -/
lemma jacobiSum_ringHomComp {R'' : Type*} [CommRing R''] (χ ψ : MulChar R R') (f : R' →+* R'') :
    jacobiSum (χ.ringHomComp f) (ψ.ringHomComp f) = f (jacobiSum χ ψ)

Proof state:
R : Type u_1
R' : Type u_2
inst✝³ : CommRing R
inst✝² : Fintype R
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ ψ : MulChar R R'
f : R' →+* R''
⊢ jacobiSum (χ.ringHomComp f) (ψ.ringHomComp f) = f (jacobiSum χ ψ)

Tactic:
simp only [jacobiSum, MulChar.ringHomComp, MulChar.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
  map_sum, map_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem AffineIndependent.finrank_vectorSpan_image_finset [DecidableEq P]
    {p : ι → P} (hi : AffineIndependent k p) {s : Finset ι} {n : ℕ} (hc : #s = n + 1) :
    finrank k (vectorSpan k (s.image p : Set P)) = n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k fun x => ↑x
hc' : #(Finset.image p s) = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ p₁ ∈ p '' ↑s

Tactic:
simpa using hp₁

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' : LinearIndependent k fun (v : ↑↑(Finset.image (fun p => p -ᵥ p₁) ((Finset.image p s).erase p₁))) => ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ #(Finset.image (fun x => x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n

Tactic:
rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' : LinearIndependent k fun (v : ↑↑(Finset.image (fun p => p -ᵥ p₁) ((Finset.image p s).erase p₁))) => ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ #(Finset.image p s) - 1 = n
-- Mathlib/Algebra/Group/Int/Units.lean
lemma units_natAbs (u : ℤˣ) : natAbs u = 1 :=
  Units.ext_iff.1 <|
    Nat.units_eq_one
      ⟨natAbs u, natAbs ↑u⁻¹, by rw [← natAbs_mul, Units.mul_inv]; rfl, by
        rw [← natAbs_mul, Units.inv_mul]; rfl⟩

Proof state:
u : ℤˣ
⊢ natAbs 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
u : ℤˣ
⊢ (↑u⁻¹).natAbs * (↑u).natAbs = 1

Tactic:
rw [← natAbs_mul, Units.inv_mul]

Result:
u : ℤˣ
⊢ natAbs 1 = 1

Proof state:
u : ℤˣ
⊢ (↑u).natAbs * (↑u⁻¹).natAbs = 1

Tactic:
rw [← natAbs_mul, Units.mul_inv]

Result:
u : ℤˣ
⊢ natAbs 1 = 1
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
/-- If two measures coincide locally, then a set is everywhere positive for the former iff it is
everywhere positive for the latter. -/
lemma isEverywherePos_iff_of_forall_exists_nhds_eq (h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u) :
    IsEverywherePos ν s ↔ IsEverywherePos μ s

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
H : ν.IsEverywherePos s
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u

Tactic:
intro x hx

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
H : ν.IsEverywherePos s
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
H : ν.IsEverywherePos s
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u

Tactic:
rcases h x hx with ⟨t, ht, h't⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
H : ν.IsEverywherePos s
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝 x
h't : ∀ u ⊆ t, ν u = μ u
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
H : ν.IsEverywherePos s
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝 x
h't : ∀ u ⊆ t, ν u = μ u
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u

Tactic:
exact ⟨t, ht, fun u hu ↦ (h't u hu).symm⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
⊢ ν.IsEverywherePos s ↔ μ.IsEverywherePos s

Tactic:
refine ⟨fun H ↦ H.of_forall_exists_nhds_eq ?_, fun H ↦ H.of_forall_exists_nhds_eq h⟩

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
H : ν.IsEverywherePos s
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem QuotientAddGroup.norm_lt_iff {S : AddSubgroup M} {x : M ⧸ S} {r : ℝ} :
    ‖x‖ < r ↔ ∃ m : M, ↑m = x ∧ ‖m‖ < r

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ ‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r

Tactic:
rw [isGLB_lt_iff (isGLB_quotient_norm _), exists_mem_image]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ (∃ x_1 ∈ {m | (mk' S) m = x}, ‖x_1‖ < r) ↔ ∃ m, ↑m = x ∧ ‖m‖ < r

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ (∃ x_1 ∈ {m | (mk' S) m = x}, ‖x_1‖ < r) ↔ ∃ m, ↑m = x ∧ ‖m‖ < r

Tactic:
rfl

Result:
no goals