harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean
theorem limsup_preimage_iterate_ae_eq {f : α → α} (hf : QuasiMeasurePreserving f μ μ)
    (hs : f ⁻¹' s =ᵐ[μ] s) : limsup (α := Set α) (fun n => (preimage f)^[n] s) atTop =ᵐ[μ] s :=
  limsup_ae_eq_of_forall_ae_eq (fun n => (preimage f)^[n] s) fun n ↦ by
    simpa only [Set.preimage_iterate_eq] using hf.preimage_iterate_ae_eq n hs

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
n : ℕ
⊢ (fun n => (preimage f)^[n] s) n =ᵐ[μ] s

Tactic:
simpa only [Set.preimage_iterate_eq] using hf.preimage_iterate_ae_eq n hs

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem List.untrop_prod [AddMonoid R] (l : List (Tropical R)) :
    untrop l.prod = List.sum (l.map untrop)

Proof state:
case nil
R : Type u_1
inst✝ : AddMonoid R
⊢ untrop [].prod = (map untrop []).sum

Tactic:
simp

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝ : AddMonoid R
hd : Tropical R
tl : List (Tropical R)
IH : untrop tl.prod = (map untrop tl).sum
⊢ untrop (hd :: tl).prod = (map untrop (hd :: tl)).sum

Tactic:
simp [← IH]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddMonoid R
l : List (Tropical R)
⊢ untrop l.prod = (map untrop l).sum

Tactic:
induction' l with hd tl IH

Result:
case nil
R : Type u_1
inst✝ : AddMonoid R
⊢ untrop [].prod = (map untrop []).sum

case cons
R : Type u_1
inst✝ : AddMonoid R
hd : Tropical R
tl : List (Tropical R)
IH : untrop tl.prod = (map untrop tl).sum
⊢ untrop (hd :: tl).prod = (map untrop (hd :: tl)).sum
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem inv_whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) [IsIso f] :
    inv (f ▷ Z) = inv f ▷ Z

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
f : X ⟶ Y
Z : C
inst✝ : IsIso f
⊢ inv (f ▷ Z) = inv f ▷ Z

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinitesimal_neg_iff_infiniteNeg_inv {x : ℝ*} :
    InfiniteNeg x⁻¹ ↔ Infinitesimal x ∧ x < 0 :=
  infiniteNeg_iff_infinitesimal_inv_neg.trans <| by rw [inv_inv]

Proof state:
x : ℝ*
⊢ x⁻¹⁻¹.Infinitesimal ∧ x⁻¹⁻¹ < 0 ↔ x.Infinitesimal ∧ x < 0

Tactic:
rw [inv_inv]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem map_dvd_map' [Field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map f ↔ x ∣ y

Proof state:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
classical
rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
  coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
  leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
  map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]

Result:
no goals

Proof state:
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
by_cases H : x = 0

Result:
case pos
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

Proof state:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
  coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
  leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
  map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]

Result:
no goals

Proof state:
case pos
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem mem_sSup_of_directedOn {S : Set (L.Substructure M)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) {x : M} :
    x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
S : Set (L.Substructure M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : M
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
S : Set (L.Substructure M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
haveI : Nonempty S := Sne.to_subtype

Result:
L : Language
M : Type w
inst✝ : L.Structure M
S : Set (L.Substructure M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : M
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_eq_right : a ∆ b = b ↔ a = ⊥

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b = b ↔ a = ⊥

Tactic:
rw [symmDiff_comm, symmDiff_eq_left]

Result:
no goals
-- Mathlib/Dynamics/FixedPoints/Basic.lean
theorem preimage_iterate {s : Set α} (h : IsFixedPt (Set.preimage f) s) (n : ℕ) :
    IsFixedPt (Set.preimage f^[n]) s

Proof state:
α : Type u
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f)^[n] s

Tactic:
exact h.iterate n

Result:
no goals

Proof state:
α : Type u
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f^[n]) s

Tactic:
rw [Set.preimage_iterate_eq]

Result:
α : Type u
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f)^[n] s
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem map_unique {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x z : ZFSet.{u}}
    (zx : z ∈ x) : ∃! w, pair z w ∈ map f x :=
  ⟨f z, image.mk _ _ zx, fun y yx => by
    let ⟨w, _, we⟩ := mem_image.1 yx
    let ⟨wz, fy⟩ := pair_injective we
    rw [← fy, wz]⟩

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w => z.pair w ∈ map f x) y
⊢ y = f z

