harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem hasBasis_uniformity_of_basis_aux₁ {p : ι → Prop} {s : ι → Set (β × β)}
    (hb : HasBasis (𝓤 β) p s) (S : Set α) :
    (@uniformity (α →ᵤ[𝔖] β) ((UniformFun.uniformSpace S β).comap S.restrict)).HasBasis p fun i =>
      UniformOnFun.gen 𝔖 S (s i)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ (comap (Prod.map S.restrict S.restrict) (𝓤 (↑S → β))).HasBasis p fun i =>
    Prod.map (S.restrict ∘ ⇑UniformFun.toFun) (S.restrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β (s i)

Tactic:
exact (UniformFun.hasBasis_uniformity_of_basis S β hb).comap _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis p fun i => UniformOnFun.gen 𝔖 S (s i)

Tactic:
simp_rw [UniformOnFun.gen_eq_preimage_restrict, uniformity_comap]

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ (comap (Prod.map S.restrict S.restrict) (𝓤 (↑S → β))).HasBasis p fun i =>
    Prod.map (S.restrict ∘ ⇑UniformFun.toFun) (S.restrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β (s i)
-- Mathlib/Data/Finsupp/Interval.lean
theorem card_uIcc :
    #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i) (g i))

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))

Tactic:
exact card_Icc (_ : ι →₀ α) _

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i) (g i))

Tactic:
rw [← support_inf_union_support_sup]

Result:
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_top_right : relrank A ⊤ = Module.rank A E

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ A.relrank ⊤ = Module.rank (↥A) E

