harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Control/Bitraversable/Lemmas.lean
theorem comp_tsnd {α β₀ β₁ β₂} (g : β₀ → F β₁) (g' : β₁ → G β₂) (x : t α β₀) :
    Comp.mk (tsnd g' <$> tsnd g x) = tsnd (Comp.mk ∘ map g' ∘ g) x

Proof state:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ Comp.mk (tsnd g' <$> tsnd g x) = tsnd (Comp.mk ∘ map g' ∘ g) x

Tactic:
rw [← comp_bitraverse]

Result:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (Comp.mk ∘ map pure ∘ pure) (Comp.mk ∘ map g' ∘ g) x = tsnd (Comp.mk ∘ map g' ∘ g) x

Proof state:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (fun x => Comp.mk (pure (pure x))) (fun x => Comp.mk (g' <$> g x)) x =
    tsnd (fun x => Comp.mk (g' <$> g x)) x

Tactic:
rfl

Result:
no goals

Proof state:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (Comp.mk ∘ map pure ∘ pure) (Comp.mk ∘ map g' ∘ g) x = tsnd (Comp.mk ∘ map g' ∘ g) x

Tactic:
simp only [Function.comp_def, map_pure]

Result:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (fun x => Comp.mk (pure (pure x))) (fun x => Comp.mk (g' <$> g x)) x =
    tsnd (fun x => Comp.mk (g' <$> g x)) x
-- Mathlib/Data/Sign.lean
theorem lt_one_iff {a : SignType} : a < 1 ↔ a ≤ 0

Proof state:
a : SignType
⊢ a < 1 ↔ a ≤ 0

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem b_of_eq (h : P.toPoly = Q.toPoly) : P.b = Q.b

Proof state:
R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.b = Q.b

Tactic:
rw [← coeff_eq_b, h, coeff_eq_b]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_lt_one : (p : K) < 1 ↔ p < 1

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
p : ℚ≥0
⊢ ↑p < 1 ↔ p < 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Data/Prod/Basic.lean
theorem LeftInverse.prodMap (hf : LeftInverse f₁ f₂) (hg : LeftInverse g₁ g₂) :
    LeftInverse (map f₁ g₁) (map f₂ g₂) :=
  fun a ↦ by rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ map f₁ g₁ (map f₂ g₂ a) = a

Tactic:
rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getElem?_range {m n : Nat} (h : m < n) : (range n)[m]? = some m

Proof state:
m n : Nat
h : m < n
⊢ (range n)[m]? = some m

Tactic:
simp [range_eq_range', getElem?_range' _ _ h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem comap_eq {f : γ → β} :
    𝒱(α, γ, 𝔖, ‹UniformSpace β›.comap f) = 𝒱(α, β, 𝔖, _).comap (f ∘ ·)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β 𝔖)

Tactic:
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.comap_eq, ←
  UniformSpace.comap_comap]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ ⨅ s ∈ 𝔖,
      UniformSpace.comap ((fun x => f ∘ x) ∘ ⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑s) β) =
    ⨅ i ∈ 𝔖,
      UniformSpace.comap ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(toFun 𝔖)) ∘ fun x => f ∘ x)
        (UniformFun.uniformSpace (↑i) β)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ ⨅ s ∈ 𝔖,
      UniformSpace.comap ((fun x => f ∘ x) ∘ ⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑s) β) =
    ⨅ i ∈ 𝔖,
      UniformSpace.comap ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(toFun 𝔖)) ∘ fun x => f ∘ x)
        (UniformFun.uniformSpace (↑i) β)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeries.term_sub (f g : ℕ → ℂ) (s : ℂ) : term (f - g) s = term f s - term g s

Proof state:
f g : ℕ → ℂ
s : ℂ
⊢ term (f - g) s = term f s - term g s

Tactic:
simp_rw [sub_eq_add_neg, term_add, term_neg]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem prod_symm (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
    (e.prod e').symm = e.symm.prod e'.symm

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
⊢ (e.prod e').symm = e.symm.prod e'.symm

Tactic:
ext x <;> simp [prod_coe_symm]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem trim_congr {m₁ m₂ : OuterMeasure α} (H : ∀ {s : Set α}, MeasurableSet s → m₁ s = m₂ s) :
    m₁.trim = m₂.trim

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ : OuterMeasure α
H : ∀ {s : Set α}, MeasurableSet s → m₁ s = m₂ s
⊢ m₁.trim = m₂.trim

Tactic:
simp +contextual only [trim, H]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_subtypeDomain {f : Π₀ i, β i} :
    (subtypeDomain p f).support = f.support.subtype p

Proof state:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

Tactic:
ext i

Result:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
⊢ i ∈ (subtypeDomain p f).support ↔ i ∈ Finset.subtype p f.support

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
⊢ i ∈ (subtypeDomain p f).support ↔ i ∈ Finset.subtype p f.support

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomologySequence.lean
@[reassoc (attr := simp)]
lemma opcyclesToCycles_homologyπ :
    K.opcyclesToCycles i j ≫ K.homologyπ j = 0

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.opcyclesToCycles i j ≫ K.homologyπ j = 0

Tactic:
simp only [← cancel_epi (K.pOpcycles i),
  pOpcycles_opcyclesToCycles_assoc, toCycles_comp_homologyπ, comp_zero]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem ghostFun_add : ghostFun (x + y) = ghostFun x + ghostFun y

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ WittVector.ghostFun (x + y) = WittVector.ghostFun x + WittVector.ghostFun y

Tactic:
ghost_fun_tac X 0 + X 1, ![x.coeff, y.coeff]

Result:
no goals
-- Mathlib/RingTheory/FreeRing.lean
theorem induction_on {C : FreeRing α → Prop} (z : FreeRing α) (hn1 : C (-1))
    (hb : ∀ b, C (of b)) (ha : ∀ x y, C x → C y → C (x + y)) (hm : ∀ x y, C x → C y → C (x * y)) :
    C z :=
  have hn : ∀ x, C x → C (-x) := fun x ih => neg_one_mul x ▸ hm _ _ hn1 ih
  have h1 : C 1 := neg_neg (1 : FreeRing α) ▸ hn _ hn1
  FreeAbelianGroup.induction_on z (neg_add_cancel (1 : FreeRing α) ▸ ha _ _ hn1 h1)
    (fun m => List.recOn m h1 fun a m ih => by
      -- Porting note: in mathlib, convert was not necessary, `exact hm _ _ (hb a) ih` worked fine
      convert hm _ _ (hb a) ih
      rw [of, ← FreeAbelianGroup.of_mul]
      rfl)
    (fun _ ih => hn _ ih) ha

Proof state:
case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = of a * FreeAbelianGroup.of m

Tactic:
rw [of, ← FreeAbelianGroup.of_mul]

Result:
case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = FreeAbelianGroup.of (FreeMonoid.of a * m)

Proof state:
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ C (FreeAbelianGroup.of (a :: m))

Tactic:
convert hm _ _ (hb a) ih

Result:
case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = of a * FreeAbelianGroup.of m

Proof state:
case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = FreeAbelianGroup.of (FreeMonoid.of a * m)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem ImageMap.factor_map {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g)
    (m : ImageMap sq) : factorThruImage f.hom ≫ m.map = sq.left ≫ factorThruImage g.hom :=
  (cancel_mono (image.ι g.hom)).1 <| by simp

Proof state:
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
m : ImageMap sq
⊢ (factorThruImage f.hom ≫ m.map) ≫ image.ι g.hom = (sq.left ≫ factorThruImage g.hom) ≫ image.ι g.hom

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List α}
    (distinct : l.Pairwise (fun a b => (a == b) = false)) :
    (∀ (a : α), m.contains a → l.contains a = false) →
    (insertManyIfNewUnit m l).1.1.size = m.1.size + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ (∀ (a : α), m.contains a = true → l.contains a = false) →
    (insertManyIfNewUnit m l).val.val.size = m.val.size + l.length

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.length_insertListIfNewUnit

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem length_toList (s : Finset α) : s.toList.length = #s

Proof state:
α : Type u_1
s : Finset α
⊢ s.toList.length = #s

Tactic:
rw [toList, ← Multiset.coe_card, Multiset.coe_toList, card_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_append' {β : Type _} (f : β → α → β) (b) (l l' : Array α)
    (w : stop = l.size + l'.size) :
    (l ++ l').foldl f b 0 stop = l'.foldl f (l.foldl f b)

Proof state:
α : Type u_1
stop : Nat
β : Type u_2
f : β → α → β
b : β
l l' : Array α
w : stop = l.size + l'.size
⊢ foldl f b (l ++ l') 0 stop = foldl f (foldl f b l) l'

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l l' : Array α
⊢ foldl f b (l ++ l') 0 (l.size + l'.size) = foldl f (foldl f b l) l'

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l l' : Array α
⊢ foldl f b (l ++ l') 0 (l.size + l'.size) = foldl f (foldl f b l) l'

Tactic:
simp [foldl_eq_foldlM]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.add_same (a : BitVec w) : a + a = a * 2#w

Proof state:
w : Nat
a : BitVec w
⊢ a + a = a * 2#w

Tactic:
rw [BitVec.mul_two]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverEntropyInfEntourage_univ (T : X → X) {F : Set X} (h : F.Nonempty) :
    coverEntropyInfEntourage T F univ = 0

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ coverEntropyInfEntourage T F univ = 0

Tactic:
simp [coverEntropyInfEntourage, coverMincard_univ T h]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem Quotient.equiv_refl (P : Submodule R M) (Q : Submodule R M)
    (hf : P.map (LinearEquiv.refl R M : M →ₗ[R] M) = Q) :
    Quotient.equiv P Q (LinearEquiv.refl R M) hf = quotEquivOfEq _ _ (by simpa using hf) :=
  rfl

Proof state:
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' P Q : Submodule R M
hf : map (↑(LinearEquiv.refl R M)) P = Q
⊢ P = Q

Tactic:
simpa using hf

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma zpow_natCast_sub_one₀ (ha : a ≠ 0) (n : ℕ) : a ^ (n - 1 : ℤ) = a ^ n / a

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (↑n - 1) = a ^ n / a

Tactic:
simpa using zpow_sub₀ ha n 1

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem isAlgebraic_bot_iff (h : Function.Injective (algebraMap R S)) {x : S} :
    _root_.IsAlgebraic (⊥ : Subalgebra R S) x ↔ _root_.IsAlgebraic R x :=
  isAlgebraic_ringHom_iff_of_comp_eq (Algebra.botEquivOfInjective h).symm (RingHom.id S)
    Function.injective_id (by rfl)

Proof state:
R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Injective ⇑(algebraMap R S)
x : S
⊢ (algebraMap (↥⊥) S).comp ↑(Algebra.botEquivOfInjective h).symm = (↑(RingHom.id S)).comp (algebraMap R S)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_alterKey_eq_sub_one {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)}
    (h : containsKey k l) (h' : (f (getValue? k l)).isNone) :
    (alterKey k f l).length = l.length - 1

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
h : containsKey k l = true
h' : (f (getValue? k l)).isNone = true
⊢ (alterKey k f l).length = l.length - 1

Tactic:
simp [length_alterKey', h, h']

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma card_snocEquiv_filter_piFinset (P : (∀ i, α (castSucc i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (init r)}.card =
      (S (last _)).card * {r ∈ piFinset (init S) | P r}.card

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ #(filter (fun r => P (init r)) (piFinset S)) = #(S (last n)) * #(filter (fun r => P r) (piFinset (init S)))

Tactic:
rw [← card_product, ← map_snocEquiv_filter_piFinset, card_map]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp] lemma krullDim_of_noMinOrder [Nonempty α] [NoMinOrder α] : krullDim α = ⊤

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Nonempty α
inst✝ : NoMinOrder α
⊢ krullDim α = ⊤

Tactic:
simp [krullDim_eq_iSup_height, height_of_noMinOrder]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_dblX (P : Fin 3 → A) : (W'.baseChange B).toProjective.dblX (f ∘ P) =
    f ((W'.baseChange A).toProjective.dblX P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toProjective.dblX (⇑f ∘ P) = f ((baseChange W' A).toProjective.dblX P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblX, map_baseChange]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_add_eq_right_of_degree_lt (h : degree p < degree q) : degree (p + q) = degree q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree < q.degree
⊢ (p + q).degree = q.degree

Tactic:
rw [add_comm, degree_add_eq_left_of_degree_lt h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma slope_of_X_ne {x₁ x₂ y₁ y₂ : F} (hx : x₁ ≠ x₂) :
    W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)

Tactic:
rw [slope, if_neg hx]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_neg_Iic : Neg.neg '' Iic a = Ici (-a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a : α
⊢ Neg.neg '' Iic a = Ici (-a)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_union_eq_right [DecidableEq α] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1) :
    ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
⊢ ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a

Tactic:
rw [union_comm, prod_union_eq_left hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_right_comm (a b c : Int) : a + b + c = a + c + b

Proof state:
a b c : Int
⊢ a + b + c = a + c + b

Tactic:
rw [Int.add_assoc, Int.add_comm b, ← Int.add_assoc]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
lemma nonempty_of_finiteDimensional [r.FiniteDimensional] : Nonempty α

Proof state:
case intro
α : Type u_1
r : Rel α α
inst✝ : r.FiniteDimensional
p : RelSeries r
h✝ : ∀ (y : RelSeries r), y.length ≤ p.length
⊢ Nonempty α

Tactic:
exact ⟨p 0⟩

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
inst✝ : r.FiniteDimensional
⊢ Nonempty α

Tactic:
obtain ⟨p, _⟩ := (Rel.finiteDimensional_iff r).mp ‹_›

Result:
case intro
α : Type u_1
r : Rel α α
inst✝ : r.FiniteDimensional
p : RelSeries r
h✝ : ∀ (y : RelSeries r), y.length ≤ p.length
⊢ Nonempty α
-- Mathlib/Order/UpperLower/Basic.lean
@[simp] lemma sdiff_singleton (s : LowerSet α) (a : α) : s.sdiff {a} = s.erase a

Proof state:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
a : α
⊢ s.sdiff {a} = s.erase a

Tactic:
simp [sdiff, erase]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_add (x y : R) (p q : R[X][Y]) :
    (p + q).evalEval x y = p.evalEval x y + q.evalEval x y

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p + q) = evalEval x y p + evalEval x y q

Tactic:
simp only [evalEval, eval_add]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.re_im_iff :
    Integrable (fun x => RCLike.re (f x)) μ ∧ Integrable (fun x => RCLike.im (f x)) μ ↔
      Integrable f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
⊢ Integrable (fun x => RCLike.re (f x)) μ ∧ Integrable (fun x => RCLike.im (f x)) μ ↔ Integrable f μ

Tactic:
simp_rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
⊢ MemLp (fun x => RCLike.re (f x)) 1 μ ∧ MemLp (fun x => RCLike.im (f x)) 1 μ ↔ MemLp f 1 μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
⊢ MemLp (fun x => RCLike.re (f x)) 1 μ ∧ MemLp (fun x => RCLike.im (f x)) 1 μ ↔ MemLp f 1 μ

Tactic:
exact memLp_re_im_iff

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
lemma inter_singleton {a : α} {s : Finset α} :
    s ∩ {a} = if a ∈ s then {a} else ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ s ∩ {a} = if a ∈ s then {a} else ∅

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_neg_one (x : ℂ) : x ^ (-1 : ℂ) = x⁻¹

Proof state:
x : ℂ
⊢ x ^ (-1) = x⁻¹

Tactic:
simpa using cpow_neg x 1

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem single_mul_single [Fintype n] [DecidableEq k] [DecidableEq m] [DecidableEq n] [Semiring α]
    (a : m) (b : n) (c : k) :
    ((single a b).toMatrix : Matrix _ _ α) * (single b c).toMatrix = (single a c).toMatrix

Proof state:
k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype n
inst✝³ : DecidableEq k
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
a : m
b : n
c : k
⊢ (single a b).toMatrix * (single b c).toMatrix = (single a c).toMatrix

Tactic:
rw [← toMatrix_trans, single_trans_single]

Result:
no goals
-- Mathlib/Analysis/Convex/Extreme.lean
theorem Convex.mem_extremePoints_iff_mem_diff_convexHull_diff (hA : Convex 𝕜 A) :
    x ∈ A.extremePoints 𝕜 ↔ x ∈ A \ convexHull 𝕜 (A \ {x})

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜) (A \ {x})

Tactic:
rw [hA.mem_extremePoints_iff_convex_diff, hA.convex_remove_iff_not_mem_convexHull_remove,
  mem_diff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem cons_merge_cons_pos (s : α → α → Bool) (l r) (h : s a b) :
    merge (a::l) (b::r) s = a :: merge l (b::r) s

Proof state:
α : Type u_1
a b : α
s : α → α → Bool
l r : List α
h : s a b = true
⊢ (a :: l).merge (b :: r) s = a :: l.merge (b :: r) s

Tactic:
rw [cons_merge_cons, if_pos h]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma star_neg_iff {x : R} : star x < 0 ↔ x < 0

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ star x < 0 ↔ x < 0

Tactic:
simpa using star_lt_star_iff (x := x) (y := 0)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
theorem HasDerivAt.clog {f : ℂ → ℂ} {f' x : ℂ} (h₁ : HasDerivAt f f' x)
    (h₂ : f x ∈ slitPlane) : HasDerivAt (fun t => log (f t)) (f' / f x) x

Proof state:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun t => log (f t)) (f' / f x) x

Tactic:
rw [div_eq_inv_mul]

Result:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x

Proof state:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x

Tactic:
exact (hasStrictDerivAt_log h₂).hasDerivAt.comp x h₁

Result:
no goals