Tactic:
let ⟨w, _, we⟩ := mem_image.1 yx

Result:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w => z.pair w ∈ map f x) y
w : ZFSet.{u}
left✝ : w ∈ x
we : w.pair (f w) = z.pair y
⊢ y = f z

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w => z.pair w ∈ map f x) y
w : ZFSet.{u}
left✝ : w ∈ x
we : w.pair (f w) = z.pair y
⊢ y = f z

Tactic:
let ⟨wz, fy⟩ := pair_injective we

Result:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w => z.pair w ∈ map f x) y
w : ZFSet.{u}
left✝ : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
fy : f w = y
⊢ y = f z

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w => z.pair w ∈ map f x) y
w : ZFSet.{u}
left✝ : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
fy : f w = y
⊢ y = f z

Tactic:
rw [← fy, wz]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem toWithTop_zero' {h : Decidable (0 : PartENat).Dom} : toWithTop 0 = 0

Proof state:
h : Decidable (Dom 0)
⊢ toWithTop 0 = 0

Tactic:
convert toWithTop_zero

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma coe_inv_variableChange_Δ' : (↑(W.variableChange C).Δ'⁻¹ : R) = C.u ^ 12 * W.Δ'⁻¹

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ ↑(W.variableChange C).Δ'⁻¹ = ↑C.u ^ 12 * ↑W.Δ'⁻¹

Tactic:
rw [inv_variableChange_Δ', Units.val_mul, Units.val_pow_eq_pow_val]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Gcd.lean
theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0

Proof state:
m n : Int
hm : m ≠ 0
hn : n ≠ 0
⊢ m.lcm n ≠ 0

Tactic:
simp only [lcm]

Result:
m n : Int
hm : m ≠ 0
hn : n ≠ 0
⊢ m.natAbs.lcm n.natAbs ≠ 0

Proof state:
m n : Int
hm : m ≠ 0
hn : n ≠ 0
⊢ m.natAbs.lcm n.natAbs ≠ 0

Tactic:
apply Nat.lcm_ne_zero <;> simpa

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma even_add' : Even (m + n) ↔ (Odd m ↔ Odd n)

Proof state:
m n : ℕ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)

Tactic:
rw [even_add, ← not_odd_iff_even, ← not_odd_iff_even, not_iff_not]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
@[simp] lemma Iic_False : Iic False = {False}

Proof state:
⊢ Iic False = {False}

Tactic:
aesop

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma of_comp_iff (hg : IsEmbedding g) : IsEmbedding (g ∘ f) ↔ IsEmbedding f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsEmbedding g
⊢ IsEmbedding (g ∘ f) ↔ IsEmbedding f

Tactic:
simp_rw [isEmbedding_iff, hg.isInducing.of_comp_iff, hg.injective.of_comp_iff f]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_int_gt (x : α) : ∃ n : ℤ, x < n :=
  let ⟨n, h⟩ := exists_nat_gt x
  ⟨n, by rwa [Int.cast_natCast]⟩

Proof state:
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℕ
h : x < ↑n
⊢ x < ↑↑n

Tactic:
rwa [Int.cast_natCast]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
lemma «exists» {p : ℂ → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩

Proof state:
p : ℂ → Prop
⊢ (∃ x, p x) ↔ ∃ a b, p { re := a, im := b }

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Multiset/Sort.lean
theorem map_sort (f : α → β) (s : Multiset α)
    (hs : ∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) :
    (s.sort r).map f = (s.map f).sort r'

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : IsAntisymm α r
inst✝⁴ : IsTotal α r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : IsAntisymm β r'
inst✝ : IsTotal β r'
f : α → β
s : Multiset α
hs : ∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)
⊢ List.map f (sort r s) = sort r' (map f s)

Tactic:
revert s

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : IsAntisymm α r
inst✝⁴ : IsTotal α r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : IsAntisymm β r'
inst✝ : IsTotal β r'
f : α → β
⊢ ∀ (s : Multiset α), (∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) → List.map f (sort r s) = sort r' (map f s)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : IsAntisymm α r
inst✝⁴ : IsTotal α r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : IsAntisymm β r'
inst✝ : IsTotal β r'
f : α → β
⊢ ∀ (s : Multiset α), (∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) → List.map f (sort r s) = sort r' (map f s)