Tactic:
rw [← relrank_mul_rank_top (show A ≤ ⊤ from le_top), IntermediateField.rank_top, mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Ioo {a b : ℝ} : volume (Ioo a b) = ofReal (b - a)

Proof state:
a b : ℝ
⊢ volume (Ioo a b) = ofReal (b - a)

Tactic:
simp [volume_val]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem le_spanSingleton_mul_iff {x : P} {I J : FractionalIdeal S P} :
    I ≤ spanSingleton S x * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI :=
  show (∀ {zI} (_ : zI ∈ I), zI ∈ spanSingleton _ x * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI by
    simp only [mem_singleton_mul, eq_comm]

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
⊢ (∀ {zI : P}, zI ∈ I → zI ∈ spanSingleton S x * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

Tactic:
simp only [mem_singleton_mul, eq_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_comm (x y : P) : midpoint R x y = midpoint R y x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ midpoint R x y = midpoint R y x

Tactic:
rw [midpoint, ← lineMap_apply_one_sub, one_sub_invOf_two, midpoint]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem sum_subgroup_units [Ring K] [NoZeroDivisors K]
    {G : Subgroup Kˣ} [Fintype G] [Decidable (G = ⊥)] :
    ∑ x : G, (x.val : K) = if G = ⊥ then 1 else 0

Proof state:
case neg
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
G_bot : ¬G = ⊥
⊢ ∑ x : ↥G, ↑↑x = if G = ⊥ then 1 else 0

Tactic:
simp only [G_bot, ite_false]

Result:
case neg
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
G_bot : ¬G = ⊥
⊢ ∑ x : ↥G, ↑↑x = 0

Proof state:
case neg
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
G_bot : ¬G = ⊥
⊢ ∑ x : ↥G, ↑↑x = 0

Tactic:
exact sum_subgroup_units_eq_zero G_bot

Result:
no goals

Proof state:
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
⊢ ∑ x : ↥G, ↑↑x = if G = ⊥ then 1 else 0

Tactic:
by_cases G_bot : G = ⊥

Result:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
G_bot : G = ⊥
⊢ ∑ x : ↥G, ↑↑x = if G = ⊥ then 1 else 0

case neg
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
G_bot : ¬G = ⊥
⊢ ∑ x : ↥G, ↑↑x = if G = ⊥ then 1 else 0

Proof state:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Fintype ↥⊥
inst✝ : Decidable (⊥ = ⊥)
⊢ ⟨1, ⋯⟩ = 1

Tactic:
rfl

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
G_bot : G = ⊥
⊢ ∑ x : ↥G, ↑↑x = if G = ⊥ then 1 else 0

Tactic:
subst G_bot

Result:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Fintype ↥⊥
inst✝ : Decidable (⊥ = ⊥)
⊢ ∑ x : ↥⊥, ↑↑x = if ⊥ = ⊥ then 1 else 0

Proof state:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Fintype ↥⊥
inst✝ : Decidable (⊥ = ⊥)
⊢ default = 1

Tactic:
rw [Set.default_coe_singleton]

Result:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Fintype ↥⊥
inst✝ : Decidable (⊥ = ⊥)
⊢ ⟨1, ⋯⟩ = 1

Proof state:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Fintype ↥⊥
inst✝ : Decidable (⊥ = ⊥)
⊢ ∑ x : ↥⊥, ↑↑x = if ⊥ = ⊥ then 1 else 0

Tactic:
simp only [univ_unique, sum_singleton, ↓reduceIte, Units.val_eq_one, OneMemClass.coe_eq_one]

Result:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Fintype ↥⊥
inst✝ : Decidable (⊥ = ⊥)
⊢ default = 1
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma pow_le_one_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a : M₀
n : ℕ
ha : 0 ≤ a
hn : n ≠ 0
⊢ a ^ n ≤ 1 ↔ a ≤ 1

Tactic:
simpa only [one_pow] using pow_le_pow_iff_left₀ ha zero_le_one hn

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem BitVec.eq_to_beq (a b : BitVec w) : (a = b) = ((a == b) = true)

Proof state:
w : Nat
a b : BitVec w
⊢ (a = b) = ((a == b) = true)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem sum_equiv_comp_eval_eq_elim : eval C ∘ (sum_equiv C hsC ho).toFun =
    (Sum.elim (fun (l : GoodProducts (π C (ord I · < o))) ↦ Products.eval C l.1)
    (fun (l : MaxProducts C ho) ↦ Products.eval C l.1))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ eval C ∘ (sum_equiv C hsC ho).toFun = Sum.elim (fun l => Products.eval C ↑l) fun l => Products.eval C ↑l

Tactic:
ext ⟨_,_⟩ <;> [rfl; rfl]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem one_lt_encard_iff_nontrivial : 1 < s.encard ↔ s.Nontrivial

Proof state:
α : Type u_1
s : Set α
⊢ 1 < s.encard ↔ s.Nontrivial

Tactic:
rw [← not_iff_not, not_lt, Set.not_nontrivial_iff, ← encard_le_one_iff_subsingleton]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem end_mem_tail_support {u v : V} {p : G.Walk u v} (h : ¬ p.Nil) : v ∈ p.support.tail :=
  p.notNilRec (by simp) h

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ¬p.Nil
⊢ ∀ {u v w : V} (h : G.Adj u v) (q : G.Walk v w), w ∈ (cons h q).support.tail

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists_eq_sublists' (l : List α) : sublists l = map reverse (sublists' (reverse l))

Proof state:
α : Type u
l : List α
⊢ l.sublists = map reverse l.reverse.sublists'

Tactic:
rw [← sublists_reverse, reverse_reverse]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem tail_enum (l : List α) : (enum l).tail = enumFrom 1 l.tail

Proof state:
α : Type u_1
l : List α
⊢ l.enum.tail = enumFrom 1 l.tail

Tactic:
simp [enum]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) :
    sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
  if_neg <| by simp [hs, h's]

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set (WithTop α)
hs : ¬s ⊆ {⊤}
h's : BddBelow s
⊢ ¬(s ⊆ {⊤} ∨ ¬BddBelow s)

Tactic:
simp [hs, h's]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_eq_zero {a b : Int} : a * b = 0 ↔ a = 0 ∨ b = 0

Proof state:
a b : Int
h : a * b = 0
x✝¹ : Int
x✝ : x✝¹ * ofNat 0 = 0
⊢ x✝¹ = 0 ∨ ofNat 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
a b : Int
h : a * b = 0
x✝¹ : Int
x✝ : ofNat 0 * x✝¹ = 0
⊢ ofNat 0 = 0 ∨ x✝¹ = 0

Tactic:
simp

Result:
no goals

Proof state:
a b : Int
h : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
exact match a, b, h with
| .ofNat 0, _, _ => by simp
| _, .ofNat 0, _ => by simp
| .ofNat (a+1), .negSucc b, h => by cases h

Result:
no goals

Proof state:
a✝ b✝ : Int
h✝ : a✝ * b✝ = 0
a b : Nat
h : ofNat (a + 1) * -[b+1] = 0
⊢ ofNat (a + 1) = 0 ∨ -[b+1] = 0

Tactic:
cases h

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem eq_of_perm_primeFactorsList {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0)
    (h : a.primeFactorsList ~ b.primeFactorsList) : a = b

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : a.primeFactorsList ~ b.primeFactorsList
⊢ a = b

Tactic:
simpa [prod_primeFactorsList ha, prod_primeFactorsList hb] using List.Perm.prod_eq h

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem conj_mul (z : K) : conj z * z = ‖z‖ ^ 2

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (starRingEnd K) z * z = ↑‖z‖ ^ 2

Tactic:
rw [mul_comm, mul_conj]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_zero : ‖(0 : E →SL[σ₁₂] F)‖ = 0 :=
  le_antisymm (opNorm_le_bound _ le_rfl fun _ ↦ by simp) (opNorm_nonneg _)

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
x✝ : E
⊢ ‖0 x✝‖ ≤ 0 * ‖x✝‖

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem UniformGroup.toUniformSpace_eq {G : Type*} [u : UniformSpace G] [Group G]
    [UniformGroup G] : IsTopologicalGroup.toUniformSpace G = u

Proof state:
case h
G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : UniformGroup G
⊢ 𝓤 G = 𝓤 G

Tactic:
rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_nhds_one G]

Result:
no goals

Proof state:
G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : UniformGroup G
⊢ IsTopologicalGroup.toUniformSpace G = u

Tactic:
ext : 1

Result:
case h
G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : UniformGroup G
⊢ 𝓤 G = 𝓤 G
-- Mathlib/Data/Num/Lemmas.lean
theorem ppred_to_nat : ∀ n : Num, (↑) <$> ppred n = Nat.ppred n
  | 0 => rfl
  | pos p => by
    rw [ppred, Option.map_some, Nat.ppred_eq_some.2]
    rw [PosNum.pred'_to_nat, Nat.succ_pred_eq_of_pos (PosNum.to_nat_pos _)]
    rfl

Proof state:
p : PosNum
⊢ castNum <$> (pos p).ppred = (↑(pos p)).ppred

Tactic:
rw [ppred, Option.map_some, Nat.ppred_eq_some.2]

Result:
p : PosNum
⊢ (↑p.pred').succ = ↑(pos p)

Proof state:
p : PosNum
⊢ ↑p = ↑(pos p)

Tactic:
rfl

Result:
no goals

Proof state:
p : PosNum
⊢ (↑p.pred').succ = ↑(pos p)

Tactic:
rw [PosNum.pred'_to_nat, Nat.succ_pred_eq_of_pos (PosNum.to_nat_pos _)]

Result:
p : PosNum
⊢ ↑p = ↑(pos p)
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_le_idealRange : I.map f ≤ f.idealRange

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ f.idealRange

Tactic:
rw [f.idealRange_eq_map]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ LieIdeal.map f ⊤

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ LieIdeal.map f ⊤

Tactic:
exact LieIdeal.map_mono le_top

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem eq_iff_eq {m n : ℕ} (hm : Odd m) (hn : Odd n) (x y : ℤ) :
    qrSign m n * x = y ↔ x = qrSign m n * y

Proof state:
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
⊢ qrSign m n * x = y ↔ x = qrSign m n * y

Tactic:
refine
    ⟨fun h' =>
      let h := h'.symm
      ?_,
      fun h => ?_⟩ <;>
  rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]

Result:
no goals
-- Mathlib/Data/Nat/BinaryRec.lean
theorem binaryRec_one (z : motive 0) (f : ∀ b n, motive n → motive (bit b n)) :
    binaryRec (motive := motive) z f 1 = f true 0 z

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
⊢ (if n0 : 1 = 0 then ⋯ ▸ z
    else
      let x := f (1 &&& 1 != 0) (1 >>> 1) (binaryRec z f (1 >>> 1));
      ⋯ ▸ x) =
    f true 0 z

Tactic:
simp only [add_one_ne_zero, ↓reduceDIte, Nat.reduceShiftRight, binaryRec_zero]

Result:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
⊢ f (1 &&& 1 != 0) 0 z = f true 0 z

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
⊢ binaryRec z f 1 = f true 0 z

Tactic:
rw [binaryRec]

Result:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
⊢ (if n0 : 1 = 0 then ⋯ ▸ z
    else
      let x := f (1 &&& 1 != 0) (1 >>> 1) (binaryRec z f (1 >>> 1));
      ⋯ ▸ x) =
    f true 0 z

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
⊢ f (1 &&& 1 != 0) 0 z = f true 0 z

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean
lemma freeHomEquiv_symm_comp {M N : SheafOfModules.{u} R} {I : Type u} (s : I → M.sections)
    (p : M ⟶ N) :
    M.freeHomEquiv.symm s ≫ p = N.freeHomEquiv.symm (fun i ↦ sectionsMap p (s i)) :=
  N.freeHomEquiv.injective (by ext; simp [freeHomEquiv_comp_apply])

Proof state:
C : Type u'
inst✝³ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝² : HasWeakSheafify J AddCommGrp
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : J.HasSheafCompose (forget₂ RingCat AddCommGrp)
M N : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
⊢ N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) = N.freeHomEquiv (N.freeHomEquiv.symm fun i => sectionsMap p (s i))

Tactic:
ext

Result:
case h.h
C : Type u'
inst✝³ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝² : HasWeakSheafify J AddCommGrp
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : J.HasSheafCompose (forget₂ RingCat AddCommGrp)
M N : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
x✝ : I
X✝ : Cᵒᵖ
⊢ ↑(N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) x✝) X✝ =
    ↑(N.freeHomEquiv (N.freeHomEquiv.symm fun i => sectionsMap p (s i)) x✝) X✝

Proof state:
case h.h
C : Type u'
inst✝³ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝² : HasWeakSheafify J AddCommGrp
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : J.HasSheafCompose (forget₂ RingCat AddCommGrp)
M N : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
x✝ : I
X✝ : Cᵒᵖ
⊢ ↑(N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) x✝) X✝ =
    ↑(N.freeHomEquiv (N.freeHomEquiv.symm fun i => sectionsMap p (s i)) x✝) X✝

Tactic:
simp [freeHomEquiv_comp_apply]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_self_le_one : a / a ≤ 1 := div_le_of_le_mul <| by rw [one_mul]

Proof state:
a : ℝ≥0∞
⊢ a ≤ 1 * a

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem zpowersEquivZPowers_apply (h : orderOf x = orderOf y) (n : ℕ) :
    zpowersEquivZPowers h ⟨x ^ n, n, zpow_natCast x n⟩ = ⟨y ^ n, n, zpow_natCast y n⟩

Proof state:
G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩

Tactic:
rw [zpowersEquivZPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivZPowers_symm_apply, ←
  Equiv.eq_symm_apply, finEquivZPowers_symm_apply]

Result:
G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (finCongr h) ⟨n % orderOf x, ⋯⟩ = ⟨n % orderOf y, ⋯⟩

Proof state:
G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (finCongr h) ⟨n % orderOf x, ⋯⟩ = ⟨n % orderOf y, ⋯⟩

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem init_pow (m : ℕ) (x : 𝕎 R) (n : ℕ) : init n (x ^ m) = init n (init n x ^ m)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
n : ℕ
⊢ init n (x ^ m) = init n (init n x ^ m)

Tactic:
init_ring using fun p [Fact (Nat.Prime p)] n => wittPow_vars p m n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem getElem?_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (h : n + 1 ≤ k) :
    (insertIdx n x l)[k]? = l[k - 1]?

Proof state:
α : Type u
l : List α
x : α
n k : Nat
h : n + 1 ≤ k
⊢ (insertIdx n x l)[k]? = l[k - 1]?

Tactic:
rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n k : Nat
h : n + 1 ≤ k
⊢ ¬k < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n k : Nat
h : n + 1 ≤ k
⊢ ¬k = n

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem trailingDegree_eq_top : trailingDegree p = ⊤ ↔ p = 0 :=
  ⟨fun h => support_eq_empty.1 (Finset.min_eq_top.1 h), fun h => by simp [h]⟩

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ p.trailingDegree = ⊤

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem cancel_counit_right {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) :
    f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X Y : D
f f' : X ⟶ e.functor.obj (e.inverse.obj Y)
⊢ f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem exists_lt_of_lt_csSup (hs : s.Nonempty) (hb : b < sSup s) : ∃ a ∈ s, b < a

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : b < sSup s
⊢ ∃ a ∈ s, b < a

Tactic:
contrapose! hb

Result:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : ∀ a ∈ s, a ≤ b
⊢ sSup s ≤ b

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : ∀ a ∈ s, a ≤ b
⊢ sSup s ≤ b

Tactic:
exact csSup_le hs hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem zero_and (x : Nat) : 0 &&& x = 0

Proof state:
x : Nat
⊢ 0 &&& x = 0

Tactic:
simp only [HAnd.hAnd, AndOp.and, land]

Result:
x : Nat
⊢ bitwise and 0 x = 0

Proof state:
x : Nat
⊢ bitwise and 0 x = 0

Tactic:
unfold bitwise

Result:
x : Nat
⊢ (if 0 = 0 then if (false && true) = true then x else 0
    else
      if x = 0 then if (true && false) = true then 0 else 0
      else
        let n' := 0 / 2;
        let m' := x / 2;
        let b₁ := 0 % 2 = 1;
        let b₂ := x % 2 = 1;
        let r := bitwise and n' m';
        if (decide b₁ && decide b₂) = true then r + r + 1 else r + r) =
    0

Proof state:
x : Nat
⊢ (if 0 = 0 then if (false && true) = true then x else 0
    else
      if x = 0 then if (true && false) = true then 0 else 0
      else
        let n' := 0 / 2;
        let m' := x / 2;
        let b₁ := 0 % 2 = 1;
        let b₂ := x % 2 = 1;
        let r := bitwise and n' m';
        if (decide b₁ && decide b₂) = true then r + r + 1 else r + r) =
    0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem mem_of_eq_bot {f : Filter α} {s : Set α} (h : f ⊓ 𝓟 sᶜ = ⊥) : s ∈ f

Proof state:
α : Type u
f : Filter α
s : Set α
h : f ⊓ 𝓟 sᶜ = ⊥
⊢ s ∈ f

Tactic:
rwa [inf_principal_eq_bot, compl_compl] at h

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem ranges_nodup {l s : List ℕ} (hs : s ∈ ranges l) : s.Nodup :=
  (List.pairwise_flatten.mp <| by rw [ranges_flatten]; exact nodup_range _).1 s hs

Proof state:
l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 => x1 ≠ x2) l.ranges.flatten

Tactic:
rw [ranges_flatten]

Result:
l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 => x1 ≠ x2) (range l.sum)

Proof state:
l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 => x1 ≠ x2) (range l.sum)

Tactic:
exact nodup_range _

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Basic.lean
@[simp]
lemma sub_le_iff {n : ℕ} {a b : Fin n} : a - b ≤ a ↔ b ≤ a

Proof state:
n : ℕ
a b : Fin n
⊢ a - b ≤ a ↔ b ≤ a

Tactic:
rw [← not_iff_not, Fin.not_le, Fin.not_le, lt_sub_iff]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem mk_mem_sym2_iff : s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s

Proof state:
α : Type u_1
s : Finset α
a b : α
⊢ s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s

Tactic:
rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithBot.le_ofDual_iff {x : WithTop α} {y : WithBot αᵒᵈ} :
    x ≤ WithBot.ofDual y ↔ y ≤ x.toDual

Proof state:
α : Type u_1
inst✝ : LE α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual x

Tactic:
cases x <;> cases y <;> simp [le_toDual]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem isCompactElement_top : CompleteLattice.IsCompactElement (⊤ : Ideal α)

Proof state:
α : Type u
inst✝ : Semiring α
⊢ CompleteLattice.IsCompactElement ⊤

Tactic:
simpa only [← span_singleton_one] using Submodule.singleton_span_isCompactElement 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem getElem?_mapFinIdx (a : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) (i : Nat) :
    (a.mapFinIdx f)[i]? =
      a[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1

Proof state:
α : Type u_1
n : Nat
β : Type u_2
a : Vector α n
f : (i : Nat) → α → i < n → β
i : Nat
⊢ (a.mapFinIdx f)[i]? = a[i]?.pbind fun b h => some (f i b ⋯)

Tactic:
simp only [getElem?_def, getElem_mapFinIdx]

Result:
α : Type u_1
n : Nat
β : Type u_2
a : Vector α n
f : (i : Nat) → α → i < n → β
i : Nat
⊢ (if h : i < n then some (f i a[i] ⋯) else none) =
    (if h : i < n then some a[i] else none).pbind fun a_1 h => some (f i a_1 ⋯)

Proof state:
α : Type u_1
n : Nat
β : Type u_2
a : Vector α n
f : (i : Nat) → α → i < n → β
i : Nat
⊢ (if h : i < n then some (f i a[i] ⋯) else none) =
    (if h : i < n then some a[i] else none).pbind fun a_1 h => some (f i a_1 ⋯)

Tactic:
split <;> simp_all

Result:
no goals