Tactic:
exact Quot.ind fun l h => map_mergeSort (l := l) (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : IsAntisymm α r
inst✝⁴ : IsTotal α r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : IsAntisymm β r'
inst✝ : IsTotal β r'
f : α → β
l : List α
h : ∀ a ∈ Quot.mk (⇑(isSetoid α)) l, ∀ b ∈ Quot.mk (⇑(isSetoid α)) l, r a b ↔ r' (f a) (f b)
⊢ ∀ a ∈ l, ∀ b ∈ l, decide (r a b) = decide (r' (f a) (f b))

Tactic:
simpa using h

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem v_p_lt_val {x : O} :
    v p < v (algebraMap O K x) ↔ (Ideal.Quotient.mk _ x : ModP O p) ≠ 0

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
⊢ v ↑p < v ((algebraMap O K) x) ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0

Tactic:
rw [lt_iff_not_le, not_iff_not, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd,
  Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma _root_.CategoryTheory.ShortComplex.isComplex_toComposableArrows (S : ShortComplex C) :
    S.toComposableArrows.IsComplex :=
  isComplex₂_mk _ (by simp)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
⊢ S.toComposableArrows.map' 0 1 ⋯ ⋯ ≫ S.toComposableArrows.map' 1 2 ⋯ ⋯ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem mod_add_div' (m k : ℕ+) : (mod m k + div m k * k : ℕ) = m

Proof state:
m k : ℕ+
⊢ ↑(m.mod k) + m.div k * ↑k = ↑m

Tactic:
rw [mul_comm]

Result:
m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Proof state:
m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
exact mod_add_div _ _

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma image_le_image_of_le {U V : X.Opens} (e : U ≤ V) : f ''ᵁ U ≤ f ''ᵁ V

Proof state:
case intro.intro
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U V : X.Opens
e : U ≤ V
u : ↑↑X.toPresheafedSpace
hu : u ∈ ↑U
⊢ (ConcreteCategory.hom f.toLRSHom.base) u ∈ ↑(f ''ᵁ V)

Tactic:
exact Set.mem_image_of_mem (⇑f.base) (e hu)

Result:
no goals

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U V : X.Opens
e : U ≤ V
⊢ f ''ᵁ U ≤ f ''ᵁ V

Tactic:
rintro a ⟨u, hu, rfl⟩

Result:
case intro.intro
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U V : X.Opens
e : U ≤ V
u : ↑↑X.toPresheafedSpace
hu : u ∈ ↑U
⊢ (ConcreteCategory.hom f.toLRSHom.base) u ∈ ↑(f ''ᵁ V)
-- Mathlib/Order/Category/LinOrd.lean
lemma comp_apply {X Y Z : LinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : LinOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {fallback v : β} :
   getD (m.insert k v) k fallback = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
fallback v : β
⊢ getD (m.insert k v) k fallback = v

Tactic:
simp_to_raw using Raw₀.Const.getD_insert_self

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_rat_lt (x : α) : ∃ q : ℚ, (q : α) < x :=
  let ⟨n, h⟩ := exists_int_lt x
  ⟨n, by rwa [Rat.cast_intCast]⟩

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x : α
n : ℤ
h : ↑n < x
⊢ ↑↑n < x

Tactic:
rwa [Rat.cast_intCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Vector β₁ n) (init : α) :
    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init

Proof state:
case mk
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝ : Monad m
f : β₁ → β₂
g : α → β₂ → m α
init : α
l : Array β₁
⊢ foldlM g init (map f { toArray := l, size_toArray := ⋯ }) =
    foldlM (fun x y => g x (f y)) init { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldlM_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
n : Nat
inst✝ : Monad m
f : β₁ → β₂
g : α → β₂ → m α
l : Vector β₁ n
init : α
⊢ foldlM g init (map f l) = foldlM (fun x y => g x (f y)) init l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝ : Monad m
f : β₁ → β₂
g : α → β₂ → m α
init : α
l : Array β₁
⊢ foldlM g init (map f { toArray := l, size_toArray := ⋯ }) =
    foldlM (fun x y => g x (f y)) init { toArray := l, size_toArray := ⋯ }
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ici_add_one_eq_Ioi (a : α) : Ici (a + 1) = Ioi a

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa [succ_eq_add_one] using Ici_succ_eq_Ioi a

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

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
⊢ W.slope x₁ x₂ y₁ y₂ = 0

Tactic:
rw [slope, if_pos hx, if_pos hy]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_on_bool (hr : Symmetric r) {a b : α} :
    Pairwise (r on fun c => cond c a b) ↔ r a b

Proof state:
α : Type u_1
r : α → α → Prop
hr : Symmetric r
a b : α
⊢ Pairwise (r on fun c => bif c then a else b) ↔ r a b

Tactic:
simpa [Pairwise, Function.onFun] using @hr a b

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma mabs_lt : |a|ₘ < b ↔ b⁻¹ < a ∧ a < b :=
  max_lt_iff.trans <| and_comm.trans <| by rw [inv_lt']

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a⁻¹ < b ∧ a < b ↔ b⁻¹ < a ∧ a < b

Tactic:
rw [inv_lt']

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem neg_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃)
    (f : M →SL[σ₁₂] M₂) : (-g).comp f = -g.comp f

Proof state:
R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ (-g).comp f = -g.comp f

Tactic:
ext

Result:
case h
R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x✝ : M
⊢ ((-g).comp f) x✝ = (-g.comp f) x✝

Proof state:
case h
R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x✝ : M
⊢ ((-g).comp f) x✝ = (-g.comp f) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem support_map_subset [Semiring R] [Semiring S] (f : R →+* S) (p : R[X]) :
    (map f p).support ⊆ p.support

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∉ p.support → x ∉ (map f p).support

Tactic:
simp +contextual

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∈ (map f p).support → x ∈ p.support

Tactic:
contrapose!

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∉ p.support → x ∉ (map f p).support

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).support ⊆ p.support

Tactic:
intro x

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∈ (map f p).support → x ∈ p.support
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem indicatorConstLp_sub {c' : E} :
    indicatorConstLp p hs hμs c - indicatorConstLp p hs hμs c' =
    indicatorConstLp p hs hμs (c - c')

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c c' : E
⊢ MemLp.toLp ((s.indicator fun x => c) - s.indicator fun x => c') ⋯ =
    MemLp.toLp (fun a => s.indicator (fun x => c) a - s.indicator (fun x => c') a) ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c c' : E
⊢ indicatorConstLp p hs hμs c - indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c - c')

Tactic:
simp_rw [indicatorConstLp, ← MemLp.toLp_sub, indicator_sub]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c c' : E
⊢ MemLp.toLp ((s.indicator fun x => c) - s.indicator fun x => c') ⋯ =
    MemLp.toLp (fun a => s.indicator (fun x => c) a - s.indicator (fun x => c') a) ⋯
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem add_mul_right_right {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (y + z * x)

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)

Tactic:
rw [isCoprime_comm]

Result:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + z * x) x

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + z * x) x

Tactic:
exact h.symm.add_mul_right_left z

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem map_cyclotomic (n : ℕ) {R S : Type*} [Ring R] [Ring S] (f : R →+* S) :
    map f (cyclotomic n R) = cyclotomic n S

Proof state:
n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)

Tactic:
have : Subsingleton (ℤ →+* S) := inferInstance

Result:
n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
this : Subsingleton (ℤ →+* S)
⊢ map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)

Proof state:
n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map f (cyclotomic n R) = cyclotomic n S

Tactic:
rw [← map_cyclotomic_int n R, ← map_cyclotomic_int n S, map_map]

Result:
n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)

Proof state:
n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
this : Subsingleton (ℤ →+* S)
⊢ map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)

Tactic:
congr!

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
lemma commute_of_mem_adjoin_singleton_of_commute {a b c : A}
    (hc : c ∈ adjoin R {b}) (h : Commute a b) (h_star : Commute a (star b)) :
    Commute a c :=
  commute_of_mem_adjoin_of_forall_mem_commute hc (by simpa) (by simpa)

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
a b c : A
hc : c ∈ adjoin R {b}
h : Commute a b
h_star : Commute a (star b)
⊢ ∀ b_1 ∈ {b}, Commute a b_1

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
a b c : A
hc : c ∈ adjoin R {b}
h : Commute a b
h_star : Commute a (star b)
⊢ ∀ b_1 ∈ {b}, Commute a (star b_1)

Tactic:
simpa

Result:
no goals